Interpolant Strength

DOI10.1007/978-3-642-11319-2_12zbMath1273.68225OpenAlexW2913808178WikidataQ62040465 ScholiaQ62040465MaRDI QIDQ3656880

Mitra Purandare, Vijay D'Silva, Daniel Kroening, Georg Weissenbacher

Publication date: 14 January 2010

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-11319-2_12

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Interpolation, preservation, definability (03C40)

Related Items (24)

Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Preface: Special issue on interpolation ⋮ Labelled interpolation systems for hyper-resolution, clausal, and local proofs ⋮ Proof tree preserving tree interpolation ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Lattice-based refinement in bounded model checking ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Interpolation and Model Checking ⋮ Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking ⋮ Incremental preprocessing methods for use in BMC ⋮ Resolution proof transformation for compression and interpolation ⋮ Farkas-based tree interpolation ⋮ On Interpolation in Decision Procedures ⋮ How to deal with unbelievable assertions ⋮ Exploiting partial variable assignment in interpolation-based model checking ⋮ Unnamed Item ⋮ Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys ⋮ Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Efficient generation of small interpolants in CNF ⋮ Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF ⋮ NIL: learning nonlinear interpolants ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic ⋮ On interpolation in automated theorem proving

This page was built for publication: Interpolant Strength