Name
Abstract | ||
|---|---|---|
We combine abstraction refinement and simulation to provide a more efficient approach to checking invariant properties whose only counterexamples are very long traces. We allow each transition of an abstract error trace to map to multiple transitions of the concrete error trace and simulate pseudorandom vectors to build segments of the concrete trace. This approach addresses the capacity limitation of the formal verification engine as well as the short-sightedness of the simulator, thus providing a more effective technique for deep, subtle bugs. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1145/1146909.1147097 | DAC |
Keywords | Field | DocType |
efficient approach,invariant property,long trace,abstraction refinement,abstract error trace,guiding simulation,concrete trace,effective technique,capacity limitation,formal verification engine,abstract trace,concrete error trace,algorithms,formal verification,model checking,verification,logic design,simulation | Formal equivalence checking,Functional verification,Model checking,Intelligent verification,Computer science,Algorithm,Runtime verification,Refinement,High-level verification,Formal verification | Conference |
ISSN | ISBN | Citations |
0738-100X | 1-59593-381-6 | 25 |
PageRank | References | Authors |
1.18 | 19 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kuntal Nanshi | 1 | 27 | 1.90 |
| Fabio Somenzi | 2 | 3394 | 302.47 |