Interpolating quantifier-free Presburger arithmetic

DOI10.1007/978-3-642-16242-8_35MaRDI QIDQ4933327zbMATH OpenOpenAlexFDO

Authors Daniel Kroening, Jérôme Leroux, Philipp Rümmer

Publication date 12 October 2010

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-16242-8_35

Mathematics Subject Classification ID

Interpolation, preservation, definability (03C40) First-order arithmetic and fragments (03F30) Specification and verification (program logics, model checking, etc.) (68Q60) Polyhedral combinatorics, branch-and-bound, branch-and-cut (90C57)

Recommendations

• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Interpolant based decision procedure for quantifier-free Presburger arithmetic
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• An interpolating theorem prover

Cited in

(12)

• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Farkas-based tree interpolation
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• SAT-Based Model Checking
• Interpolation and model checking
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Articulations and Products of Transition Systems and their Applications to Petri Net Synthesis
• Mind the gap: bit-vector interpolation recast over linear integer arithmetic
• Computer Aided Verification
• Interpolant based decision procedure for quantifier-free Presburger arithmetic
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

Describes a project that uses

Uses Software

• OpenSMT
• CSIsat

This page was built for publication: Interpolating quantifier-free Presburger arithmetic

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