Document Open Access Logo

Reasoning on Dynamic Transformations of Symbolic Heaps

Author Nicolas Peltier

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2022.9.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
  • Theory of computation → Automated reasoning
  • Theory of computation → Modal and temporal logics
Keywords
  • Separation Logic
  • Symbolic Heaps
  • Linear Temporal Logic

Metrics

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

Abstract

Building on previous results concerning the decidability of the satisfiability and entailment problems for separation logic formulas with inductively defined predicates, we devise a proof procedure to reason on dynamic transformations of memory heaps. The initial state of the system is described by a separation logic formula of some particular form, its evolution is modeled by a finite transition system and the expected property is given as a linear temporal logic formula built over assertions in separation logic.

Cite As Get BibTex

Nicolas Peltier. Reasoning on Dynamic Transformations of Symbolic Heaps. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.TIME.2022.9

Author Details

Nicolas Peltier
  • Univ. Grenoble Alpes, CNRS, LIG, Grenoble, France

Funding

This work has been partially funded by the the French National Research Agency (ANR-21-CE48-0011).

References

  1. Callum Bannister, Peter Höfner, and Gerwin Klein. Backwards and forwards with separation logic. In Jeremy Avigad and Assia Mahboubi, editors, ITP 2018, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of LNCS, pages 68-87. Springer, 2018. Google Scholar
  2. Rémi Brochenin, Stéphane Demri, and Étienne Lozes. Reasoning about sequences of memory states. In Sergei N. Artëmov and Anil Nerode, editors, LFCS 2007, New York, NY, USA, June 4-7, 2007, Proceedings, volume 4514 of LNCS, pages 100-114. Springer, 2007. Google Scholar
  3. James Brotherston, Carsten Fuhs, Juan Antonio Navarro Pérez, and Nikos Gorogiannis. A decision procedure for satisfiability in separation logic with inductive predicates. In Thomas A. Henzinger and Dale Miller, editors, CSL-LICS '14, Vienna, Austria, July 14-18, 2014, pages 25:1-25:10. ACM, 2014. Google Scholar
  4. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Entailment checking in separation logic with inductive definitions is 2-exptime hard. In LPAR 2020, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC Series in Computing, pages 191-211. EasyChair, 2020. Google Scholar
  5. Mnacho Echenim, Radu Iosif, and Nicolas Peltier. Decidable entailments in separation logic with inductive definitions: Beyond establishment. In CSL 2021, EPiC Series in Computing. EasyChair, 2021. Google Scholar
  6. Didier Galmiche and Daniel Méry. Labelled tableaux for linear time bunched implication logic. In ASL 2022 (Workshop on Advancing Separation Logic), 2022. Google Scholar
  7. Radu Iosif, Adam Rogalewicz, and Jiri Simacek. The tree width of separation logic with recursive definitions. In Proc. of CADE-24, volume 7898 of LNCS, 2013. Google Scholar
  8. Norihiro Kamide. Temporal BI: proof system, semantics and translations. Theor. Comput. Sci., 492:40-69, 2013. Google Scholar
  9. Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM, 53(6):937-977, 2006. Google Scholar
  10. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bull. Symb. Log., 5(2):215-244, 1999. Google Scholar
  11. Jens Pagel, Christoph Matheja, and Florian Zuleger. Complete entailment checking for separation logic with inductive definitions, 2020. URL: http://arxiv.org/abs/2002.01202.
  12. Jens Pagel and Florian Zuleger. Beyond symbolic heaps: Deciding separation logic with inductive definitions. In LPAR-23, volume 73 of EPiC Series in Computing, pages 390-408. EasyChair, 2020. Google Scholar
  13. Amir Pnueli. The temporal logic of programs. In FOCS, Providence, Rhode Island, USA, pages 46-57. IEEE Computer Society, 1977. Google Scholar
  14. J.C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. of LICS'02, 2002. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact