Proofs from Tests - Beckman, Nels E.; Nori, Aditya; Rajamani, Sriram; Simmons, Robert J. (Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), 2008)
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 it refines and maintains a sound program abstraction as a consequence of failed test generation operations. Thus, each teration of the algorithm is inexpensive, and can be implemented without any global may-alias information. In particular, we introduce a new refinement operator WPalpha that uses only the alias information obtained by executing a test to refine abstractions in a sound manner. We present a full exposition of the Dash algorithm, its theoretical properties, and its implementation.