Guiding Craig interpolation with domain-specific abstractions
From MaRDI portal
Publication:300418
DOI10.1007/s00236-015-0236-zzbMath1344.68139OpenAlexW595779784MaRDI QIDQ300418
Philipp Rümmer, Jérôme Leroux, Pavle Subotić
Publication date: 28 June 2016
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-268743
Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)
Related Items
Causality-based game solving, Automating regression verification of pointer programs by predicate abstraction, Unnamed Item, Syntax-guided synthesis for lemma generation in hardware model checking, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On recursion-free Horn clauses and Craig interpolation
- On the reachability problem for 5-dimensional vector addition systems
- A structure to decide reachability in Petri nets
- Dual analysis for proving safety and finding bugs
- Infinite-state invariant checking with IC3 and predicate abstraction
- Generalized Property Directed Reachability
- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification
- Lazy Abstraction with Interpolants for Arrays
- Playing in the grey area of proofs
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- A Lightweight Approach for Loop Summarization
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Abstractions from proofs
- Automatic Verification of Integer Array Programs
- Interpolant Strength
- Accelerating Interpolants
- Synthesis of Circular Compositional Program Proofs via Abduction
- An Efficient and Flexible Approach to Resolution Proof Reduction
- Consistency analysis of decision-making programs
- Vector addition system reachability problem
- Constraint Solving for Interpolation
- Invariant Synthesis for Combined Theories
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Accelerating Interpolation-Based Model-Checking
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Programs with Lists Are Counter Automata
- Lazy Abstraction with Interpolants
- Complete instantiation-based interpolation
- Tools and Algorithms for the Construction and Analysis of Systems
