Authors: Adithya Murali, Cody Rivera, and P. Madhusudan
Proceedings of the ACM on Programming Languages, Volume 8, Issue PLDI
Article No.: 220, Pages 1804 - 1829
Published: 20 June 2024 Publication History
Related Artifact: Artifact for ``Predictable Verification using Intrinsic Definitions'' June 2024softwarehttps://doi.org/10.5281/zenodo.10963124
- 0citation
- 72
- Downloads
Metrics
Total Citations0Total Downloads72Last 12 Months72
Last 6 weeks72
New Citation Alert added!
This alert has been successfully added and will be sent to:
You will be notified whenever a record that you have chosen has been cited.
To manage your alert preferences, click on the button below.
Manage my Alerts
New Citation Alert!
Please log in to your account
PDFeReader
- View Options
- References
- Media
- Tables
- Share
Abstract
We propose a novel mechanism of defining data structures using intrinsic definitions that avoids recursion and instead utilizes monadic maps satisfying local conditions. We show that intrinsic definitions are a powerful mechanism that can capture a variety of data structures naturally. We show that they also enable a predictable verification methodology that allows engineers to write ghost code to update monadic maps and perform verification using reduction to decidable logics. We evaluate our methodology using Boogie and prove a suite of data structure manipulating programs correct.
Supplementary Material
These are the Appendices referenced in the paper "Predictable Verification using Intrinsic Definitions".
- Download
- 741.90 KB
References
[1]
Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max Kanovich, and Joël Ouaknine. 2014. Foundations for Decision Problems in Separation Logic with General Inductive Predicates. In Foundations of Software Science and Computation Structures, Anca Muscholl (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 411–425. isbn:978-3-642-54830-7
[2]
Anindya Banerjee, Mike Barnett, and David A. Naumann. 2008. Boogie Meets Regions: A Verification Experience Report. In Verified Software: Theories, Tools, Experiments, Natarajan Shankar and Jim Woodco*ck (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 177–191. isbn:978-3-540-87873-5
[3]
Anindya Banerjee and David A. Naumann. 2013. Local Reasoning for Global Invariants, Part II: Dynamic Boundaries. J. ACM, 60, 3 (2013), Article 19, jun, 73 pages. issn:0004-5411 https://doi.org/10.1145/2485981
Digital Library
[4]
Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2008. Regional Logic for Local Reasoning about Global Invariants. In ECOOP 2008 – Object-Oriented Programming, Jan Vitek (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 387–411. isbn:978-3-540-70592-5
Digital Library
[5]
Anindya Banerjee, David A. Naumann, and Stan Rosenberg. 2013. Local Reasoning for Global Invariants, Part I: Region Logic. J. ACM, 60, 3 (2013), Article 18, June, 56 pages. issn:0004-5411 http://doi.acm.org/10.1145/2485982
Digital Library
[6]
Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2006. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 364–387. isbn:978-3-540-36750-5
[7]
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 171–177. isbn:978-3-642-22110-1
[8]
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. A Decidable Fragment of Separation Logic. In FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, Kamal Lodaya and Meena Mahajan (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 97–109. isbn:978-3-540-30538-5
[9]
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Symbolic Execution with Separation Logic. In Programming Languages and Systems, Kwangkeun Yi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 52–68. isbn:978-3-540-32247-4
[10]
Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2006. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects (FMCO’05). Springer-Verlag, Berlin, Heidelberg. 115–137. isbn:3-540-36749-7, 978-3-540-36749-9 https://doi.org/10.1007/11804192_6
Digital Library
[11]
Rémi Brochenin, Stéphane Demri, and Etienne Lozes. 2008. On the Almighty Wand. In Computer Science Logic, Michael Kaminski and Simone Martini (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 323–338. isbn:978-3-540-87531-4
[12]
Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2011. Compositional Shape Analysis by Means of Bi-Abduction. J. ACM, 58, 6 (2011), Article 26, dec, 66 pages. issn:0004-5411 https://doi.org/10.1145/2049697.2049700
Digital Library
[13]
Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. 2007. Automated Verification of Shape, Size and Bag Properties. In Proceedings of the 12th IEEE International Conference on Engineering Complex Computer Systems (ICECCS ’07). IEEE Computer Society, USA. 307–320. isbn:0769528953 https://doi.org/10.1109/ICECCS.2007.17
Digital Library
[14]
Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. 2015. Automatic Induction Proofs of Data-Structures in Imperative Programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 457–466. isbn:9781450334686 https://doi.org/10.1145/2737924.2737984
[15]
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 23–42. isbn:978-3-642-03359-9
[16]
Jeremy Condit, Brian Hackett, Shuvendu K. Lahiri, and Shaz Qadeer. 2009. Unifying Type Checking and Property Checking for Low-Level Code. SIGPLAN Not., 44, 1 (2009), jan, 302–314. issn:0362-1340 https://doi.org/10.1145/1594834.1480921
Digital Library
[17]
Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08). Springer-Verlag, Berlin, Heidelberg. 337–340. isbn:3-540-78799-2, 978-3-540-78799-0
Digital Library
[18]
Leonardo de Moura and Nikolaj Bjørner. 2009. Generalized, efficient array decision procedures. In 2009 Formal Methods in Computer-Aided Design. IEEE, 45–52. https://doi.org/10.1109/FMCAD.2009.5351142
[19]
David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, and Emma Zhong. 2022. Fast and Reliable Formal Verification of Smart Contracts with the Move Prover. In Tools and Algorithms for the Construction and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham. 183–200. isbn:978-3-030-99524-9
[20]
Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2006. A Local Shape Analysis Based on Separation Logic. In Tools and Algorithms for the Construction and Analysis of Systems, Holger Hermanns and Jens Palsberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 287–302. isbn:978-3-540-33057-8
[21]
Dino Distefano and Matthew Parkinson. 2008. jStar: Towards Practical Verification for Java. Sigplan Notices - SIGPLAN, 43, 213–226. https://doi.org/10.1145/1449764.1449782
Digital Library
[22]
Mnacho Echenim, Radu Iosif, and Nicolas Peltier. 2021. Unifying Decidable Entailments in Separation Logic with Inductive Definitions. In Automated Deduction – CADE 28, André Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham. 183–199. isbn:978-3-030-79876-5
[23]
Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. 2016. The spirit of ghost code. Formal Methods in System Design, 48 (2016), 152–174.
Digital Library
[24]
Alex Gyori, Pranav Garg, Edgar Pek, and P. Madhusudan. 2017. Efficient Incrementalized Runtime Checking of Linear Measures on Lists. In 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, March 13-17, 2017. IEEE Computer Society, 310–320. https://doi.org/10.1109/ICST.2017.35
[25]
Radu Iosif, Adam Rogalewicz, and Jiri Simacek. 2013. The Tree Width of Separation Logic with Recursive Definitions. In Automated Deduction – CADE-24, Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 21–38. isbn:978-3-642-38574-2
[26]
Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. 2011. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In Proceedings of the Third International Conference on NASA Formal Methods (NFM’11). Springer-Verlag, Berlin, Heidelberg. 41–55. isbn:9783642203978
[27]
C. B. Jones. 2010. The Role of Auxiliary Variables in the Formal Development of Concurrent Programs. In Reflections on the Work of C.A.R. Hoare, A.W. Roscoe, Cliff B. Jones, and Kenneth R. Wood (Eds.). Springer London, London. 167–187. isbn:978-1-84882-912-1 https://doi.org/10.1007/978-1-84882-912-1_8
[28]
Bernhard Kragl and Shaz Qadeer. 2021. The Civl Verifier. In 2021 Formal Methods in Computer Aided Design (FMCAD). 143–152. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_23
[29]
Siddharth Krishna, Nisarg Patel, Dennis Shasha, and Thomas Wies. 2020. Verifying Concurrent Search Structure Templates. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). Association for Computing Machinery, New York, NY, USA. 181–196. isbn:9781450376136 https://doi.org/10.1145/3385412.3386029
Digital Library
[30]
Siddharth Krishna, Dennis E. Shasha, and Thomas Wies. 2018. Go with the flow: compositional abstractions for concurrent data structures. Proc. ACM Program. Lang., 2, POPL (2018), 37:1–37:31. https://doi.org/10.1145/3158125
Digital Library
[31]
Siddharth Krishna, Alexander J. Summers, and Thomas Wies. 2020. Local Reasoning for Global Graph Properties. In Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Peter Müller (Ed.) (Lecture Notes in Computer Science, Vol. 12075). Springer, 308–335. https://doi.org/10.1007/978-3-030-44914-8_12
Digital Library
[32]
Shuvendu Lahiri and Shaz Qadeer. 2008. Back to the Future: Revisiting Precise Program Verification Using SMT Solvers. SIGPLAN Not., 43, 1 (2008), jan, 171–182. issn:0362-1340 https://doi.org/10.1145/1328897.1328461
Digital Library
[33]
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs Using Linear Ghost Types. Proc. ACM Program. Lang., 7, OOPSLA1 (2023), Article 85, apr, 30 pages. https://doi.org/10.1145/3586037
Digital Library
[34]
Oukseh Lee, Hongseok Yang, and Rasmus Petersen. 2011. Program Analysis for Overlaid Data Structures. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 592–608. isbn:978-3-642-22110-1
[35]
K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning. 348–370.
[36]
Tal Lev-Ami, Neil Immerman, Thomas Reps, Mooly Sagiv, Siddharth Srivastava, and Greta Yorsh. 2009. Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science, 5 (2009), 04, https://doi.org/10.2168/LMCS-5(2:12)2009
[37]
Christof Löding, P. Madhusudan, and Lucas Peña. 2018. Foundations for natural proofs and quantifier instantiation. PACMPL, 2, POPL (2018), 10:1–10:30. https://doi.org/10.1145/3158098
Digital Library
[38]
P Lucas. 1968. Two constructive realizations of the block concept and their equivalence, IBM Lab. Vienna TR 25.085.
[39]
P. Madhusudan, Gennaro Parlato, and Xiaokang Qiu. 2011. Decidable Logics Combining Heap Structures and Data. SIGPLAN Not., 46, 1 (2011), jan, 611–622. issn:0362-1340 https://doi.org/10.1145/1925844.1926455
Digital Library
[40]
P. Madhusudan and Xiaokang Qiu. 2011. Efficient Decision Procedures for Heaps Using STRAND. In Static Analysis, Eran Yahav (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 43–59. isbn:978-3-642-23702-7
[41]
Roland Meyer, Thomas Wies, and Sebastian Wolff. 2022. A Concurrent Program Logic with a Future and History. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), Article 174, oct, 30 pages. https://doi.org/10.1145/3563337
Digital Library
[42]
Roland Meyer, Thomas Wies, and Sebastian Wolff. 2023. Make Flows Small Again: Revisiting the Flow Framework. In Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023, Proceedings, Part I. Springer-Verlag, Berlin, Heidelberg. 628–646. isbn:978-3-031-30822-2 https://doi.org/10.1007/978-3-031-30823-9_32
Digital Library
[43]
Peter Müller, Malte Schwerhoff, and Alexander J. Summers. 2016. Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham. 405–425.
[44]
Adithya Murali, Lucas Peña, Eion Blanchard, Christof Löding, and P. Madhusudan. 2022. Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), Article 191, oct, 30 pages. https://doi.org/10.1145/3563354
Digital Library
[45]
Adithya Murali, Lucas Peña, Ranjit Jhala, and P. Madhusudan. 2023. Complete First-Order Reasoning for Properties of Functional Programs. Proc. ACM Program. Lang., 7, OOPSLA2 (2023), Article 259, oct, 30 pages. https://doi.org/10.1145/3622835
Digital Library
[46]
Adithya Murali, Cody Rivera, and P. Madhusudan. 2024. Artifact for “Predictable Verification using Intrinsic Definitions” (v1.0). https://doi.org/10.5281/zenodo.10963124
Digital Library
[47]
Adithya Murali, Cody Rivera, and P. Madhusudan. 2024. Predictable Verification using Intrinsic Defintitions (Technical Report), arXiv 2404.04515. arxiv:2404.04515
[48]
Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph. D. Dissertation. Stanford University. Stanford, CA, USA. AAI8011683
[49]
Greg Nelson and Derek C. Oppen. 1979. Simplification by Cooperating Decision Procedures. ACM Trans. Program. Lang. Syst., 1, 2 (1979), oct, 245–257. issn:0164-0925 https://doi.org/10.1145/357073.357079
Digital Library
[50]
Huu Hai Nguyen and Wei-Ngan Chin. 2008. Enhancing Program Verification with Lemmas. In Proceedings of the 20th International Conference on Computer Aided Verification (CAV ’08). Springer-Verlag, Berlin, Heidelberg. 355–369. isbn:9783540705437 https://doi.org/10.1007/978-3-540-70545-1_34
Digital Library
[51]
Peter W. O’Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security - Tools for Analysis and Verification, Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann (Eds.) (NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 33). IOS Press, 286–318. https://doi.org/10.3233/978-1-61499-028-4-286
[52]
Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning About Programs That Alter Data Structures. In Proceedings of the 15th International Workshop on Computer Science Logic (CSL ’01). Springer-Verlag, London, UK, UK. 1–19. isbn:3-540-42554-3 http://dl.acm.org/citation.cfm?id=647851.737404
Digital Library
[53]
Nisarg Patel, Siddharth Krishna, Dennis Shasha, and Thomas Wies. 2021. Verifying Concurrent Multicopy Search Structures. Proc. ACM Program. Lang., 5, OOPSLA (2021), Article 113, oct, 32 pages. https://doi.org/10.1145/3485490
Digital Library
[54]
Edgar Pek, Xiaokang Qiu, and P. Madhusudan. 2014. Natural Proofs for Data Structure Manipulation in C Using Separation Logic. SIGPLAN Not., 49, 6 (2014), jun, 440–451. issn:0362-1340 https://doi.org/10.1145/2666356.2594325
Digital Library
[55]
Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating Separation Logic Using SMT. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13). Springer-Verlag, Berlin, Heidelberg. 773–789. isbn:978-3-642-39798-1 https://doi.org/10.1007/978-3-642-39799-8_54
[56]
Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. Automating Separation Logic with Trees and Data. In Proceedings of the 16th International Conference on Computer Aided Verification (CAV’14). Springer-Verlag, Berlin, Heidelberg. 711–728.
Digital Library
[57]
John C. Reynolds. 1981. The craft of programming. Prentice Hall. isbn:978-0-13-188862-3
[58]
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS ’02). IEEE Computer Society, USA. 55–74. isbn:0769514839
Digital Library
[59]
John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS ’02). IEEE Computer Society, USA. 55–74. isbn:0769514839
Digital Library
[60]
Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid types. SIGPLAN Not., 43, 6 (2008), jun, 159–169. issn:0362-1340 https://doi.org/10.1145/1379022.1375602
Digital Library
[61]
Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. 2002. Parametric Shape Analysis via 3-Valued Logic. ACM Trans. Program. Lang. Syst., 24, 3 (2002), may, 217–298. issn:0164-0925 https://doi.org/10.1145/514188.514190
Digital Library
[62]
Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2016. Automated Mutual Explicit Induction Proof in Separation Logic. In FM 2016: Formal Methods, John Fitzgerald, Constance Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.). Springer International Publishing, Cham. 659–676. https://doi.org/10.1007/978-3-319-48989-6_40
[63]
Cesare Tinelli and Calogero G. Zarba. 2004. Combining Decision Procedures for Sorted Theories. In Logics in Artificial Intelligence, Jóse Júlio Alferes and João Leite (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 641–653. isbn:978-3-540-30227-8
Index Terms
Predictable Verification using Intrinsic Definitions
Software and its engineering
Software creation and management
Software verification and validation
Formal software verification
Theory of computation
Logic
Automated reasoning
Logic and verification
Recommendations
- Multi-parameterised compositional verification of safety properties
We introduce a fully automatic technique for the parameterised verification of safety properties. The technique combines compositionality and completeness with support to multiple parameters and it is implemented in a tool. We start with an LTS-based (...
Read More
- Decidability of infinite-state timed CCP processes and first-order LTL
Expressiveness in concurrency
The ntcc process calculus is a timed concurrent constraint programming (ccp) model equipped with a first-order linear-temporal logic (LTL) for expressing process specifications. A typical behavioral observation in ccp is the strongest postcondition (sp)...
Read More
- Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
The completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Read More
Comments
Information & Contributors
Information
Published In
Proceedings of the ACM on Programming Languages Volume 8, Issue PLDI
June 2024
2198 pages
EISSN:2475-1421
DOI:10.1145/3554317
- Editor:
- Michael Hicks
Amazon, USA
Issue’s Table of Contents
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 June 2024
Published inPACMPLVolume 8, Issue PLDI
Permissions
Request permissions for this article.
Check for updates
Badges
Author Tags
- Decidability
- Ghost-Code Annotations
- Intrinsic Definitions
- Predictable Verification
- Verification of Linked Data Structures
Qualifiers
- Research-article
Contributors
Other Metrics
View Article Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
Total Citations
72
Total Downloads
- Downloads (Last 12 months)72
- Downloads (Last 6 weeks)72
Other Metrics
View Author Metrics
Citations
View Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderGet Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in
Full Access
Get this Article
Media
Figures
Other
Tables