Nothing Special   »   [go: up one dir, main page]
Document Open Access Logo

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

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

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.25.pdf
  • Filesize: 1.09 MB
  • 28 pages

Document Identifiers

Author Details

Andreas Lööw
  • Imperial College London, UK
Daniele Nantes-Sobrinho
  • Imperial College London, UK
Sacha-Élie Ayoun
  • Imperial College London, UK
Caroline Cronjäger
  • Ruhr-Universität Bochum, Germany
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 Nat Karmios for help with preparing the artefact for this paper. We would also like to thank the anonymous reviewers for their comments.

Cite AsGet BibTex

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 25:1-25:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.25

Abstract

The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction. We evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool grounded on a common formal compositional symbolic execution engine to support both correctness and incorrectness reasoning.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Program analysis
  • Theory of computation → Separation logic
  • Theory of computation → Automated reasoning
Keywords
  • separation logic
  • incorrectness logic
  • symbolic execution
  • bi-abduction

Metrics

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

Related Versions

Supplementary Materials

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. Josh Berdine, Cristiano Calcagno, and Peter 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. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Symbolic execution with separation logic. In Asian Symposium 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. Cristiano Calcagno, Dino Distefano, Peter O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. In Principles of Programming Languages, 2009. URL: https://doi.org/10.1145/1480881.1480917.
  6. Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. Journal of the ACM, 58(6), 2011. URL: https://doi.org/10.1145/2049697.2049700.
  7. David Darais, Nicholas Labich, Phúc C. Nguyen, and David Van Horn. Abstracting definitional interpreters (functional pearl). Proceedings of the ACM on Programming Languages, 1(ICFP), 2017. URL: https://doi.org/10.1145/3110256.
  8. José Fragoso Santos, Petar Maksimović, Théotime Grohens, Julian Dolby, and Philippa Gardner. Symbolic execution for JavaScript. In Principles and Practice of Declarative Programming, 2018. URL: https://doi.org/10.1145/3236950.3236956.
  9. José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner. JaVerT: Javascript verification toolchain. Proceedings of the ACM on Programming Languages, 2(POPL), 2018. URL: https://doi.org/10.1145/3158138.
  10. 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.
  11. José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, and Philippa Gardner. Gillian, part I: A multi-language platform for symbolic execution. In Programming Language Design and Implementation, 2020. URL: https://doi.org/10.1145/3385412.3386014.
  12. Philippa Gardner, Sergio Maffeis, and Gareth David Smith. Towards a program logic for JavaScript. In Principles of Programming Languages, 2012. URL: https://doi.org/10.1145/2103656.2103663.
  13. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and Sai Deep Tetali. Compositional may-must program analysis: Unleashing the power of alternation. In Principles of Programming Languages, 2010. URL: https://doi.org/10.1145/1706299.1706307.
  14. 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.
  15. Bart Jacobs, Frédéric Vogels, and Frank Piessens. Featherweight VeriFast. Logical Methods in Computer Science, 11, 2015. URL: https://doi.org/10.2168/LMCS-11(3:19)2015.
  16. Daniel Kroening and Michael Tautschnig. CBMC - C bounded model checker. In Tools and Algorithms for the Construction and Analysis of Systems, 2014. URL: https://doi.org/10.1007/978-3-642-54862-8_26.
  17. Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn. Finding real bugs in big programs with incorrectness logic. Proceedings of the ACM on Programming Languages, 6(OOPSLA1), 2022. URL: https://doi.org/10.1145/3527325.
  18. Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional symbolic execution for correctness and incorrectness reasoning (extended version), 2024. URL: https://doi.org/10.48550/arXiv.2407.10838.
  19. Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching plans for frame inference in compositional reasoning. In European Conference on Object-Oriented Programming, 2024. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2024.26.
  20. Petar Maksimović, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner. Exact separation logic. In European Conference on Object-Oriented Programming, 2023. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.19.
  21. 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.
  22. Adrian D. Mensing, Hendrik van Antwerpen, Casper Bach Poulsen, and Eelco Visser. From definitional interpreter to symbolic executor. In International Workshop on Meta-Programming Techniques and Reflection, 2019. URL: https://doi.org/10.1145/3358502.3361269.
  23. 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.
  24. 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.
  25. Srdja Panić. Collections-C: A library of generic data structures. https://github.com/srdja/Collections-C, 2014.
  26. 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.
  27. Sorawee Porncharoenwase, Luke Nelson, Xi Wang, and Emina Torlak. A formal foundation for symbolic evaluation with merging. Proceedings of the ACM on Programming Languages, 6(POPL), 2022. URL: https://doi.org/10.1145/3498709.
  28. Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn, and Jules Villard. Local reasoning about the presence of bugs: Incorrectness separation logic. In Computer Aided Verification, 2020. URL: https://doi.org/10.1007/978-3-030-53291-8_14.
  29. 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.
  30. Malte Hermann Schwerhoff. Advancing Automated, Permission-Based Program Verification Using Symbolic Execution. PhD thesis, ETH Zürich, 2016. Google Scholar
  31. Jan Smans, Bart Jacobs, and Frank Piessens. Implicit dynamic frames: Combining dynamic frames and separation logic. In European Conference on Object-Oriented Programming (ECOOP), 2009. URL: https://doi.org/10.1007/978-3-642-03013-0_8.
  32. Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In Conference on Programming Language Design and Implementation, 2014. URL: https://doi.org/10.1145/2594291.2594340.
  33. Hongseok Yang. Local Reasoning for Stateful Programs. PhD thesis, University of Illinois Urbana-Champaign, 2001. Google Scholar
  34. Noam Zilberstein, Derek Dreyer, and Alexandra Silva. Outcome logic: A unifying foundation for correctness and incorrectness reasoning. Proceedings of the ACM on Programming Languages, 7(OOPSLA1), 2023. URL: https://doi.org/10.1145/3586045.
  35. Conrad Zimmerman, Jenna DiVincenzo, and Jonathan Aldrich. Sound gradual verification with symbolic execution. Proceedings of the ACM on Programming Languages, 8(POPL), 2024. URL: https://doi.org/10.1145/3632927.
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