Applications of Craig interpolation to model checking

DOI10.1007/978-3-540-30124-0_3MaRDI QIDQ5311270zbMATH OpenOpenAlexFDO

Authors K. L. McMillan

Publication date 22 August 2005

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

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

Mathematics Subject Classification ID

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

Recommendations

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

Cited in

(43)

• Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations
• Fast interpolating BMC
• Exploiting partial variable assignment in interpolation-based model checking
• Syntax-guided synthesis for lemma generation in hardware model checking
• Interpolants in nonlinear theories over the reals
• An interpolating theorem prover
• Interpolant strength revisited
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• PeRIPLO: a framework for producing effective interpolants in SAT-based software verification
• Generalized Craig interpolation for stochastic Boolean satisfiability problems with applications to probabilistic state reachability and region stability
• Guiding Craig interpolation with domain-specific abstractions
• Craig interpolation in the presence of non-linear constraints
• Interpolation and model checking
• Selfless interpolation for infinite-state model checking
• Generalized Craig interpolation for stochastic satisfiability modulo theory problems
• Abstractions from proofs
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Craig Interpolation for Linear Temporal Languages
• Interpolant strength
• Effectively propositional interpolants
• Accelerating interpolants
• Resolution proof transformation for compression and interpolation
• Craig interpolation and reachability analysis
• Encoding techniques, Craig interpolants and bounded model checking for incomplete designs
• Interpolation Properties and SAT-Based Model Checking
• Interpolant Generation for UTVPI
• Effective interpolation and preservation in guarded logics
• Interpolants and Symbolic Model Checking
• Approximation Refinement for Interpolation-Based Model Checking
• Accelerating Interpolation-Based Model-Checking
• Correct Hardware Design and Verification Methods
• Applications of Craig interpolants in model checking
• Applications of Craig interpolation to model checking
• Lazy Abstraction with Interpolants
• Complete instantiation-based interpolation
• Interpolation and SAT-based model checking.
• Constructing Craig interpolation formulas
• Decomposing Farkas Interpolants
• Invariant inference with provable complexity from the monotone theory
• Interpolating strong induction
• Efficient generation of small interpolants in CNF
• Interpolation and model checking for nonlinear arithmetic
• Optimization techniques for Craig interpolant compaction in unbounded model checking

This page was built for publication: Applications of Craig interpolation to model checking

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