Interpolation and Model Checking
From MaRDI portal
Publication:3176372
DOI10.1007/978-3-319-10575-8_14zbMath1392.68260OpenAlexW2803502305MaRDI QIDQ3176372
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_14
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)
Related Items
Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic, A note on constructive interpolation for the multi-modal logic \(K_m\), SAT-Based Model Checking, Satisfiability Modulo Theories, Combining Model Checking and Deduction, The mu-calculus and Model Checking, Differentiable learning of matricized DNFs and its application to Boolean networks
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Constraint solving for interpolation
- An interpolating theorem prover
- Playing in the grey area of proofs
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
- SAT-Based Model Checking
- Abstraction and Abstraction Refinement
- Predicate Abstraction for Program Verification
- Combining Model Checking and Deduction
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Abstractions from proofs
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
- Interpolant Strength
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Interpolating Quantifier-Free Presburger Arithmetic
- Interpolant Generation for UTVPI
- Interpolation and Symbol Elimination
- Rewriting-based Quantifier-free Interpolation for a Theory of Arrays.
- Automated Deduction – CADE-20
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- Tools and Algorithms for the Construction and Analysis of Systems
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
- Lazy Abstraction with Interpolants
- Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
