Name
Abstract | ||
|---|---|---|
Verification benefits from removing logic that is not relevant for a proof. Techniques for doing this are known as localization abstraction. Abstraction is often performed by selecting a subset of gates to be included in the abstracted model; the signals feeding into this subset become unconstrained cut-points. In this paper, we propose several improvements to substantially increase the scalability of automated abstraction. In particular, we show how a better integration between the BMC engine and the SAT solver is achieved, resulting in a new hybrid abstraction engine, that is faster and uses less memory. This engine speeds up computation by constant propagation and circuit-based structural hashing while collecting UNSAT cores for the intermediate proofs in terms of a subset of the original variables. Experimental results show improvements in the abstraction depth and size. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.7873/DATE.2013.286 | DATE |
Keywords | Field | DocType |
liquid cooling,finite difference method | Abstraction model checking,Abstraction,Computer science,Parallel computing,Boolean satisfiability problem,Algorithm,Real-time computing,Mathematical proof,Abstraction inversion,Hash function,Scalability,Computation | Conference |
ISSN | Citations | PageRank |
1530-1591 | 7 | 0.51 |
References | Authors | |
13 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alan Mishchenko | 1 | 982 | 84.79 |
| Niklas Een | 2 | 1573 | 66.34 |
| Robert K. Brayton | 3 | 6224 | 883.32 |
| Jason Baumgartner | 4 | 313 | 23.36 |
| Hari Mony | 5 | 186 | 13.30 |
| Pradeep Kumar Nalla | 6 | 7 | 0.51 |