Name
Title | ||
|---|---|---|
Multiple-counterexample guided iterative abstraction refinement: an industrial evaluation |
Abstract | ||
|---|---|---|
In this paper, we describe a completely automated framework for iterative abstraction refinement that is fully integrated into a formal-verification environment. This environment consists of three basic software tools: Forecast, a BDD-based model checker, Thunder, a SAT-based bounded model checker, and MCE, a technology for multiple-counterexample analysis. In our framework, the initial abstraction is chosen relative to the property under verification. The abstraction is model checked by Forecast; in case of failure, a counter example is returned. Our framework includes an abstract counterexample analyzer module that applies techniques for bounded model checking to check whether the abstract counter example holds in the concrete model. If it does, it is extended to a concrete counter example. This important capability is provided as a separate tool that also addresses one of the major problems of verification by manual abstraction. If the counter example is spurious, we use a novel refinement heuristic based on MCE to guide the refinement. After the part of the abstract model to be refined is chosen, our refinement algorithm computes a new abstraction that includes as much logic as possible without adding too many new variables, therefore striking a balance between refining the abstraction and keeping its size manageable. We demonstrate the effectiveness of our framework on challenging Intel designs that were not amenable to BDD-based model-checking approaches. |
Year | Venue | Keywords |
|---|---|---|
2003 | TACAS | concrete model,counter example,iterative abstraction refinement,abstract model,bdd-based model checker,sat-based bounded model checker,bounded model checking,industrial evaluation,manual abstraction,new abstraction,initial abstraction,formal verification,model checking |
Field | DocType | Volume |
Abstraction model checking,Heuristic,Programming language,Model checking,Abstraction,Computer science,Theoretical computer science,Software,Counterexample,Spurious relationship,Bounded function | Conference | 2619 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-00898-5 | 39 |
PageRank | References | Authors |
1.47 | 30 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marcelo Glusman | 1 | 49 | 2.89 |
| Gila Kamhi | 2 | 344 | 23.22 |
| Sela Mador-Haim | 3 | 174 | 6.87 |
| Ranan Fraer | 4 | 276 | 17.94 |
| Moshe Y. Vardi | 5 | 13413 | 2267.07 |