Interpolants for Linear Arithmetic in SMT

DOI10.1007/978-3-540-88387-6_13MaRDI QIDQ3540071zbMATH OpenOpenAlexFDO

Authors

Publication date 20 November 2008

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-88387-6_13

Mathematics Subject Classification ID

Interpolation, preservation, definability (03C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Interpolation and model checking for nonlinear arithmetic
• Efficient interpolant generation in satisfiability modulo linear integer arithmetic
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Interpolation Properties and SAT-Based Model Checking
• Interpolation in fragments of classical linear logic
• Improving interpolants for linear arithmetic
• An SMT solver for non-linear real arithmetic inside maple
• Interpolation with decidable fixpoint logics
• Incomplete SMT techniques for solving non-linear formulas over the integers

Cites work

• Automated Deduction – CADE-20
• Constraint Solving for Interpolation
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Fourier-Motzkin elimination and its dual
• Interpolation and SAT-based model checking.
• Introduction to algorithms
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(6)

• Cutting the mix
• Preface: Special issue on interpolation
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Constraint solving for interpolation

Describes a project that uses

Uses Software

• BLAST
• FOCI
• Yices

This page was built for publication: Interpolants for Linear Arithmetic in SMT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3540071)