Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Proofs from tests
Beckman N., Nori A., Rajamani S., Simmons R.  Software testing and analysis (Proceedings of the 2008 International Symposium on Software Testing and Analysis, Seattle, WA, Jul 20-24, 2008)3-14.2008.Type:Proceedings
Date Reviewed: Sep 29 2008

Based in the area of software verification that uses model-checking methods, this paper builds on the recent verification methods that employ the technique of counterexample guided abstraction refinement (CEGAR) for proving a program’s correctness. In order to check whether a program satisfies a safety property, CEGAR-based techniques build a series of finite-state abstractions of the program until one of the following is found: a counterexample that demonstrates that the property is violated, or a finite-state abstraction of the program, which is an over approximation of the program satisfying the property. CEGAR-based verification methods differ from one another based on the kind of abstractions employed and the particular methods used for refinement.

This paper proposes an algorithm, called DASH, that is based on an algorithm called Synergy, proposed earlier by the authors. Like Synergy, DASH performs testing and abstraction simultaneously, guiding the test process to select the right abstraction. DASH extends Synergy in three significant respects: it can handle programs with pointers; it can handle programs with procedure calls; and, for proving the soundness of the abstraction, it makes less theorem-proving calls, a costly step in the CEGAR techniques. The simple idea of template-based refinement reduces the number of theorem-prover calls. Variable aliasing information is important for handling pointers, and accurate computation of this is not always possible. A novel strategy of using the aliasing local to a given test improves the performance and accuracy of the algorithm. The entire algorithm is implemented and evaluated successfully on a number of device driver benchmarks.

The paper is very well written, with good illustrations and explanations. It is a must-read for people working with software verification, and will interest people working in program testing too.

Reviewer:  S. Ramesh Review #: CR136108 (0912-1169)
Bookmark and Share
  Reviewer Selected
Featured Reviewer
 
 
Model Checking (D.2.4 ... )
 
 
Correctness Proofs (D.2.4 ... )
 
 
Symbolic Execution (D.2.5 ... )
 
 
Software/ Program Verification (D.2.4 )
 
 
Testing And Debugging (D.2.5 )
 
Would you recommend this review?
yes
no
Other reviews under "Model Checking": Date
Systems and software verification: model-checking techniques and tools
B ., Bidoit M., Finkel A., Laroussinie F., Petit A., Petrucci L., Schnoebelen P., McKenzie P., Springer-Verlag New York, Inc., New York, NY, 1999.  190, Type: Book (9783540415237)
Sep 30 2002
Module checking
Kupferman O., Vardi M., Wolper P. Information and Computation 164(2): 322-344, 2001. Type: Article
Mar 1 2002
SMC: a symmetry-based model checker for verification of safety and liveness properties
Sistla A., Gyuris V., Emerson E. ACM Transactions on Software Engineering and Methodology 9(2): 133-166, 2000. Type: Article
Sep 1 2000
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy