Interpolation and model checking

DOI10.1007/978-3-319-10575-8_14zbMATH Open1392.68260OpenAlexW2803502305MaRDI QIDQ3176372FDOQ3176372

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (11)

• 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
• Differentiable learning of matricized DNFs and its application to Boolean networks

Uses Software

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

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)