Sciweavers

Share
DAC
2004
ACM

Abstraction refinement by controllability and cooperativeness analysis

10 years 2 months ago
Abstraction refinement by controllability and cooperativeness analysis
ion Refinement by Controllability and Cooperativeness Analysis Freddy Y.C. Mang and Pei-Hsin Ho Advanced Technology Group, Synopsys, Inc. {fmang, pho}@synopsys.com nt a new abstraction refinement algorithm to better he abstract model for formal property verification. In previous work, refinements are selected either based on a set of examples of the current abstract model, as in [5][6][7][8][9][19][20], or independent of any counter examples, as in [17]. 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 he abstract model. We implemented the algorithm and applied it to verify several real-world designs and properties. We the algorithm against the abstraction refinement algorithms in [19] and [20] and the interpolation-based reachability analysis in [14]. The experimental r...
Freddy Y. C. Mang, Pei-Hsin Ho
Added 13 Nov 2009
Updated 13 Nov 2009
Type Conference
Year 2004
Where DAC
Authors Freddy Y. C. Mang, Pei-Hsin Ho
Comments (0)
books