Proofs from tests
- 20 July 2008
- proceedings article
- Published by Association for Computing Machinery (ACM)
- Vol. 36 (4) , 3-14
- https://doi.org/10.1145/1390630.1390634
Abstract
We present an algorithm DASH to check if a program P satisfies a safety property phi. 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 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_alpha 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.Keywords
This publication has 17 references indexed in Scilit:
- Boogie: A Modular Reusable Verifier for Object-Oriented ProgramsPublished by Springer Nature ,2006
- CUTEPublished by Association for Computing Machinery (ACM) ,2005
- Model checking, testing and verification working togetherFormal Aspects of Computing, 2005
- Software Model Checking: Searching for Computations in the Abstract or the ConcretePublished by Springer Nature ,2005
- KISSPublished by Association for Computing Machinery (ACM) ,2004
- Abstractions from proofsPublished by Association for Computing Machinery (ACM) ,2004
- Counterexample Guided Abstraction Refinement Via Program ExecutionPublished by Springer Nature ,2004
- Syntactic Program Transformations for Automatic AbstractionPublished by Springer Nature ,2000
- Counterexample-Guided Abstraction RefinementPublished by Springer Nature ,2000
- The humble programmerCommunications of the ACM, 1972