Interpolation and model checking

DOI10.1007/978-3-319-10575-8_14MaRDI QIDQ3176372zbMATH OpenOpenAlexFDO

Authors K. L. McMillan

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Interpolation, preservation, definability (03C40)

Recommendations

• Computer Science Logic
• Guiding Craig interpolation with domain-specific abstractions
• Abstractions from proofs
• Approximation Refinement for Interpolation-Based Model Checking
• Interpolation Properties and SAT-Based Model Checking

Cites work

• scientific article; zbMATH DE number 1670555 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Abstraction and abstraction refinement
• Abstractions from proofs
• An interpolating sequent calculus for quantifier-free Presburger arithmetic
• An interpolating theorem prover
• Automated Deduction – CADE-20
• Beyond quantifier-free interpolation in extensions of Presburger arithmetic
• Combining Model Checking and Deduction
• Constraint solving for interpolation
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Interpolant Generation for UTVPI
• Interpolant strength
• Interpolating quantifier-free Presburger arithmetic
• Interpolation and SAT-based model checking.
• Interpolation and Symbol Elimination
• Lazy Abstraction with Interpolants
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Playing in the grey area of proofs
• Predicate abstraction for program verification
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Rewriting-based quantifier-free interpolation for a theory of arrays
• SAT-Based Model Checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(11)

• Differentiable learning of matricized DNFs and its application to Boolean networks
• Mind the gap: bit-vector interpolation recast over linear integer arithmetic
• A note on constructive interpolation for the multi-modal logic \(K_m\)
• Correct Hardware Design and Verification Methods
• The mu-calculus and Model Checking
• Craig interpolation for decidable first-order fragments
• SAT-Based Model Checking
• Satisfiability modulo theories
• Combining Model Checking and Deduction
• Interpolation Properties and SAT-Based Model Checking
• Interpolation in practical formal development

Describes a project that uses

Uses Software

• YOGI
• FOCI
• SatAbs
• Bebop
• Princess
• z3
• SPIN

This page was built for publication: Interpolation and model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176372)