Conference proceeding
Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.216-230
ACM Conferences
CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs
01/08/2026
DOI: 10.1145/3779031.3779111
Abstract
Determining the satisfiability of formulas involving nonlinear real arithmetic and transcendental functions is necessary in many applications, such as formally verifying dynamic systems. Doing this automatically generally requires costly and intricate methods, which limits their applicability. In the context of SMT solving, Incremental Linearization was introduced recently to facilitate reasoning on this domain, via an incomplete but easy to implement and highly effective approach. The approach, based on abstraction-refinement via an incremental axiomatization of the nonlinear and transcendental operators, is currently implemented in the SMT solvers MathSAT and cvc5. The cvc5 implementation is also proof-producing. This paper presents two contributions: a formalization in the Lean proof assistant of the proof calculus employed by cvc5, and an extension of the lean-smt plugin to reconstruct the proofs produced by cvc5 using this proof calculus. These contributions ensure the soundness of the proof calculus, making the underlying algorithm more trustworthy. Moreover, they allow users to check cvc5 results obtained via incremental linearization, as well as improve Lean’s automation for problems in nonlinear arithmetic. We discuss how we modeled the rules in the proof assistant and the challenges encountered while formalizing them, as well as the issues in reconstructing proofs involving these rules in Lean, and how we solved them.
Details
- Title: Subtitle
- Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions
- Creators
- Tomaz Mascarenhas - Universidade Federal de Minas GeraisHarun Khan - Stanford UniversityAbdalrhman Mohamed - Stanford UniversityAndrew Reynolds - University of IowaHaniel Barbosa - Universidade Federal de Minas GeraisClark Barrett - Stanford UniversityCesare Tinelli - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.216-230
- Conference
- CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs
- Series
- ACM Conferences
- DOI
- 10.1145/3779031.3779111
- Publisher
- ACM
- Grant note
- Coordenacao de Aperfeicoamento de Pessoal de Nivel Superior - Brasil (CAPES): 001 Defense Advanced Research Projects Agency (DARPA): FA8750-24-2-1001
This work was partially supported by a gift from Amazon Web Services, the Stanford Center for Automated Reasoning, the Coordenacao de Aperfeicoamento de Pessoal de Nivel Superior - Brasil (CAPES) - Finance Code 001, and the Defense Advanced Research Projects Agency (DARPA) under contract FA8750-24-2-1001 (https://www.darpa.mil/research/programs/pipelined-reasoning-of-verifiers-enabling-robustsystems).Any opinions, findings, and conclusions or recommendations expressed here are those of the authors and do not necessarily reflect the views of DARPA.
- Language
- English
- Date published
- 01/08/2026
- Academic Unit
- Computer Science
- Record Identifier
- 9985116910302771
Metrics
13 Record Views