Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

Sohei Ito, Makoto Tatsuta

Abstract

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 where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.

Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic

Abstract

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 where numbers are important. However, properties of the validity such as decidability and complexity for separation logic with numbers have not been fully studied yet. This paper presents the translation of Pi-0-1 formulas in Peano arithmetic to formulas in a small fragment of separation logic with numbers, which consists only of the intuitionistic points-to predicate, 0 and the successor function. Then this paper proves that a formula in Peano arithmetic is valid in the standard model if and only if its translation in this fragment is valid in the standard interpretation. As a corollary, this paper also gives a perspective proof for the undecidability of the validity in this fragment. Since Pi-0-1 formulas can describe consistency of logical systems and non-termination of computations, this result also shows that these properties discussed in Peano arithmetic can also be discussed in such a small fragment of separation logic with numbers.

Paper Structure

This paper contains 8 sections, 20 theorems, 163 equations.

Table of Contents

  1. Introduction
  2. Peano arithmetic
  3. Separation logic with numbers $\mathsf{SLN}$
  4. Translation of Normal Formulas in $\mathsf{PA}$ into $\mathsf{SLN}$
  5. Translation from $\mathsf{PA}$ into $\mathsf{SLN}$
  6. Another undecidability proof
  7. $\Pi^0_1$-completeness of validity in $\mathsf{SLN}$
  8. Conclusion

Key Result

Lemma 4.3

Let $\sigma$ be a variable assignment and $h$ be a heap. (1) If $\sigma, h \models H$, $h(m)=0$, $h(m+1) = n+3$ and $h(m+2) = k+3$, then $h(m+3) = n + k + 3$. (2) If $\sigma, h \models H$, $h(m)=1$, $h(m+1) = n+3$ and $h(m+2) = k+3$, then $h(m+3) = n \times k + 3$. (3) If $\sigma, h \models H$, $h(m

Theorems & Definitions (31)

  • Definition 4.1: Normal form
  • Definition 4.2: Table Heap Condition
  • Lemma 4.3
  • Definition 4.4: Translation $( \cdot )^\circ$
  • Definition 4.5
  • Definition 4.6
  • Lemma 4.7
  • Lemma 4.8
  • Lemma 4.9
  • Lemma 4.10
  • ...and 21 more