Name
Abstract | ||
|---|---|---|
The major challenge in model checking for more than two decades has been dealing with the very large number of states that typify industrial systems. Abstraction-based methods have been particularly successful in this regard. Heuristic-based methods that use domain knowledge to guide a model checker can also be effective in dealing with large systems. In this work, we present an abstraction and heuristic-based model checking algorithm (called Static Abstraction Guided model checking) that verifies the safety properties of a system. Unlike other abstraction-based approaches, this work proposes a model-checking algorithm that uses a sequence of abstract models as input, and a method to refine counterexamples to determine whether they are spurious or real. During this refinement, abstract models in the sequence are used as heuristics to guide the model checker. This tight integration of abstraction and guidance is doubly effective in countering state explosion. This paper deals with the theoretical and algorithmic aspects of the approach only. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/978-3-540-30476-0_17 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
model checking,domain knowledge | Abstraction model checking,Heuristic,Abstraction,Algorithmics,Model checking,Abstract interpretation,Computer science,Model-based reasoning,Theoretical computer science,Program analysis | Conference |
Volume | ISSN | Citations |
3299 | 0302-9743 | 9 |
PageRank | References | Authors |
0.50 | 24 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kairong Qian | 1 | 63 | 3.38 |
| Albert Nymeyer | 2 | 106 | 9.98 |