Name
Abstract | ||
|---|---|---|
Model checking is an automated formal method for verifying whether a finite-state system satisfies a user-supplied specification. The usefulness of the verification result depends on how well the specification distinguishes intended from non-intended system behavior. Vacuity is a notion that helps formalize this distinction in order to improve the user's understanding of why a property is satisfied. The goal of this paper is to expose vacuity in a property in a way that increases our knowledge of the design. Our approach, based on abstraction refinement, computes a maximal set of atomic subformula occurrences that can be strengthened without compromising satisfaction. The result is a shorter and stronger and thus, generally, more valuable property. We quantify the benefits of our technique on a substantial set of circuit benchmarks. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1109/DATE.2009.5090935 | Nice |
Keywords | Field | DocType |
circuit CAD,formal verification,integrated circuit testing,temporal logic,abstraction refinement,circuit benchmarks,finite-state system,formal verification,model checking,system behavior,temporal logic,user-supplied specification | Logic synthesis,Model checking,Programming language,Maximal set,Computer science,Upper and lower bounds,Theoretical computer science,Real-time computing,Formal methods,Temporal logic,Benchmark (computing),Formal verification | Conference |
ISSN | ISBN | Citations |
1530-1591 | 978-1-4244-3781-8 | 4 |
PageRank | References | Authors |
0.40 | 14 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mitra Purandare | 1 | 4 | 0.40 |
| Thomas Wahl | 2 | 103 | 10.21 |
| Daniel Kroening | 3 | 3084 | 187.60 |