@inproceedings{beckman2008proofs,
author = {Beckman, Nels E. and Nori, Aditya and Rajamani, Sriram and Simmons, Robert J.},
title = {Proofs from Tests},
booktitle = {Proceedings of the International Symposium on Software Testing and Analysis (ISSTA)},
year = {2008},
month = {July},
abstract = {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.},
publisher = {Association for Computing Machinery, Inc.},
url = {http://approjects.co.za/?big=en-us/research/publication/proofs-from-tests-2/},
edition = {Proceedings of the International Symposium on Software Testing and Analysis (ISSTA)},
}