Document Open Access Logo

Representation of Peano Arithmetic in Separation Logic

Authors Sohei Ito , Makoto Tatsuta

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.18.pdf
  • Filesize: 0.76 MB
  • 17 pages

Document Identifiers

Author Details

Sohei Ito
  • Nagasaki University, Nagasaki, Japan
Makoto Tatsuta
  • National Institute of Informatics / Sokendai, Tokyo, Japan

Funding

  • Ito, Sohei: MEXT/JSPS KAKENHI Grant Number JP21K11756, ROIS NII Open Collaborative Research 2023(22FP03)
  • Tatsuta, Makoto: ROIS NII Open Collaborative Research 2023(22FP03)

Cite AsGet BibTex

Sohei Ito and Makoto Tatsuta. Representation of Peano Arithmetic in Separation Logic. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.18

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
Keywords
  • First order logic
  • Separation logic
  • Peano arithmetic
  • Presburger arithmetic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Joël Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8412 of Lecture Notes in Computer Science, pages 411-425. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54830-7_27.
  2. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. A decidable fragment of separation logic. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 97-109. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30538-5_9.
  3. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Symbolic execution with separation logic. In Kwangkeun Yi, editor, Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings, volume 3780 of Lecture Notes in Computer Science, pages 52-68. Springer, 2005. URL: https://doi.org/10.1007/11575467_5.
  4. Rémi Brochenin, Stéphane Demri, and Étienne Lozes. On the almighty wand. Inf. Comput., 211:106-137, 2012. URL: https://doi.org/10.1016/j.ic.2011.12.003.
  5. Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6):26:1-26:66, 2011. URL: https://doi.org/10.1145/2049697.2049700.
  6. Cristiano Calcagno, Philippa Gardner, and Matthew Hague. From separation logic to first-order logic. In Vladimiro Sassone, editor, Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3441 of Lecture Notes in Computer Science, pages 395-409. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31982-5_25.
  7. Cristiano Calcagno, Hongseok Yang, and Peter W. O'Hearn. Computability and complexity results for a spatial assertion language for data structures. In The Second Asian Workshop on Programming Languages and Systems, APLAS'01, Korea Advanced Institute of Science and Technology, Daejeon, Korea, December 17-18, 2001, Proceedings, pages 289-300, 2001. Google Scholar
  8. Byron Cook, Christoph Haase, Joël Ouaknine, Matthew J. Parkinson, and James Worrell. Tractable reasoning in a fragment of separation logic. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 235-249. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_16.
  9. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer-Verlag, 1995. Google Scholar
  10. Radu Iosif, Adam Rogalewicz, and Jirí Simácek. The tree width of separation logic with recursive definitions. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 21-38. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_2.
  11. Koji Nakazawa, Makoto Tatsuta, Daisuke Kimura, and Mitsuru Yamamura. Spatial factorization in cyclic-proof system for separation logic. Computer Software, 37(1):1_125-1_144, 2020. URL: https://doi.org/10.11309/jssst.37.1_125.
  12. Peter W. O'Hearn. Separation logic. Commun. ACM, 62(2):86-95, 2019. URL: https://doi.org/10.1145/3211968.
  13. Joseph R. Shoenfield. Mathematical Logic. Addison-Wesley, 1967. Google Scholar
  14. Makoto Tatsuta and Daisuke Kimura. Separation logic with monadic inductive definitions and implicit existentials. In Xinyu Feng and Sungwoo Park, editors, Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings, volume 9458 of Lecture Notes in Computer Science, pages 69-89. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-26529-2_5.
  15. Makoto Tatsuta, Quang Loc Le, and Wei-Ngan Chin. Decision procedure for separation logic with inductive definitions and presburger arithmetic. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, volume 10017 of Lecture Notes in Computer Science, pages 423-443, 2016. URL: https://doi.org/10.1007/978-3-319-47958-3_22.
  16. Makoto Tatsuta, Koji Nakazawa, and Daisuke Kimura. Completeness of cyclic proofs for symbolic heaps with inductive definitions. In Anthony Widjaja Lin, editor, Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, volume 11893 of Lecture Notes in Computer Science, pages 367-387. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-34175-6_19.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact