Proofs from Tests
- Nels E. Beckman ,
- Aditya Nori ,
- Sriram Rajamani ,
- Robert J. Simmons
Proceedings of the International Symposium on Software Testing and Analysis (ISSTA) |
Published by Association for Computing Machinery, Inc.
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.
Copyright © 2007 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org. The definitive version of this paper can be found at ACM's Digital Library --http://www.acm.org/dl/.