Name
Abstract | ||
|---|---|---|
Symbolic property verification is an increasingly popular debugging method based on Binary Decision Diagrams (BDDs). The lack of optimization of the state space search is often responsible for the excessive growth of the BDDs. In this paper we present an accelerated symbolic property verification by means of a new guiding technique that automatically finds the set of interesting variables by exploiting the property and the transition relation of a design. Our property based state space guiding can substantially speed up the verification process. The heuristic picks up the interesting state or the input variables automatically and utilizes them in guiding the state space traversal. This guiding approach is a novel one as it is automatic, efficient and stable for fast falsification. Furthermore it does not degrade as much for full validation. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1145/1146909.1147181 | DAC |
Keywords | Field | DocType |
state space traversal,symbolic bounded property checking,interesting state,state space,new guiding technique,guiding approach,verification process,accelerated symbolic property verification,interesting variable,symbolic property verification,state space search,property checking,verification,binary decision diagram | Heuristic,Tree traversal,Model checking,Computer science,Binary decision diagram,Algorithm,Theoretical computer science,State space search,State space,Bounded function,Debugging | Conference |
ISBN | Citations | PageRank |
1-59593-381-6 | 0 | 0.34 |
References | Authors | |
18 | 6 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Prakash M. Peranandam | 1 | 9 | 0.89 |
| Pradeep K. Nalla | 2 | 16 | 1.82 |
| Jürgen Ruf | 3 | 122 | 23.04 |
| Roland J. Weiss | 4 | 11 | 4.81 |
| Thomas Kropf | 5 | 326 | 59.09 |
| Wolfgang Rosenstiel | 6 | 1462 | 212.32 |