Proofs from Tests

Nels E. Beckman, Aditya V. Nori, Sriram K. Rajamani, and Robert J. Simmons


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.


Publication typeInproceedings
Published inProceedings of the International Symposium on Software Testing and Analysis (ISSTA)
PublisherAssociation for Computing Machinery, Inc.
> Publications > Proofs from Tests