Flexible proof production in an industrial-strength SMT solver
From MaRDI portal
Publication:2104495
Cites work
- A mathematical introduction to logic.
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A verified implementation of algebraic numbers in Isabelle/HOL
- Algebraic numbers in Isabelle/HOL
- Construction of real algebraic numbers in Coq
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
- DRAT-based bit-vector proofs in CVC4
- DRAT-trim
- Efficient certified RAT verification
- Efficient verified (UN)SAT certificate checking
- Exploiting symmetry in SMT problems
- Extended resolution simulates \({\mathsf{DRAT}}\)
- Extending Sledgehammer with SMT solvers
- Fast LCF-Style Proof Reconstruction for Z3
- Fine grained SMT proofs for the theory of fixed-width bit-vectors
- High-level abstractions for simplifying extended string constraints in SMT
- scientific article; zbMATH DE number 1234104 (Why is no real title available?)
- scientific article; zbMATH DE number 2110621 (Why is no real title available?)
- scientific article; zbMATH DE number 7178358 (Why is no real title available?)
- Implementing the cylindrical algebraic decomposition within the Coq system
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Satisfiability modulo theories
- Satisfiability modulo transcendental functions via incremental linearization
- Scalable fine-grained proofs for formula processing
- Scaling up DPLL(T) string solvers using context-dependent simplification
- SMT proof checking using a logical framework
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- The Lean 4 theorem prover and programming language
- The MathSAT5 SMT solver
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(16)- Towards bit-width-independent proofs in SMT solvers
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Levelwise construction of a single cylindrical algebraic cell
- Verified verifying: SMT-LIB for strings in Isabelle
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
- A resolution-based interactive proof system for UNSAT
- Reconstruction of SMT proofs with Lambdapi
- Certainty in formalising SMT-LIB for strings in Isabelle
- Proof-carrying neuro-symbolic code
- Satisfiability of non-linear transcendental arithmetic as a certificate search problem
- Satisfiability modulo user propagators
- Certifying phase abstraction
- A resolution-based interactive proof system for UNSAT
- A certified proof checker for deep neural network verification in imandra
- Improving the SMT proof reconstruction pipeline in Isabelle/HOL
Describes a project that uses
Uses Software
This page was built for publication: Flexible proof production in an industrial-strength SMT solver
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104495)
