Craig interpolation in the presence of non-linear constraints

DOI10.1007/978-3-642-24310-3_17MaRDI QIDQ3172854zbMATH OpenOpenAlexFDO

Authors Stefan Kupferschmid, Bernd Becker

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

SATinterval arithmeticSMTCraig interpolationBMC

Mathematics Subject Classification ID

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

Recommendations

• Interpolants in nonlinear theories over the reals
• Nonlinear Craig interpolant generation
• Computer Science Logic
• Applications and Theory of Petri Nets 2005
• scientific article; zbMATH DE number 2090854

Cites work

• scientific article; zbMATH DE number 3837022 (Why is no real title available?)
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A two-dimensional mapping with a strange attractor
• An interpolating theorem prover
• Automated Deduction – CADE-20
• Efficient generation of Craig interpolants in satisfiability modulo theories
• Interpolation and SAT-based model checking.
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Lower bounds for resolution and cutting plane proofs and monotone computations
• The algorithmic analysis of hybrid systems

Cited in

(9)

• Interpolation and model checking for nonlinear arithmetic
• scientific article; zbMATH DE number 1543346 (Why is no real title available?)
• Invariant checking of NRA transition systems via incremental reduction to LRA with EUF
• scientific article; zbMATH DE number 2090854 (Why is no real title available?)
• NIL: learning nonlinear interpolants
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Nonlinear Craig interpolant generation
• Interpolants in nonlinear theories over the reals
• Temporal logic verification for delay differential equations

Describes a project that uses

Uses Software

• FOCI
• BLAST

This page was built for publication: Craig interpolation in the presence of non-linear constraints

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