This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Proofs from Tests
July/August 2010 (vol. 36 no. 4)
pp. 495-508
ASCII Text
x 
 
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, Aditya V. Thakur, "Proofs from Tests," IEEE Transactions on Software Engineering, vol. 36, no. 4, pp. 495-508, July/August, 2010.
 
 
BibTex
x
 
@article{ 10.1109/TSE.2010.49,
author = {Nels E. Beckman and Aditya V. Nori and Sriram K. Rajamani and Robert J. Simmons and Sai Deep Tetali and Aditya V. Thakur},
title = {Proofs from Tests},
journal ={IEEE Transactions on Software Engineering},
volume = {36},
number = {4},
issn = {0098-5589},
year = {2010},
pages = {495-508},
doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.49},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Software Engineering
TI - Proofs from Tests
IS - 4
SN - 0098-5589
SP495
EP508
EPD - 495-508
A1 - Nels E. Beckman,
A1 - Aditya V. Nori,
A1 - Sriram K. Rajamani,
A1 - Robert J. Simmons,
A1 - Sai Deep Tetali,
A1 - Aditya V. Thakur,
PY - 2010
KW - Software model checking
KW - directed testing
KW - abstraction refinement.
VL - 36
JA - IEEE Transactions on Software Engineering
ER -
 
Nels E. Beckman, Carnegie Mellon University, Pittsburgh
Aditya V. Nori, Microsoft Research India, Bangalore
Sriram K. Rajamani, Microsoft Research India, Bangalore
Robert J. Simmons, Carnegie Mellon University, Pittsburgh
Sai Deep Tetali, University of California, Los Angeles, Los Angeles
Aditya V. Thakur, University of Wisconsin-Madison, Madison
We present an algorithm Dash to check if a program P satisfies a safety property \varphi. The unique feature of this algorithm is that it uses only test generation operations, and it refines and maintains a sound program abstraction as a consequence of failed test generation operations. Thus, each iteration of the algorithm is inexpensive, and can be implemented without any global may-alias information. In particular, we introduce a new refinement operator {\rm {WP}}_\alpha that uses only the alias information obtained by symbolically executing a test to refine abstractions in a sound manner. We present a full exposition of the Dash algorithm and its theoretical properties. We have implemented Dash in a tool called Yogi that plugs into Microsoft's Static Driver Verifier framework. We have used this framework to run Yogi on 69 Windows Vista drivers with 85 properties and find that Yogi scales much better than Slam, the current engine driving Microsoft's Static Driver Verifier.

[1] E.W. Dijkstra, "The Humble Programmer," Comm. ACM, vol. 15, no. 10, pp. 859-866, 1972.
[2] P. Godefroid, N. Klarlund, and K. Sen, "Dart: Directed Automated Random Testing," Proc. Programming Language Design and Implementation, pp. 213-223, 2005.
[3] C. Cadar, V. Ganesh, P.M. Pawlowski, D.L. Dill, and D.R. Engler, "EXE: Automatically Generating Inputs of Death," Proc. ACM Conf. Computer and Comm. Security, 2006.
[4] K. Sen, D. Marinov, and G. Agha, "Cute: A Concolic Unit Testing Engine for C," Proc. Foundations of Software Eng., pp. 263-272, 2005.
[5] B.S. Gulavani, T.A. Henzinger, Y. Kannan, A.V. Nori, and S.K. Rajamani, "Synergy: A New Algorithm for Property Checking," Proc. Foundations of Software Eng., pp. 117-127, 2006.
[6] T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani, "Automatic Predicate Abstraction of C Programs," Proc. Programming Language Design and Implementation, pp. 203-213, 2001.
[7] T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, "Lazy Abstraction," Proc. Principles of Programming Languages, pp. 58-70, 2002.
[8] E.W. Dijkstra, A Discipline of Programming. Prentice Hall, 1997.
[9] T. Ball and S.K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces," Proc. SPIN Workshop Model Checking of Software, pp. 103-122, 2001.
[10] T.A. Henzinger, R. Jhala, R. Majumdar, and K.L. McMillan, "Abstractions from Proofs," Proc. Principles of Programming Languages, pp. 232-244, 2004.
[11] N.E. Beckman, A.V. Nori, S.K. Rajamani, and R.J. Simmons, "Proofs from Tests," Proc. Int'l Symp. Software Testing and Analysis, pp. 103-122, 2008.
[12] P. Godefroid and N. Klarlund, "Software Model Checking: Searching for Computations in the Abstract or the Concrete," Proc. Integrated Formal Methods, pp. 20-32, 2005.
[13] E. Gunter and D. Peled, "Model Checking, Testing and Verification Working Together," Formal Aspects of Computing, vol. 17, no. 2, pp. 201-221, 2005.
[14] G. Yorsh, T. Ball, and M. Sagiv, "Testing, Abstraction, Theorem Proving: Better Together!" Proc. Int'l Symp. Software Testing and Analysis, pp. 145-156, 2006.
[15] D. Kroening, A. Groce, and E.M. Clarke, "Counterexample Guided Abstraction Refinement via Program Execution," Proc. Int'l Conf. Formal Eng. Methods, pp. 224-238, 2004.
[16] P. Godefroid, "Compositional Dynamic Test Generation," Proc. Principles of Programming Languages, pp. 47-54, 2007.
[17] R. Majumdar and K. Sen, "Latest: Lazy Dynamic Test Input Generation," Technical Report UCB/EECS-2007-36, Electrical Eeng. and Computer Science Dept., Univ. of California, http://www.eecs.berkeley.edu/Pubs/TechRpts/ 2007EECS-2007-36.html, Mar. 2007.
[18] P. Godefroid, A.V. Nori, S.K. Rajamani, and S. Tetali, "Compositional May-Must Program Analysis: Unleashing the Power of Alternation," Proc. Principles of Programming Languages, 2010.
[19] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-Guided Abstraction Refinement," Proc. Computer Aided Verification, pp. 154-169, 2000.
[20] D.L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe, "Extended Static Checking," Technical Report/Research Report 159, Compaq Systems Research Center, Dec. 1998.
[21] M. Barnett, B.-Y.E. Chang, R. DeLine, B. Jacobs, and K.R.M. Leino, "Boogie: A Modular Reusable Verifier for Object-Oriented Programs," Proc. Formal Methods for Components and Objects, pp. 364-387.
[22] K.S. Namjoshi and R.P. Kurshan, "Syntactic Program Transformations for Automatic Abstraction," Proc. Computer Aided Verification, pp. 435-449, 2000.
[23] T. Ball, personal communication.
[24] T. Ball and S.K. Rajamani, "Slic: A Specification Language for Interface Checking of C," Technical Report MSR-TR-2001-21, Microsoft Research, 2001.
[25] L. de Moura and N. Bjorner, "Z3: An Efficient Smt Solver," Proc. Tools and Algorithms for the Construction and Analysis of Systems, 2008.
[26] S. Qadeer and D. Wu, "KISS: Keep it Simple and Sequential," Proc. Programming Language Design and Implementation, pp. 14-24, 2004.
[27] B. Cook, A. Podelski, and A. Rybalchenko, "Termination Proofs for Systems Code," Proc. Programming Language Design and Implementation, pp. 415-426, 2006.

Index Terms:
Software model checking, directed testing, abstraction refinement.
Citation:
Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, Sai Deep Tetali, Aditya V. Thakur, "Proofs from Tests," IEEE Transactions on Software Engineering, vol. 36, no. 4, pp. 495-508, July-Aug. 2010, doi:10.1109/TSE.2010.49
Usage of this product signifies your acceptance of the Terms of Use.