Lazy Abstraction with Interpolants for Arrays
From MaRDI portal
Publication:2891439
DOI10.1007/978-3-642-28717-6_7zbMath1352.68141OpenAlexW2116333887MaRDI QIDQ2891439
Silvio Ghilardi, Silvio Ranise, Francesco Alberti, Roberto Bruttomesso, Natasha Sharygina
Publication date: 15 June 2012
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-28717-6_7
Related Items (16)
RustHorn: CHC-Based Verification for Rust Programs ⋮ Decision procedures for flat array properties ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Lingva: Generating and Proving Program Properties Using Symbol Elimination ⋮ Analyzing Array Manipulating Programs by Program Transformation ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ Complete instantiation-based interpolation ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ 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 ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists
Uses Software
This page was built for publication: Lazy Abstraction with Interpolants for Arrays
