The Community for Technology Leaders
Green Image
Issue No. 04 - July/August (2010 vol. 36)
ISSN: 0098-5589
pp: 495-508
Nels E. Beckman , Carnegie Mellon University, Pittsburgh
Sriram K. Rajamani , Microsoft Research India, Bangalore
Aditya V. Thakur , University of Wisconsin-Madison, Madison
Robert J. Simmons , Carnegie Mellon University, Pittsburgh
Aditya V. Nori , Microsoft Research India, Bangalore
Sai Deep Tetali , University of California, Los Angeles, Los Angeles
ABSTRACT
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.
INDEX TERMS
Software model checking, directed testing, abstraction refinement.
CITATION
Nels E. Beckman, Sriram K. Rajamani, Aditya V. Thakur, Robert J. Simmons, Aditya V. Nori, Sai Deep Tetali, "Proofs from Tests", IEEE Transactions on Software Engineering, vol. 36, no. , pp. 495-508, July/August 2010, doi:10.1109/TSE.2010.49
99 ms
(Ver )