pith. sign in

arxiv: 2605.23022 · v1 · pith:FWVHGGPMnew · submitted 2026-05-21 · 💻 cs.LO · cs.PL

Complete first-order reasoning for functional programs

Adithya Murali , Lucas Pe\~na , Ranjit Jhala , P. Madhusudan This is my paper

Pith reviewed 2026-05-25 05:06 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords functional program verificationfirst-order logicalgebraic datatypesSMT solversrecursive functionscompletenesstheory combination
0
0 comments X

The pith

Unrolling recursive function definitions plus quantifier-free SMT reasoning is complete for first-order theories of algebraic datatypes combined with suitable background theories.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Verification tools for functional programs often unroll recursive definitions and then apply quantifier-free reasoning in an SMT solver. The paper shows that this heuristic generalizes to a complete procedure for deciding validity in the combined first-order theory of algebraic datatypes and background theories whose quantifier-free fragments are decidable. The completeness result explains both when the heuristic succeeds without help and when user-supplied lemmas become necessary to finish a proof.

Core claim

The technique of unrolling recursive function definitions followed by quantifier-free reasoning is complete for validity in the combined first-order theory of algebraic datatypes and any background theory that supports decidable quantifier-free reasoning.

What carries the argument

The unrolling procedure that reduces first-order validity over datatypes to a sequence of quantifier-free checks in the background theory.

Load-bearing premise

Background theories support decidable quantifier-free reasoning.

What would settle it

A formula that is valid in the combined theory but cannot be established by any finite number of unrollings followed by a quantifier-free check.

Figures

Figures reproduced from arXiv: 2605.23022 by Adithya Murali, Lucas Pe\~na, P. Madhusudan, Ranjit Jhala.

