Applications of Craig interpolants in model checking

DOI10.1007/B107194MaRDI QIDQ5703754zbMATH OpenOpenAlexFDO

Authors K. L. McMillan

Publication date 10 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b107194

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Applications of Craig interpolation to model checking
• Applications of Craig interpolation to model checking
• Interpolants and Symbolic Model Checking
• Craig interpolation and reachability analysis
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(37)

• Generalised graded interpolation
• Efficient strategies for CEGAR-based model checking
• Interpolants in nonlinear theories over the reals
• Modularity results for interpolation, amalgamation and superamalgamation
• Craig interpolation with clausal first-order tableaux
• A configurable CEGAR framework with interpolation-based refinements
• Automated formal analysis and verification: an overview
• Splitting via Interpolants
• Generalized Craig interpolation for stochastic Boolean satisfiability problems
• Guiding Craig interpolation with domain-specific abstractions
• Craig interpolation in displayable logics
• Satisfiability modulo theories
• Interpolants for Linear Arithmetic in SMT
• Craig Interpolation for Linear Temporal Languages
• Efficient combination of decision procedures for MUS computation
• Craig interpolation for networks of sentences
• A decidability result for the model checking of infinite-state systems
• Cuts from proofs: a complete and practical technique for solving linear inequalities over integers
• Craig interpolation and reachability analysis
• Sharper and Simpler Nonlinear Interpolants for Program Verification
• Interpolation Properties and SAT-Based Model Checking
• Applications of Craig interpolation to model checking
• Rewriting interpolants
• Competent predicate abstraction in model checking
• Interpolants and Symbolic Model Checking
• An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
• Correct Hardware Design and Verification Methods
• Mechanising a Proof of Craig’s Interpolation Theorem for Intuitionistic Logic in Nominal Isabelle
• Applications of Craig interpolation to model checking
• Constructing Craig interpolation formulas
• Transition power abstractions for deep counterexample detection
• Interpolation for converse PDL
• On symbol elimination and uniform interpolation in theory extensions
• The Craig interpolation property in first-order Gödel logic
• Invertibility in Sequent Calculi
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Property-directed incremental invariant generation

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Applications of Craig interpolants in model checking

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