Quantifier-Free Interpolation of a Theory of Arrays
From MaRDI portal
Publication:2887061
DOI10.2168/LMCS-8(2:4)2012zbMath1237.68123OpenAlexW2036325129MaRDI QIDQ2887061
Silvio Ranise, Roberto Bruttomesso, Silvio Ghilardi
Publication date: 16 May 2012
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.2168/lmcs-8(2:4)2012
Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)
Related Items
Interpolation systems for ground proofs in automated deduction: a survey, Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays, Interpolation Results for Arrays with Length and MaxDiff, Weakly Equivalent Arrays, An extension of lazy abstraction with interpolation for programs with arrays, Interpolation and amalgamation for arrays with MaxDiff, Quantifier-free interpolation in combinations of equality interpolating theories, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Reasoning in the theory of heap: satisfiability and interpolation
Uses Software
