Craig Interpolation in the Presence of Non-linear Constraints

DOI10.1007/978-3-642-24310-3_17zbMath1348.68141OpenAlexW207011911MaRDI QIDQ3172854

Bernd Becker, Stefan Kupferschmid

Publication date: 7 October 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-24310-3_17

zbMATH Keywords

interval arithmeticCraig interpolationSATSMTBMC

Mathematics Subject Classification ID

Related Items (5)

Interpolation and model checking for nonlinear arithmetic ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ Temporal Logic Verification for Delay Differential Equations ⋮ Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF ⋮ NIL: learning nonlinear interpolants

Uses Software

• BLAST
• FOCI

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The algorithmic analysis of hybrid systems
• A two-dimensional mapping with a strange attractor
• An interpolating theorem prover
• Efficient generation of craig interpolants in satisfiability modulo theories
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Automated Deduction – CADE-20
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Computer Aided Verification

This page was built for publication: Craig Interpolation in the Presence of Non-linear Constraints