Interpolant Strength
From MaRDI portal
Publication:3656880
DOI10.1007/978-3-642-11319-2_12zbMath1273.68225WikidataQ62040465 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
68Q60: Specification and verification (program logics, model checking, etc.)
03B35: Mechanization of proofs and logical operations
03C40: Interpolation, preservation, definability
Related Items
Unnamed Item, Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference, Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking, 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, Guiding Craig interpolation with domain-specific abstractions, Incremental preprocessing methods for use in BMC, Resolution proof transformation for compression and interpolation, How to deal with unbelievable assertions, Efficient generation of small interpolants in CNF, Lattice-based refinement in bounded model checking, Exploiting partial variable assignment in interpolation-based model checking, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Farkas-based tree interpolation, NIL: learning nonlinear interpolants, On interpolation in automated theorem proving, Efficient Unlinkable Sanitizable Signatures from Signatures with Re-randomizable Keys, Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF, On Interpolation in Decision Procedures, Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic, Interpolation and Model Checking
