Paper Info
Title
A Hybrid of Counterexample-Based and Proof-Based Abstraction
Abstract
Counterexample- and proof-based refinement are complementary approaches to iterative abstraction. In the former case, a single abstract counterexample is eliminated by each refinement step, while in the latter case, all counterexamples of a given length are eliminated. In counterexample-based abstraction, the concretization and refinement problems are relatively easy, but the number of iterations tends to be large. Proof-based abstraction, on the other hand, puts a greater burden on the refinement step, which can then become the performance bottleneck. In this paper, we show that counterexample- and proof-based refinement are extremes of a continuum, and propose a hybrid approach that balances the cost and quality of refinement. In a study of a large number of industrial verification problems, we find that there is a strong relation between the effort applied in the refinement phase and the number of refinement iterations. For this reason, proof-based abstraction is substantially more efficient than counterexample-based abstraction. However, a judicious application of the hybrid approach can lessen the refinement effort without unduly increasing the number of iterations, yielding a method that is somewhat more robust overall.
Year
DOI
Venue
2004
10.1007/978-3-540-30494-4_19
Lecture Notes in Computer Science
Field
DocType
Volume
Discrete mathematics,Bottleneck,Abstraction,Iterative method,Computer science,Computer Aided Design,Algorithm,Theoretical computer science,Formal methods,Counterexample
Conference
3312
ISSN
Citations 
PageRank 
0302-9743
19
0.98
References 
Authors
15
2
Name
Order
Citations
PageRank
Nina Amla131816.23
Kenneth L. McMillan23332269.05