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 iteration of the algorithm is extremely inexpensive, and can be implemented without any extra theorem prover calls and without any global may-alias information. In particular, we introduce a new refinement operator WP_α 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. Our empirical results show significant improvement over SLAM in the runtimes of several examples. We also show several cases where SLAM is unable to terminate due to pointer analysis imprecisions, whereas DASH is able to terminate in seconds.

PDF file

Details