Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

Sohei Ito, Makoto Tatsuta

Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software…