Abstraction refinement for bounded model checking

DOI10.1007/11513988_11MaRDI QIDQ5716541zbMATH OpenOpenAlexFDO

Authors Anubhav Gupta, Ofer Strichman

Publication date 10 January 2006

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

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

Mathematics Subject Classification ID

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

Recommendations

• SAT-based counterexample guided abstraction refinement
• Counterexample-guided abstraction refinement
• SAT based abstraction-refinement using ILP and machine learning techniques
• Counterexample-guided abstraction refinement for symbolic model checking
• Partial predicate abstraction and counter-example guided refinement

Cited in

(25)

• SAT competition 2020
• Efficient strategies for CEGAR-based model checking
• Partial predicate abstraction and counter-example guided refinement
• Infinite-state invariant checking with IC3 and predicate abstraction
• A configurable CEGAR framework with interpolation-based refinements
• Computing over-approximations with bounded model checking
• Abstraction and abstraction refinement
• Abstraction and Refinement in Model Checking
• Refinement of LTL formulas for abstract model checking
• Automata-Based Abstraction Refinement for µHORS Model Checking
• SAT-based counterexample guided abstraction refinement
• SAT based abstraction-refinement using ILP and machine learning techniques
• Semi-formal bounded model checking
• Thread-modular counterexample-guided abstraction refinement
• Compositional safety refutation techniques
• Model Checking Software
• A type-directed abstraction refinement approach to higher-order model checking
• Concrete model checking with abstract matching and refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification Modulo theories
• Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking
• Constraint reusing and k-induction for three-valued bounded model checking
• Proof-Guided Underapproximation Widening for Bounded Model Checking
• An efficient approach for abstraction-refinement in model checking
• Model checking as program verification by abstract interpretation

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Abstraction refinement for bounded model checking

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