Making abstraction-refinement efficient in model checking

DOI10.1007/978-3-642-22685-4_36MaRDI QIDQ3087967zbMATH OpenOpenAlexFDO

Authors Cong Tian, Zhenhua Duan

Publication date 17 August 2011

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

Full work available at URL https://arxiv.org/abs/1007.3569

Mathematics Subject Classification ID

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

Abstract: Abstraction is one of the most important strategies for dealing with the state space explosion problem in model checking. In the abstract model, although the state space is largely reduced, however, a counterexample found in such a model may not be a real counterexample. And the abstract model needs to be further refined where an NP-hard state separation problem is often involved. In this paper, a novel method is presented by adding extra variables to the abstract model for the refinement. With this method, not only the NP-hard state separation problem is avoided, but also a smaller refined abstract model is obtained.

Recommendations

• An efficient approach for abstraction-refinement in model checking
• Abstraction and abstraction refinement
• Correct Hardware Design and Verification Methods
• Abstraction and Refinement in Model Checking
• Counterexample-guided abstraction refinement for symbolic model checking

Cited in

(9)

• An automatic method for the dynamic construction of abstractions of states of a formal model
• Comparing abstraction refinement algorithms
• Abstraction and Refinement in Model Checking
• Automata-Based Abstraction Refinement for µHORS Model Checking
• A type-directed abstraction refinement approach to higher-order model checking
• Correct Hardware Design and Verification Methods
• Tools and Algorithms for the Construction and Analysis of Systems
• The role of abstraction in model checking
• An efficient approach for abstraction-refinement in model checking

This page was built for publication: Making abstraction-refinement efficient in model checking

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