Abstract | ||
---|---|---|
We present a new abstraction refinement algorithm to better refine the abstract model for formal property verification. In previous work, refinements are selected either based on a set of counter examples of the current abstract model, as in [5, 6, 7, 8, 9, 20, 211, or independent of any counter examples, as in [18]. We (1) introduce a new controllability analysis that is independent of any particular counter examples, (2) apply a new cooperativeness analysis that extracts information from a particular set of counter examples and (3) combine both to better refine the abstract model. We implemented the algorithm and applied it to verify several real-world designs and properties. We compared the algorithm against the abstraction refinement algorithms in [20] and [211 and the interpolation-based reachability analysis in [15]. The experimental results indicate that the new algorithm outperforms the other three algorithms in terms of runtime, abstraction efficiency (as defined in [20]) and the number of proven properties. |
Year | DOI | Venue |
---|---|---|
2006 | 10.1142/S0129054106004091 | INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE |
Keywords | Field | DocType |
formal verification, abstraction refinement, controllability, cooperativeness | Discrete mathematics,Abstraction,Controllability,Interpolation,Reachability,Theoretical computer science,Cooperativeness,Abstraction refinement,Counterexample,Mathematics,Formal verification | Journal |
Volume | Issue | ISSN |
17 | 4 | 0129-0541 |
Citations | PageRank | References |
0 | 0.34 | 6 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
FREDDY Y. C. MANG | 1 | 0 | 0.34 |
Pei-hsin Ho | 2 | 2577 | 305.29 |