Name
Abstract | ||
|---|---|---|
While SAT-based algorithms have largely displaced BDD-based verification techniques due to their typically higher scalability, there are classes of problems for which BDD-based reachability analysis is the only existing method for an automated solution. Nonetheless, reachability engines require a high degree of tuning to perform well on challenging benchmarks. In addition to clever partitioning and scheduling techniques, the use of hints has been proposed to decompose an otherwise breadth-first fixedpoint computation into a series of underapproximate computations, requiring a larger number of (pre-)image iterations though often significantly reducing peak BDD size and thus resource requirements. In this paper, we introduce a novel approach to boost the scalability of reachability computation: automated netlist-based hint generation. Experiments confirm that this approach can yield significant resource reductions; often over an order of magnitude on complex problems compared to reachability analysis without hints, and even compared to SAT-based proof techniques. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/s10703-014-0213-0 | Formal Methods in System Design |
Keywords | DocType | Volume |
Formal methods,Formal verification,Reachability analysis,Automatic hints generation,Dynamic hints generation,Scalable formal methods,BDD-based reachability analysis | Journal | 45 |
Issue | ISSN | Citations |
2 | 0925-9856 | 6 |
PageRank | References | Authors |
0.55 | 19 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jiazhao Xu | 1 | 118 | 4.59 |
| Mark Williams | 2 | 7 | 1.25 |
| Hari Mony | 3 | 186 | 13.30 |
| Jason Baumgartner | 4 | 313 | 23.36 |