Predictable Verification using Intrinsic Definitions (2024)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

P Lucas. 1968. Two constructive realizations of the block concept and their equivalence, IBM Lab. Vienna TR 25.085.

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

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

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

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

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.

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

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

Adithya Murali, Cody Rivera, and P. Madhusudan. 2024. Artifact for “Predictable Verification using Intrinsic Definitions” (v1.0). https://doi.org/10.5281/zenodo.10963124

Adithya Murali, Cody Rivera, and P. Madhusudan. 2024. Predictable Verification using Intrinsic Defintitions (Technical Report), arXiv 2404.04515. arxiv:2404.04515

Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph. D. Dissertation. Stanford University. Stanford, CA, USA. AAI8011683

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

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

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

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

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

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

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

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.

John C. Reynolds. 1981. The craft of programming. Prentice Hall. isbn:978-0-13-188862-3

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

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

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

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

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

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