Christof Löding
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We give foundational results that explain the efficacy of heuristics used for dealing with quantified formulas and recursive definitions. We develop a framework for first order logic (FOL) over an uninterpreted combination of background theories. Our central technical result is that systematic term instantiation is complete for a fragment of FOL that we call safe. Coupled with the fact that unfolding recursive definitions is essentially term instantiation and with the observation that heap verification engines generate verification conditions in the safe fragment explains the efficacy of verification engines like natural proofs that resort to such heuristics. Furthermore, we study recursive definitions with least fixpoint semantics and show that though they are not amenable to complete procedures, we can systematically introduce induction principles that in practice bridge the divide between FOL and FOL with recursive definitions.
Supplemental Material
Available for Download
zip
popl18-p99-aux.zip (27.7 KB)
This is the artifact associated with Section 6.3 in the paper. The entries in Table 1 as well as the information in the section regarding the McCarthy 91 function can all be justified with this code. All files compiled with Z3 version 4.4.1
- Aharon Abadi, Alexander Rabinovich, and Mooly Sagiv. 2007. Decidable Fragments of Many-sorted Logic. In LPAR’07. 17–31. http://dl.acm.org/citation.cfm?id=1779419.1779423Google Scholar
- Rolf Backofen, James Rogers, and K. Vijay-Shanker. 1995. A First-Order Axiomatization of the Theory of Finite Trees. Journal of Logic, Language and Information 4, 1 (1995), 5–39. Google ScholarCross Ref
- Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In CAV’11. 171–177. Google ScholarCross Ref
- Clark Barrett and Cesare Tinelli. 2007. CVC3. In CAV’07. 298–302. Google ScholarCross Ref
- Egon Börger, Erich Grädel, and Yuri Gurevich. 1997. The Classical Decision Problem. Springer. Google ScholarCross Ref
- Robert S. Boyer and J. Strother Moore. 1980. A computational logic. Academic Press.Google Scholar
- Aaron Bradley. 2007. Safety Analysis of Systems. Ph.D. Dissertation. Stanford University.Google Scholar
- Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag New York, Inc., Secaucus, NJ, USA.Google ScholarDigital Library
- Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What’s Decidable About Arrays?. In VMCAI’06, Vol. 3855. Springer, 427–442. Google ScholarCross Ref
- James Brotherston, Dino Distefano, and Rasmus Lerchedahl Petersen. 2011. Automated Cyclic Entailment Proofs in Separation Logic. In CADE’11. Springer-Verlag, 131–146. http://dl.acm.org/citation.cfm?id=2032266.2032278 Google ScholarCross Ref
- Duc-Hiep Chu, Joxan Jaffar, and Minh-Thai Trinh. 2015. Automatic induction proofs of data-structures in imperative programs. In PLDI’15. 457–466. Google ScholarDigital Library
- Martin Davis and Hilary Putnam. 1960. A Computing Procedure for Quantification Theory. J. ACM 7, 3 (1960), 201–215. Google ScholarDigital Library
- Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340.Google ScholarDigital Library
- David Detlefs, Greg Nelson, and James B. Saxe. 2005. Simplify: A Theorem Prover for Program Checking. J. ACM 52, 3 (May 2005), 365–473. Google ScholarDigital Library
- Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. 2013. Inductive invariant generation via abductive inference. In OOPSLA’13. 443–456. Google ScholarDigital Library
- Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas. 1994. Mathematical logic (2. ed.). Springer.Google Scholar
- Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham. 2017. Bounded Quantifier Instantiation for Checking Inductive Invariants. In TACAS 2017 (Lecture Notes in Computer Science), Vol. 10205. 76–95. Google ScholarCross Ref
- Harald Ganzinger and Konstantin Korovin. 2003. New Directions in Instantiation-Based Theorem Proving. In LICS’03. IEEE Computer Society, 55–64. Google ScholarCross Ref
- Harald Ganzinger and Konstantin Korovin. 2006. Theory Instantiation. In LPAR’06. 497–511. Google ScholarDigital Library
- Yeting Ge and Leonardo Mendonça de Moura. 2009. Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. In CAV’09 (Lecture Notes in Computer Science), Vol. 5643. Springer, 306–320. Google ScholarDigital Library
- Paul C. Gilmore. 1960. A Proof Method for Quantification Theory: Its Justification and Realization. IBM Journal of Research and Development 4, 1 (1960), 28–35. Google ScholarDigital Library
- Andrzej Granas and James Dugundji. 2003. Fixed Point Theory. Springer. Google ScholarCross Ref
- John Harrison, Josef Urban, and Freek Wiedijk. 2014. History of Interactive Theorem Proving. In Computational Logic. 135–214. Google ScholarCross Ref
- Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans. 2008. On Local Reasoning in Verification. In TACAS’08/ETAPS’08. 265–281. Google ScholarCross Ref
- Bart Jacobs and Frank Piessens. 2008. The VeriFast Program Verifier. (2008).Google Scholar
- Matt Kaufmann and J. Strother Moore. 1997. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. Software Eng. 23, 4 (1997), 203–213. Google ScholarDigital Library
- Matt Kaufmann, J. Strother Moore, and Panagiotis Manolios. 2000. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell, MA, USA.Google ScholarDigital Library
- K. Korovin and C. Sticksel. 2010. iProver-Eq: An Instantiation-Based Theorem Prover with Equality. In IJCAR’10 (Lecture Notes in Computer Science), J. Giesl and R. Hähnle (Eds.), Vol. 6173. Springer, 196–202.Google Scholar
- Laura Kovács and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire. In CAV’13. 1–35. Google ScholarDigital Library
- Q. L. (Quang Loc) Le, M. Tatsuta, J. ( Jun) Sun, and W. N. (Wei-Ngan) Chin. 2017. A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. In CAV’17. http://hdl.handle.net/10149/621090Google Scholar
- K. Rustan M. Leino. 2012. Automating Induction with an SMT Solver. In VMCAI’12. 315–331. Google ScholarDigital Library
- Tal Lev-Ami, Neil Immerman, Thomas W. 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, 2 (2009). Google ScholarCross Ref
- Christof Löding, Parthasarathy Madhusudan, and Lucas Peña. 2017. Foundations for Natural Proofs and Quantifier Instantiation: Artifact. https://github.com/lucaspena/foundations- np- qi- artifcat . (2017).Google Scholar
- P. Madhusudan, Gennaro Parlato, and Xiaokang Qiu. 2011. Decidable logics combining heap structures and data. In POPL’11. 611–622. Google ScholarDigital Library
- P. Madhusudan and Xiaokang Qiu. 2011. Efficient Decision Procedures for Heaps Using STRAND. In SAS’11. 43–59. Google ScholarCross Ref
- Parthasarathy Madhusudan, Xiaokang Qiu, and Andrei Stefanescu. 2012. Recursive Proofs for Inductive Tree Data-structures. In POPL’12. 123–136. Google ScholarDigital Library
- Zohar Manna and John McCarthy. 1970. Properties of Programs and Partial Function Logic. Machine Intelligence 5 (1970), 79–98.Google Scholar
- The Coq development team. 2016. The Coq Proof Assistant Reference Manual. (2016). Version 8.6.Google Scholar
- Kenneth L. McMillan. 2003. Interpolation and SAT-Based Model Checking. In CAV’03. 1–13. Google ScholarCross Ref
- Yiannis N. Moschovakis. 2008. Elementary induction on abstract structures. Dover Publications.Google Scholar
- Charles Gregory Nelson. 1980. Techniques for Program Verification. Ph.D. Dissertation. Stanford, CA, USA. AAI8011683.Google Scholar
- Greg Nelson and Derek C. Oppen. 1979. Simplification by Cooperating Decision Procedures. ACM Trans. Program. Lang. Syst. 1, 2 (1979), 245–257. Google ScholarDigital Library
- Huu Hai Nguyen and Wei-Ngan Chin. 2008. Enhancing Program Verification with Lemmas. In CAV’08. 355–369. Google ScholarDigital Library
- Ulf Norell. 2009. Dependently Typed Programming in Agda. In TLDI’09. 1–2. Google ScholarDigital Library
- 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. Vol. 33. IOS Press, 286–318. Google ScholarCross Ref
- Derek C. Oppen. 1980. Complexity, Convexity and Combinations of Theories. Theor. Comput. Sci. 12 (1980), 291–302. Google ScholarCross Ref
- Sam Owre, John M. Rushby, and Natarajan Shankar. 1992. PVS: A Prototype Verification System. In CADE’11. 748–752. http://dl.acm.org/citation.cfm?id=648230.752639Google Scholar
- Oden Padon, Giuliano Losa, Mooly Sagiv, and Sharon Shoham. 2017. Paxos Made EPR: Decidable Reasoning about Distributed Protocols. In OOPSLA’17. To Appear.Google Scholar
- Lawrence C. Paulson. 1993. Isabelle: The Next 700 Theorem Provers. CoRR cs.LO/9301106 (1993). http://arxiv.org/abs/cs.LO/ 9301106Google Scholar
- Edgar Pek, Xiaokang Qiu, and Parthasarathy Madhusudan. 2014. Natural proofs for data structure manipulation in C using separation logic. In PLDI’14. 440–451. http://dl.acm.org/citation.cfm?id=2594291Google Scholar
- Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating Separation Logic Using SMT. In CAV’13. 773–789. Google ScholarDigital Library
- Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014. Automating Separation Logic with Trees and Data. In CAV’14. 711–728. Google ScholarDigital Library
- Xiaokang Qiu, Pranav Garg, Andrei Stefanescu, and Parthasarathy Madhusudan. 2013. Natural proofs for structure, data, and separation. In PLDI’13. ACM, 231–242. Google ScholarDigital Library
- Andrew Reynolds. 2016. Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. In Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop, Coimbra, Portugal, July 2, 2016. 1–15.Google Scholar
- John Alan Robinson. 1965. A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12, 1 (1965), 23–41. Google ScholarDigital Library
- Philipp Rümmer. 2012. E-Matching with Free Variables. In LPAR’12. 359–374. Google ScholarDigital Library
- Uwe Schöning. 2008. Logic for Computer Scientists. Birkhäuser. Google ScholarCross Ref
- Stephan Schulz. 2002. E - a brainiac theorem prover. AI Commun. 15, 2-3 (2002), 111–126. http://content.iospress.com/ articles/ai- communications/aic260Google Scholar
- Thoralf Skolem. 1934. Über die Nicht-charakterisierbarkeit der Zahlenreihe mittels endlich oder abzählbar unendlich vieler Aussagen mit ausschließlich Zahlenvariablen. Fundamenta Mathematica 1 (1934), 150–161. Google ScholarCross Ref
- Philippe Suter, Mirco Dotta, and Viktor Kuncak. 2010. Decision Procedures for Algebraic Data Types with Abstractions. In POPL’10. ACM, New York, NY, USA, 199–210. Google ScholarDigital Library
- Quang-Trung Ta, Ton Chanh Le, Siau-Cheng Khoo, and Wei-Ngan Chin. 2016. Automated Mutual Explicit Induction Proof in Separation Logic. CoRR abs/1609.00919 (2016). http://arxiv.org/abs/1609.00919Google Scholar
- Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. 2009. SPASS Version 3.5. In CADE’09. 140–145. Google ScholarDigital Library
Index Terms
- Foundations for natural proofs and quantifier instantiation
Recommendations
Foundations of Paraconsistent Resolution
An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness ...
Foundations of Paraconsistent Resolution
An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness ...
Soundness and Completeness Proofs by Coinductive Methods
We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an ...
Comments