Figure 1
Figure 1. Figure 1: Rogue Nonstandard Model for Peano over the universe U ≡ {0, 1, 2, . . .} ∪ {. . . , −2 ′ , −1 ′ , 0 ′ , 1 ′ , 2 ′ , . . .}. comprising the naturals and a primed version of each integer. The model provides an interpretation for various constructors, destructors and plus that respects the ADT axioms, but where plus has a nonstandard interpretation on nonstandard ADT elements 𝑖 ′ : I (plus) (𝑖 ′ , Z) = (𝑖 + 1… view at source ↗
Figure 2
Figure 2. Figure 2: Proof of the commutativity of Peano addition: The explicit case-splitting, recursion and “lemma application” are needed to eliminate rogue nonstandard models. separately the cases where the argument is Z or S n. Second, the recursive call to zeroR n puts the post-condition of zeroR for the smaller input n as a hypothesis for the new VC defplus → (∀𝑛. plus(Z, Z) = Z ∧ plus(𝑛, Z) = 𝑛 → plus(S(𝑛), Z) = S(𝑛)) … view at source ↗
Figure 3
Figure 3. Figure 3: Implementations of get and set functions for Binary Search Tree. verifying more complicated properties. Consider the datatype of finite maps from keys (k) to values (v) data Map k v = Leaf | Node k v (Map k v) (Map k v) [PITH_FULL_IMAGE:figures/full_fig_p027_3.png] view at source ↗
read the original abstract

Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact complete for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explains why they fail when they fail, and the precise role that user help plays in making proofs succeed.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims that the unrolling heuristic employed by tools such as Liquid Haskell and Leon can be generalized and formalized into a complete procedure for deciding validity in the combined first-order theory of algebraic datatypes together with background theories that admit decidable quantifier-free reasoning; the development explains the heuristic's successes, its failures, and the precise contribution of user-provided assistance.

Significance. If the completeness result is established with a correct reduction to quantifier-free reasoning, the work supplies a theoretical account of why practical unrolling-based verifiers succeed when they do and clarifies the boundary conditions under which they are guaranteed to terminate, which would be a useful bridge between heuristic practice and complete FO reasoning in the ADT setting.

major comments (1)
  1. [Abstract] Abstract (paragraph 2): the central completeness claim for the combined theory is asserted without an explicit theorem statement, proof sketch, or reduction argument; because this is the load-bearing result, the manuscript must supply at least an outline of how unrolling interacts with the decidable QF fragment and how mutual recursion or non-free constructors are handled.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful review and constructive feedback. We address the single major comment below and will revise the manuscript to strengthen the presentation of the central result.

read point-by-point responses

  1. Referee: [Abstract] Abstract (paragraph 2): the central completeness claim for the combined theory is asserted without an explicit theorem statement, proof sketch, or reduction argument; because this is the load-bearing result, the manuscript must supply at least an outline of how unrolling interacts with the decidable QF fragment and how mutual recursion or non-free constructors are handled.

    Authors: We agree that the abstract would benefit from greater explicitness. In the revised version we will insert a direct reference to the main completeness theorem (Theorem 4.1) together with a one-sentence outline: unrolling is performed until every recursive call has been eliminated, yielding a quantifier-free formula whose validity is then decided by the background theory; mutual recursion is handled by simultaneous unrolling of all mutually recursive definitions, and non-free constructors are accommodated by the standard axioms of the algebraic-datatype theory. The full reduction argument and termination proof remain in Section 4; only the abstract is augmented. revision: yes

Circularity Check

0 steps flagged

No circularity: completeness claim is a standalone theoretical result

full rationale

The provided abstract and context present a completeness theorem for a formalized version of an existing unrolling heuristic in the combined theory of algebraic datatypes and background theories (under the decidable QF assumption). No equations, fitted parameters, self-citations, or ansatzes are exhibited that reduce the claimed completeness to the input heuristic by construction. The derivation chain is therefore self-contained as a standard proof of completeness rather than a renaming or re-derivation of its own premises.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only abstract available; no explicit free parameters, axioms, or invented entities are stated.

pith-pipeline@v0.9.0 · 5639 in / 1067 out tokens · 22209 ms · 2026-05-25T05:06:40.509400+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

96 extracted references · 96 canonical work pages

  1. [1]

    Rustan M

    Nada Amin, K. Rustan M. Leino, and Tiark Rompf. 2014. Computing with an SMT Solver. InTests and Proofs, Martina Seidl and Nikolai Tillmann (Eds.). Springer International Publishing, Cham, 20–35

    work page 2014

  2. [2]

    Franz Baader and Silvio Ghilardi. 2005. Connecting Many-Sorted Theories. InAutomated Deduction – CADE-20, Robert Nieuwenhuis (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 278–294

    work page 2005

  3. [3]

    Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, and Thomas Wies. 2015. Deciding Local Theory Extensions via E-matching. InComputer Aided Verification, Daniel Kroening and Corina S. P ˘as˘areanu (Eds.). Springer International Publishing, Cham, 87–105

    work page 2015

  4. [4]

    Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´c, Tim King, Andrew Reynolds, and Cesare Tinelli

    Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´c, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. InComputer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 171–177

    work page 2011

  5. [5]

    Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´c, Tim King, Andrew Reynolds, and Cesare Tinelli

    Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´c, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. InProceedings of the 23rd International Conference on Computer Aided Verification(Snowbird, UT)(CAV’11). Springer-Verlag, Berlin, Heidelberg, 171–177

    work page 2011

  6. [6]

    1977.Handbook of Mathematical Logic

    Jon Barwise. 1977.Handbook of Mathematical Logic. North-Holland Publishing Company, Amsterdam

    work page 1977

  7. [7]

    Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Symbolic Execution with Separation Logic. InProceedings of the Third Asian Conference on Programming Languages and Systems (APLAS’05). 52–68

    work page 2005

  8. [8]

    1999.Integrating Decision Procedures for Temporal Verification

    Nikolaj Skallerud Bjorner. 1999.Integrating Decision Procedures for Temporal Verification. Ph. D. Dissertation. Stanford University, Stanford, CA, USA. Advisor(s) Manna, Zohar. AAI9924398

    work page 1999

  9. [9]

    R´egis Blanc, Viktor Kuncak, Etienne Kneuss, and Philippe Suter. 2013. An Overview of the Leon Verification System: Verification by Translation to Recursive Functions. InProceedings of the 4th Workshop on Scala (Montpellier, France)(SCALA ’13). Association for Computing Machinery, New York, NY, USA, Article 1, 10 pages. doi:10.1145/2489837.2489838

    work page doi:10.1145/2489837.2489838 2013

  10. [10]

    Jasmin Christian Blanchette and Koen Claessen. 2010. Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models. InLogic for Programming, Artificial Intelligence, and Reasoning, Christian G. Ferm¨ uller and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 127–141

    work page 2010

  11. [11]

    Franc ¸ois Bobot, Jean-Christophe Filliˆatre, Claude March´e, and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. InBoogie 2011: First International Workshop on Intermediate Verification Languages. HAL-Inria, Wroclaw, Poland, 53–64. https://hal.inria.fr/hal-00790310

    work page 2011

  12. [12]

    Franc ¸ois Bobot, Jean-Christophe Filliˆatre, Claude March´e, and Andrei Paskevich. 2015. Let’s Verify This with Why3.International Journal on Software Tools for Technology Transfer (STTT)17, 6 (2015), 709–727. doi:10.1007/s10009-014-0314-5 See also http://toccata.lri.fr/gallery/fm2012comp.en.html

    work page doi:10.1007/s10009-014-0314-5 2015

  13. [13]

    Boyer and J

    Robert S. Boyer and J. Strother Moore. 1988.A Computational Logic Handbook. Academic Press Professional, Inc., USA

    work page 1988

  14. [14]

    Bradley and Zohar Manna

    Aaron R. Bradley and Zohar Manna. 2007.The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, Berlin, Heidelberg

    work page 2007

  15. [15]

    Bradley, Zohar Manna, and Henny B

    Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What’s Decidable About Arrays?. InVerification, Model Checking, and Abstract Interpretation, E. Allen Emerson and Kedar S. Namjoshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 427–442

    work page 2006

  16. [16]

    Harsh Raju Chamarthi, Peter Dillinger, Panagiotis Manolios, and Daron Vroon. 2011. The ACL2 Sedan Theorem Proving System. InProceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Part of the Joint European Conferences on Theory and Practice of Software(Saarbr¨ ucken, Germany)(TACAS’11/ETAPS’1...

    work page 2011

  17. [17]

    Koen Claessen, Moa Johansson, Dan Ros´en, and Nicholas Smallbone. 2013. Automating Inductive Proofs Using Theory Exploration. InAutomated Deduction – CADE-24, Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 392–406

    work page 2013

  18. [18]

    Simon Cruanes. 2017. Superposition with Structural Induction. InFrontiers of Combining Systems, Clare Dixon and Marcelo Finger (Eds.). Springer International Publishing, Cham, 172–188

    work page 2017

  19. [19]

    The dafny-lang community. 2022. https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef 44 Adithya Murali, Lucas Pe ˜na, Ranjit Jhala, and P. Madhusudan

    work page 2022

  20. [20]

    Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. 2018. Solving Horn Clauses on Inductive Data Types Without Induction.Theory and Practice of Logic Programming18, 3-4 (2018), 452–469. doi:10.1017/S1471068418000157

    work page doi:10.1017/s1471068418000157 2018

  21. [21]

    Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. InProceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(Budapest, Hungary)(TACAS’08). Springer-Verlag, Berlin, Heidelberg, 337–340

    work page 2008

  22. [22]

    Leonardo de Moura and Nikolaj Bjørner. 2009. Generalized, efficient array decision procedures. In2009 Formal Methods in Computer-Aided Design. IEEE, 45–52. doi:10.1109/FMCAD.2009.5351142

    work page doi:10.1109/fmcad.2009.5351142 2009

  23. [23]

    David Detlefs, Greg Nelson, and James B. Saxe. 2005. Simplify: A Theorem Prover for Program Checking.J. ACM52, 3 (May 2005), 365–473. doi:10.1145/1066100.1066102

    work page doi:10.1145/1066100.1066102 2005

  24. [24]

    Neta Elad, Adithya Murali, and Sharon Shoham. 2026. Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof Mechanisms for Separation Logic with Inductive Definitions.Proc. ACM Program. Lang.10, POPL, Article 29 (Jan. 2026), 32 pages. doi:10.1145/3776671

    work page doi:10.1145/3776671 2026

  25. [25]

    Neta Elad, Oded Padon, and Sharon Shoham. 2024. An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification.Proc. ACM Program. Lang.8, POPL, Article 33 (Jan. 2024), 31 pages. doi:10.1145/3632875

    work page doi:10.1145/3632875 2024

  26. [26]

    Neta Elad and Sharon Shoham. 2025. Axe ’Em: Eliminating Spurious States with Induction Axioms.Proc. ACM Program. Lang.9, POPL, Article 17 (Jan. 2025), 30 pages. doi:10.1145/3704853

    work page doi:10.1145/3704853 2025

  27. [27]

    Enderton

    Herbert B. Enderton. 1972.A mathematical introduction to logic. Academic Press, New York

    work page 1972

  28. [28]

    Jean-Christophe Filliˆatre and Andrei Paskevich. 2013. Why3 — Where Programs Meet Provers. InProgramming Languages and Systems, Matthias Felleisen and Philippa Gardner (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 125–128

    work page 2013

  29. [29]

    Pascal Fontaine. 2007. Combinations of Theories and the Bernays-Sch ¨onfinkel-Ramsey Class. In4th Interna- tional Verification Workshop - VERIFY’07 (CEUR Workshop Proceedings, Vol. 259), Bernhard Beckert (Ed.). HAL-Inria, Bremen, Germany, 37–54. https://hal.inria.fr/inria-00186639 URL : http://sunsite.informatik.rwth- aachen.de/Publications/CEUR-WS/Vol-25...

    work page 2007

  30. [30]

    Rui Ge, Ronald Garcia, and Alexander J. Summers. 2024. A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations. InAutomated Reasoning, Christoph Benzm¨ uller, Marijn J.H. Heule, and Renate A. Schmidt (Eds.). Springer Nature Switzerland, Cham, 419–438

    work page 2024

  31. [31]

    Yeting Ge and Leonardo de Moura. 2009. Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories. InComputer Aided Verification, Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 306–320

    work page 2009

  32. [32]

    Silvio Ghilardi. 2004. Model-Theoretic Methods in Combined Constraint Satisfiability.Journal of Automated Reasoning33, 3 (01 Oct 2004), 221–249. doi:10.1007/s10817-004-6241-5

    work page doi:10.1007/s10817-004-6241-5 2004

  33. [33]

    P. C. Gilmore. 1960. A proof method for quantification theory: its justification and realization.IBM J. Res. Dev.4, 1 (Jan. 1960), 28–35. doi:10.1147/rd.41.0028

    work page doi:10.1147/rd.41.0028 1960

  34. [34]

    Fajar Haifani, Sophie Tourret, and Christoph Weidenbach. 2021. Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance. InAutomated Deduction – CADE 28, Andr´e Platzer and Geoff Sutcliffe (Eds.). Springer International Publishing, Cham, 327–343

    work page 2021

  35. [35]

    M´arton Hajd´ u, Petra Hozzov´a, Laura Kov´acs, Johannes Schoisswohl, and Andrei Voronkov. 2020. Induction with Generalization in Superposition Reasoning. InIntelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings(Bertinoro, Italy). Springer-Verlag, Berlin, Heidelberg, 123–137. doi:10.1007...

    work page doi:10.1007/978-3-030-53518-6 2020

  36. [36]

    M´arton Hajd´ u, Petra Hozzov´a, Laura Kov´acs, and Andrei Voronkov. 2021. Induction with Recursive Definitions in Superposition. InProceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021. TU Wien Academic Press, Wien, 246–255. doi:10.34727/2021/isbn.978-3-85448-046-4 34

    work page doi:10.34727/2021/isbn.978-3-85448-046-4 2021

  37. [37]

    Jad Hamza, Nicolas Voirol, and Viktor Kun ˇcak. 2019. System FR: Formalized Foundations for the Stainless Verifier.Proc. ACM Program. Lang.3, OOPSLA, Article 166 (oct 2019), 30 pages. doi:10.1145/3360592

    work page doi:10.1145/3360592 2019

  38. [38]

    1997.A Shorter Model Theory

    Wilfrid Hodges. 1997.A Shorter Model Theory. Cambridge University Press, USA

    work page 1997

  39. [39]

    Hossein Hojjat and Philipp R¨ ummer. 2017. Deciding and Interpolating Algebraic Data Types by Reduction. In19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, September 21-24, 2017, Tudor Jebelean, Viorel Negru, Dana Petcu, Daniela Zaharie, Tetsuo Ida, and Stephen M. Watt (Eds.). IEEE ...

    work page doi:10.1109/synasc.2017.00033 2017

  40. [40]

    Hopcroft, Rajeev Motwani, and Jeffrey D

    John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. 2006.Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., USA

    work page 2006

  41. [41]

    Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans. 2008. On Local Reasoning in Verification. InTools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 265–281

    work page 2008

  42. [42]

    Radu Iosif, Adam Rogalewicz, and Jiri Simacek. 2013. The Tree Width of Separation Logic with Recursive Definitions. InAutomated Deduction – CADE-24, Maria Paola Bonacina (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 21–38

    work page 2013

  43. [43]

    Andrew Ireland and Alan Bundy. 1996. Productive Use of Failure in Inductive Proof. InAutomated Mathematical Induction, Hantao Zhang (Ed.). Springer Netherlands, Dordrecht, 79–111. doi:10.1007/978-94-009-1675-3 3

    work page doi:10.1007/978-94-009-1675-3 1996

  44. [44]

    Moa Johansson, Lucas Dixon, and Alan Bundy. 2010. Case-Analysis for Rippling and Inductive Proof. In Proceedings of the First International Conference on Interactive Theorem Proving(Edinburgh, UK)(ITP’10). Springer-Verlag, Berlin, Heidelberg, 291–306. https://doi.org/10.1007/978-3-642-14052-5 21

    work page doi:10.1007/978-3-642-14052-5 2010

  45. [45]

    Deepak Kapur, Rupak Majumdar, and Calogero G. Zarba. 2006. Interpolation for Data Structures. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (Portland, Oregon, USA)(SIGSOFT ’06/FSE-14). Association for Computing Machinery, New York, NY, USA, 105–116. doi:10.1145/1181775.1181789

    work page doi:10.1145/1181775.1181789 2006

  46. [46]

    Strother Moore, and Panagiotis Manolios

    Matt Kaufmann, J. Strother Moore, and Panagiotis Manolios. 2000.Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, USA

    work page 2000

  47. [47]

    Laura Kov´acs, Simon Robillard, and Andrei Voronkov. 2017. Coming to Terms with Quantified Reasoning. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages(Paris, France) (POPL ’17). ACM, New York, NY, USA, 260–270. doi:10.1145/3009837.3009887

    work page doi:10.1145/3009837.3009887 2017

  48. [48]

    Laura Kov´acs and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire. InComputer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–35

    work page 2013

  49. [49]

    Sava Krstic, Amit Goel, Jim Grundy, and Cesare Tinelli. 2007. Combined Satisfiability modulo Parametric Theories. InProceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(Braga, Portugal)(TACAS’07). Springer-Verlag, Berlin, Heidelberg, 602–617

    work page 2007

  50. [50]

    Rustan M

    K. Rustan M. Leino. 2008. This is Boogie 2. (June 2008). https://www.microsoft.com/en-us/research/ publication/this-is-boogie-2-2/ Technical Report

    work page 2008

  51. [51]

    Rustan M

    K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. InProceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning(Dakar, Senegal)(LPAR’10). Springer-Verlag, Berlin, Heidelberg, 348–370. doi:10.5555/1939141.1939161

    work page doi:10.5555/1939141.1939161 2010

  52. [52]

    K. R. M. Leino and Cl´ement Pit-Claudel. 2016. Trigger Selection Strategies to Stabilize Program Verifiers. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham, 361–381

    work page 2016

  53. [53]

    Rustan Leino and Nadia Polikarpova. 2013. Verified Calculations. https://www.microsoft.com/en-us/research/ publication/verified-calculations/

    work page 2013

  54. [54]

    Madhusudan, and Lucas Pe ˜na

    Christof L ¨oding, P. Madhusudan, and Lucas Pe ˜na. 2018. Foundations for natural proofs and quantifier instantiation.PACMPL2, POPL (2018), 10:1–10:30. doi:10.1145/3158098

    work page doi:10.1145/3158098 2018

  55. [55]

    A. I. Mal’tsev. 1962. Axiomatizable classes of locally free algebras of certain types.Sibirsk. Mat. Zh.3 (1962), 729–743. Issue 5

    work page 1962

  56. [56]

    Sipma, and Ting Zhang

    Zohar Manna, Henny B. Sipma, and Ting Zhang. 2007. Verifying Balanced Trees. InLogical Foundations of Computer Science, Sergei N. Artemov and Anil Nerode (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 363–378

    work page 2007

  57. [57]

    Matiyasevich

    Yuri V. Matiyasevich. 1993.Hilbert’s Tenth Problem. MIT Press, Cambridge, MA, USA

    work page 1993

  58. [58]

    Micha l Moskal. 2009. Programming with Triggers. InProceedings of the 7th International Workshop on Satisfiability Modulo Theories(Montreal, Canada)(SMT ’09). Association for Computing Machinery, New York, NY, USA, 20–29. doi:10.1145/1670412.1670416

    work page doi:10.1145/1670412.1670416 2009

  59. [59]

    Madhusudan

    Adithya Murali, Hrishikesh Balakrishnan, Aaron Councilman, and P. Madhusudan. 2025. FO-Complete Program Verification for Heap Logics.Proc. ACM Program. Lang.9, OOPSLA1, Article 106 (April 2025), 29 pages. doi:10.1145/3720447

    work page doi:10.1145/3720447 2025

  60. [60]

    Madhusudan

    Adithya Murali, Lucas Pe˜na, Eion Blanchard, Christof L ¨oding, and P. Madhusudan. 2022. Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints.Proc. ACM Program. Lang.6, OOPSLA2, 46 Adithya Murali, Lucas Pe ˜na, Ranjit Jhala, and P. Madhusudan Article 191 (oct 2022), 30 pages. doi:10.1145/3563354

    work page doi:10.1145/3563354 2022

  61. [61]

    Madhusudan

    Adithya Murali, Lucas Pe˜na, Ranjit Jhala, and P. Madhusudan. 2023. Complete First-Order Reasoning for Properties of Functional Programs.Proc. ACM Program. Lang.7, OOPSLA2, Article 259 (oct 2023), 30 pages. doi:10.1145/3622835

    work page doi:10.1145/3622835 2023

  62. [62]

    1980.Techniques for Program Verification

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

    work page 1980

  63. [63]

    Greg Nelson and Derek C. Oppen. 1979. Simplification by Cooperating Decision Procedures.ACM Trans. Program. Lang. Syst.1, 2 (oct 1979), 245–257. doi:10.1145/357073.357079

    work page doi:10.1145/357073.357079 1979

  64. [64]

    O’Hearn, Hongseok Yang, and John C

    Peter W. O’Hearn, Hongseok Yang, and John C. Reynolds. 2004. Separation and Information Hiding. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Venice, Italy)(POPL ’04). ACM, New York, NY, USA, 268–280. doi:10.1145/964001.964024

    work page doi:10.1145/964001.964024 2004

  65. [65]

    Grant Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, and Nicola Mometto. 2020. The Imandra Automated Reasoning System (System Description). InAutomated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing, Cham, 464–471

    work page 2020

  66. [66]

    Madhusudan

    Edgar Pek, Xiaokang Qiu, and P. Madhusudan. 2014. Natural Proofs for Data Structure Manipulation in C Using Separation Logic. InProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation(Edinburgh, United Kingdom)(PLDI ’14). ACM, New York, NY, USA, 440–451. doi:10.1145/2594291.2594325

    work page doi:10.1145/2594291.2594325 2014

  67. [67]

    Tuan-Hung Pham and Michael W. Whalen. 2013. RADA: A Tool for Reasoning about Algebraic Data Types with Abstractions. InProceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (Saint Petersburg, Russia)(ESEC/FSE 2013). Association for Computing Machinery, New York, NY, USA, 611–614. doi:10.1145/2491411.2494597

    work page doi:10.1145/2491411.2494597 2013

  68. [68]

    Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2013. Automating Separation Logic Using SMT. In Proceedings of the 25th International Conference on Computer Aided Verification(Saint Petersburg, Russia) (CAV’13). Springer-Verlag, Berlin, Heidelberg, 773–789. doi:10.1007/978-3-642-39799-8 54

    work page doi:10.1007/978-3-642-39799-8 2013

  69. [69]

    Moj˙ zesz Presburger and Dale Jabcquette. 1991. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation.History and Philosophy of Logic12, 2 (1991), 225–233. arXiv:https://doi.org/10.1080/014453409108837187 doi:10.1080/014453409108837187

    work page doi:10.1080/014453409108837187 1991

  70. [70]

    Madhusudan

    Xiaokang Qiu, Pranav Garg, Andrei S ¸tef˘anescu, and P. Madhusudan. 2013. Natural Proofs for Structure, Data, and Separation. InProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation(Seattle, Washington, USA)(PLDI ’13). ACM, New York, NY, USA, 231–242. doi:10.1145/2491956.2462169

    work page doi:10.1145/2491956.2462169 2013

  71. [71]

    Giles Reger, Martin Suda, and Andrei Voronkov. 2017. Instantiation and pretending to be an SMT solver with V AMPIRE.CEUR Workshop Proceedings1889 (1 Jan. 2017), 63–75. 15th International Workshop on Satisfiability Modulo Theories, SMT 2017 ; Conference date: 22-07-2017 Through 23-07-2017

    work page 2017

  72. [72]

    Andrew Reynolds. 2017. Conflicts, Models and Heuristics for Quantifier Instantiation in SMT. InVampire

    work page 2017

  73. [73]

    44), Laura Kovacs and Andrei Voronkov (Eds.)

    Proceedings of the 3rd Vampire Workshop (EPiC Series in Computing, Vol. 44), Laura Kovacs and Andrei Voronkov (Eds.). EasyChair, Portugal, 1–15. doi:10.29007/jmd3

    work page doi:10.29007/jmd3

  74. [74]

    Andrew Reynolds and Jasmin Christian Blanchette. 2017. A Decision Procedure for (Co)Datatypes in SMT Solvers.J. Autom. Reason.58, 3 (mar 2017), 341–362. doi:10.1007/s10817-016-9372-6

    work page doi:10.1007/s10817-016-9372-6 2017

  75. [75]

    Andrew Reynolds and Viktor Kuncak. 2015. Induction for SMT Solvers. InVerification, Model Checking, and Abstract Interpretation, Deepak D’Souza, Akash Lal, and Kim Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 80–98

    work page 2015

  76. [76]

    Reynolds

    John C. Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. InProceedings of the ACM Annual Conference - Volume 2(Boston, Massachusetts, USA)(ACM ’72). Association for Computing Machinery, New York, NY, USA, 717–740. doi:10.1145/800194.805852

    work page doi:10.1145/800194.805852 1972

  77. [77]

    Rondon, Ming Kawaguci, and Ranjit Jhala

    Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types.SIGPLAN Not.43, 6 (jun 2008), 159–169. doi:10.1145/1379022.1375602

    work page doi:10.1145/1379022.1375602 2008

  78. [78]

    Philipp R¨ ummer. 2012. E-Matching with Free Variables. InLogic for Programming, Artificial Intelligence, and Reasoning, Nikolaj Bjørner and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 359–374

    work page 2012

  79. [79]

    Rybina and A

    T. Rybina and A. Voronkov. 2001. A Decision Procedure for Term Algebras with Queues.ACM Trans. Comput. Logic2, 2 (apr 2001), 155–181. doi:10.1145/371316.371494 Complete first-order reasoning for functional programs 47

    work page doi:10.1145/371316.371494 2001

  80. [80]

    Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Sorin Lerner, and Todd Millstein. 2022. Data-Driven Lemma Synthesis for Interactive Proofs.Proc. ACM Program. Lang.6, OOPSLA2, Article 143 (oct 2022), 27 pages. doi:10.1145/3563306

    work page doi:10.1145/3563306 2022

Showing first 80 references.