Lazy Abstraction with Interpolants
From MaRDI portal
Publication:5756749
DOI10.1007/11817963_14zbMath1188.68196OpenAlexW1565898282MaRDI QIDQ5756749
Publication date: 5 September 2007
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11817963_14
Related Items (59)
Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Whale: An Interpolation-Based Algorithm for Inter-procedural Verification ⋮ Splitting via Interpolants ⋮ Proof tree preserving tree interpolation ⋮ Decision procedures for flat array properties ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Guiding Craig interpolation with domain-specific abstractions ⋮ Abstraction and Abstraction Refinement ⋮ Interpolation and Model Checking ⋮ Predicate Abstraction for Program Verification ⋮ Sharper and Simpler Nonlinear Interpolants for Program Verification ⋮ On Abstraction of Probabilistic Systems ⋮ Constraint solving for interpolation ⋮ Interpolation Results for Arrays with Length and MaxDiff ⋮ Symbolic encoding of LL(1) parsing and its applications ⋮ Dynamic Reductions for Model Checking Concurrent Software ⋮ Counterexample Validation and Interpolation-Based Refinement for Forest Automata ⋮ SAT-based invariant inference and its relation to concept learning ⋮ Probabilistic CEGAR ⋮ A unifying view on SMT-based software verification ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ Efficient strategies for CEGAR-based model checking ⋮ Unnamed Item ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ Complete instantiation-based interpolation ⋮ Unnamed Item ⋮ SMT-based verification of data-aware processes: a model-theoretic approach ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Counterexample-Guided Refinement of Template Polyhedra ⋮ Parallelizing SMT solving: lazy decomposition and conciliation ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ Exploiting partial variable assignment in interpolation-based model checking ⋮ Sharpening constraint programming approaches for bit-vector theory ⋮ An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic ⋮ Interpolant Generation for UTVPI ⋮ Ground Interpolation for Combined Theories ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Proving Safety with Trace Automata and Bounded Model Checking ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ Accelerating Interpolation-Based Model-Checking ⋮ Automatically Refining Abstract Interpretations ⋮ Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference ⋮ Abstraction refinement and antichains for trace inclusion of infinite state systems ⋮ On recursion-free Horn clauses and Craig interpolation ⋮ Efficient generation of small interpolants in CNF ⋮ Under-approximating loops in C programs for fast counterexample detection ⋮ Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) ⋮ Model completeness, covers and superposition ⋮ Refinement of Trace Abstraction ⋮ Interpolation in computing science: The semantics of modularization ⋮ A Configurable CEGAR Framework with Interpolation-Based Refinements ⋮ Infeasible Paths Elimination by Symbolic Execution Techniques ⋮ A Survey of Satisfiability Modulo Theory ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
This page was built for publication: Lazy Abstraction with Interpolants
