Efficient Interpolant Generation in Satisfiability Modulo Theories
From MaRDI portal
Publication:5458340
DOI10.1007/978-3-540-78800-3_30zbMATH Open1134.68402OpenAlexW1499948164WikidataQ62041289 ScholiaQ62041289MaRDI QIDQ5458340FDOQ5458340
Authors: Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani 
Publication date: 11 April 2008
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-78800-3_30
Recommendations
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Efficient interpolant generation in satisfiability modulo linear integer arithmetic
- Interpolant Generation for UTVPI
- Improving interpolants for linear arithmetic
Cites Work
- M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
- Linear programming. Foundations and extensions
- Lazy satisfiability modulo theories
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- Interpolation and SAT-based model checking.
- An interpolating theorem prover
- Abstractions from proofs
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Automated Deduction – CADE-20
- Array Abstractions from Proofs
- Constraint Solving for Interpolation
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- Computer Aided Verification
- Lazy Abstraction with Interpolants
- Tools and Algorithms for the Construction and Analysis of Systems
- Fast and Flexible Difference Constraint Propagation for DPLL(T)
- Verifying industrial hybrid systems with \textsc{MathSAT}
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- Efficient theory combination via Boolean search
- Interpolant learning and reuse in SAT-based model checking
- Fast congruence closure and extensions
- Tools and Algorithms for the Construction and Analysis of Systems
- Zap: Automated Theorem Proving for Software Analysis
Cited In (29)
- Challenges in Constraint-Based Analysis of Hybrid Systems
- Mind the gap: bit-vector interpolation recast over linear integer arithmetic
- Interpolation and model checking for nonlinear arithmetic
- Resolution proof transformation for compression and interpolation
- Configurable verification of timed automata with discrete variables
- Interpolant Generation for UTVPI
- Ground Interpolation for Combined Theories
- Interpolation and Symbol Elimination
- Proof tree preserving tree interpolation
- Interpolant synthesis for quadratic polynomial inequalities and combination with EUF
- Quantifier-free interpolation in combinations of equality interpolating theories
- Efficient Interpolant Generation in Satisfiability Modulo Theories
- NIL: learning nonlinear interpolants
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Efficient interpolant generation in satisfiability modulo linear integer arithmetic
- Constraint solving for interpolation
- Interpolation and symbol elimination in Vampire
- On interpolation in decision procedures
- Proof tree preserving interpolation
- Efficient generation of Craig interpolants in satisfiability modulo theories
- Satisfiability modulo theories
- Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
- Generalized Craig interpolation for stochastic satisfiability modulo theory problems
- Improving interpolants for linear arithmetic
- Efficient Generation of Small Interpolants in CNF
- Interpolants for Linear Arithmetic in SMT
- Interpolant learning and reuse in SAT-based model checking
- Ground Interpolation for the Theory of Equality
- Interpolation-based GR(1) assumptions refinement
Uses Software
This page was built for publication: Efficient Interpolant Generation in Satisfiability Modulo Theories
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5458340)
