Proofs from Tests

We present an algorithm Dash to check if a program P satisfies a safety property ϕ. The unique feature of the algorithm is that it uses only test generation operations, and nes 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 WPα that uses only the alias information obtained by executing a test ne abstractions in a sound manner. We present a full exposition of the Dash algorithm, its theoretical properties, and its implementation. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification—Correctness proofs, Model checking; D.2.5 [Software Engineering]: Testing Tools—Symbolic execution General Terms Testing, Verification Keywords Software model checking; Directed testing; Abstraction refinement

• Type: Journal
• Year: 2010
• Where: TSE
• Authors: Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, Robert J. Simmons, SaiDeep Tetali, Aditya V. Thakur
• Keywords: Abstraction, Algorithm, Test Generation Operations, TSE 2010