Counterexample-guided abstraction refinement

The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant...

Full description

Saved in:
Bibliographic Details
Main Author: Clarke, E.
Format: Conference Proceeding
Language:English
Subjects:
Boolean functions
Collaboration
Computer science
Concrete
Contracts
Data mining
Data structures
Explosions
State-space methods
US Department of Defense
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The main practical problem in model checking is the combinatorial explosion of system states commonly known as the state explosion problem. Abstraction methods attempt to reduce the size of the state space by employing knowledge about the system and the specification in order to model only relevant features in the Kripke structure. Counterexample-guided abstraction refinement is an automatic abstraction method where, starting with a relatively small skeletal representation of the system to be verified, increasingly precise abstract representations of the system are computed. The key step is to extract information from false negatives ("spurious counterexamples") due to over-approximation.
ISSN:1530-1311
2332-6468
DOI:10.1109/TIME.2003.1214874