Document Open Access Logo

Matching Plans for Frame Inference in Compositional Reasoning

Authors Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, Philippa Gardner

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2024.26.pdf
  • Filesize: 0.84 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Separation logic
  • Theory of computation → Automated reasoning
Keywords
  • Compositional reasoning
  • separation logic
  • frame inference

Metrics

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

Abstract

The use of function specifications to reason about function calls and the manipulation of user-defined predicates are two essential ingredients of modern compositional verification tools based on separation logic. To execute these operations successfully, these tools must be able to solve the frame inference problem, that is, to understand which parts of the state are relevant for the operation at hand. We introduce matching plans, a concept that is used in the Gillian verification platform to automate frame inference efficiently. We extract matching plans and their automation machinery from the Gillian implementation and present them in a tool-agnostic way, making the Gillian approach available to the broader verification community as a verification-tool design pattern.

Cite As Get BibTex

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching Plans for Frame Inference in Compositional Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ECOOP.2024.26

Author Details

Andreas Lööw
  • Imperial College London, UK
Daniele Nantes-Sobrinho
  • Imperial College London, UK
Sacha-Élie Ayoun
  • Imperial College London, UK
Petar Maksimović
  • Imperial College London, UK
  • Runtime Verification Inc., Chicago, IL, USA
Philippa Gardner
  • Imperial College London, UK

Funding

This work was supported by the EPSRC Fellowship "VetSpec: Verified Trustworthy Software Specification" (EP/R034567/1).

Acknowledgements

We would like to thank José Fragoso Santos, who conceived the idea of matching plans (which we formalise in this work) as part of the work on JaVerT [Fragoso Santos et al., 2019] and did their original implementation in Gillian. We would also like to thank the anonymous reviewers for their comments.

References

  1. Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Computing Surveys, 51(3), 2018. URL: https://doi.org/10.1145/3182657.
  2. J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In International Conference on Formal Methods for Components and Objects, 2005. URL: https://doi.org/10.1007/11804192_6.
  3. J. Berdine, C. Calcagno, and P. W. O'Hearn. Symbolic execution with separation logic. In Asian Conference on Programming Languages and Systems, 2005. URL: https://doi.org/10.1007/11575467_5.
  4. Cristiano Calcagno and Dino Distefano. Infer: An automatic program verifier for memory safety of C programs. In NASA Formal Methods Symposium, 2011. URL: https://doi.org/10.1007/978-3-642-20398-5_33.
  5. Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, and Alexander J. Summers. Sound automation of magic wands. In Computer Aided Verification, 2022. URL: https://doi.org/10.1007/978-3-031-13188-2_7.
  6. José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner. JaVerT 2.0: Compositional symbolic execution for JavaScript. Proceedings of the ACM on Programming Languages, 3(POPL), 2019. URL: https://doi.org/10.1145/3290379.
  7. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In NASA Formal Methods Symposium, 2011. URL: https://doi.org/10.1007/978-3-642-20398-5_4.
  8. Bart Jacobs, Jan Smans, and Frank Piessens. The VeriFast Program Verifier: A Tutorial, 2017. URL: https://doi.org/10.5281/ZENODO.1068185.
  9. Daniel Jost and Alexander J. Summers. An automatic encoding from VeriFast predicates into implicit dynamic frames. In Verified Software: Theories, Tools, Experiments, 2014. URL: https://doi.org/10.1007/978-3-642-54108-7_11.
  10. Ioannis T. Kassios. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Symposium on Formal Methods, 2006. URL: https://doi.org/10.1007/11813040_19.
  11. Philipp Körner, Michael Leuschel, João Barbosa, Vítor Santos Costa, Verónica Dahl, Manuel V. Hermenegildo, Jose F. Morales, Jan Wielemaker, Daniel Diaz, Salvador Abreu, and Giovanni Ciatto. Fifty years of Prolog and beyond. Theory and Practice of Logic Programming, 22(6), 2022. URL: https://doi.org/10.1017/S1471068422000102.
  12. K. Rustan M. Leino. This is Boogie 2, 2008. URL: https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/.
  13. Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos, and Philippa Gardner. Gillian, part II: Real-world verification for JavaScript and C. In Computer Aided Verification, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_38.
  14. Michał Moskal. Programming with triggers. In Workshop on Satisfiability Modulo Theories, 2009. URL: https://doi.org/10.1145/1670412.1670416.
  15. Ike Mulder, Robbert Krebbers, and Herman Geuvers. Diaframe: Automated verification of fine-grained concurrent programs in Iris. In Conference on Programming Language Design and Implementation, 2022. URL: https://doi.org/10.1145/3519939.3523432.
  16. Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A verification infrastructure for permission-based reasoning. In Verification, Model Checking, and Abstract Interpretation, 2016. URL: https://doi.org/10.1007/978-3-662-49122-5_2.
  17. Huu Hai Nguyen, Viktor Kuncak, and Wei-Ngan Chin. Runtime checking for separation logic. In Verification, Model Checking, and Abstract Interpretation, 2008. URL: https://doi.org/10.1007/978-3-540-78163-9_19.
  18. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Computer Science Logic, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  19. Matthew J. Parkinson and Alexander J. Summers. The relationship between separation logic and implicit dynamic frames. In European Symposium on Programming, 2011. URL: https://doi.org/10.1007/978-3-642-19718-5_23.
  20. Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami. CN: Verifying systems C code with separation-logic refinement types. Proceedings of the ACM on Programming Languages, 7(POPL), 2023. URL: https://doi.org/10.1145/3571194.
  21. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  22. Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. RefinedC: Automating the foundational verification of C code with refined ownership types. In International Conference on Programming Language Design and Implementation, 2021. URL: https://doi.org/10.1145/3453483.3454036.
  23. Malte Schwerhoff and Alexander J. Summers. Lightweight support for magic wands in an automatic verifier. In European Conference on Object-Oriented Programming, 2015. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2015.614.
  24. Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In European Conference on Object-Oriented Programming, 2009. URL: https://doi.org/10.1007/978-3-642-03013-0_8.
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