Efficient interpolant generation in satisfiability modulo linear integer arithmetic

DOI10.2168/LMCS-8(3:3)2012MaRDI QIDQ5891705zbMATH OpenFDO

Authors Alberto Griggio, Thi Thieu Hoa Le, Roberto Sebastiani

Publication date 15 August 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/LMCS-8(3:3)2012

zbMATH Keywords

Craig interpolationdecision procedureinterpolant generationinterpolation algorithmlinear arithmetic over the integersmodel checkingSMT

Mathematics Subject Classification ID

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

Recommendations

• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Improving interpolants for linear arithmetic
• Interpolant Generation for UTVPI

Cited in

(10)

• Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
• A practical approach to satisfiability modulo linear integer arithmetic
• Efficient Generation of Small Interpolants in CNF
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Improving interpolants for linear arithmetic
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Interpolants for Linear Arithmetic in SMT
• Interpolant Generation for UTVPI
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

Describes a project that uses

Uses Software

• Princess
• FOCI

This page was built for publication: Efficient interpolant generation in satisfiability modulo linear integer arithmetic

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