Name
Abstract | ||
|---|---|---|
A heuristic-based symbolic model checking algorithm, BDD-IDA*. that efficiently falsifies invariant properties of a system is presented. As in bounded model checking, the algorithm uses an iterative deepening search strategy. However, in our case, the search strategy is guided by a heuristic that is computed from an abstract model, which is derived from the concrete model by a synthesis technique. Synthesis involves eliminating so-called weak variables from the concrete specification, where the weak variables are identified by a data-dependency analysis. Unique to this work is the use of the depth-first IDA* search algorithm in a BDD setting, and the automatic synthesis of the heuristic. The performance of the approach on a large number of small examples is compared with standard BDD-based approaches. Experiments on a variety of real-world models from different domains are also conducted. The approach reveals a consistent improvement on all models, and in some cases a speed-up of 2 orders of magnitude is obtained. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11562436_21 | FORTE |
Keywords | Field | DocType |
search strategy,abstract model,search algorithm,concrete specification,abstraction-guided model checking,automatic synthesis,real-world model,synthesis technique,concrete model,heuristic-based symbolic model checking,symbolic ida,bounded model checking,heuristic synthesis,model checking,heuristic search,formal verification | Heuristic,Search algorithm,Model checking,Computer science,Iterative method,Abstract interpretation,Algorithm,Theoretical computer science,Symbolic trajectory evaluation,Iterative deepening depth-first search,Formal verification | Conference |
Volume | ISSN | ISBN |
3731 | 0302-9743 | 3-540-29189-X |
Citations | PageRank | References |
7 | 0.45 | 22 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kairong Qian | 1 | 63 | 3.38 |
| Albert Nymeyer | 2 | 106 | 9.98 |
| Steven Susanto | 3 | 10 | 0.85 |