Accelerating Interpolation-Based Model-Checking

DOI10.1007/978-3-540-78800-3_32MaRDI QIDQ5458343zbMATH OpenOpenAlexFDO

Authors Nicolas Caniart, Emmanuel Fleury, Jérôme Leroux, Marc Zeitoun

Publication date 11 April 2008

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78800-3_32

Mathematics Subject Classification ID

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

Recommendations

• Approximation Refinement for Interpolation-Based Model Checking
• Accelerating interpolants
• Interpolation and SAT-based model checking.
• Selfless interpolation for infinite-state model checking
• Computer Science Logic

Cites work

• scientific article; zbMATH DE number 1670791 (Why is no real title available?)
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• An interpolating theorem prover
• Automated Technology for Verification and Analysis
• Counterexample-guided abstraction refinement for symbolic model checking
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Lazy abstraction
• On iterating linear transformations over recognizable sets of integers
• Semigroups, Presburger formulas, and languages
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(13)

• Algebraic program analysis
• Guiding Craig interpolation with domain-specific abstractions
• Selfless interpolation for infinite-state model checking
• A calculus for modular loop acceleration
• Approximation Refinement for Interpolation-Based Model Checking
• Correct Hardware Design and Verification Methods
• Optimization techniques for Craig interpolant compaction in unbounded model checking
• Accelerating interpolants
• Intertwined forward-backward reachability analysis using interpolants
• Interpolation Properties and SAT-Based Model Checking
• Fast interpolating BMC
• Transition power abstractions for deep counterexample detection
• Automated Technology for Verification and Analysis

This page was built for publication: Accelerating Interpolation-Based Model-Checking

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