SYNERGY : A New Algorithm for Property Checking

The property checking problem is to check if a program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking have been proposed: (1) testing and (2) verification. Testing tries to find inputs and executions that demonstrate violations to the property. Verification tries to find proofs that all executions of the program satisfy the property. Testing works when errors are easy to find, and verification works when proofs are easy to find. Testing is typically inefficient for correct programs, and verification methods are typically inefficient at finding errors. We propose a new algorithm, SYNERGY, that combines testing and verification. SYNERGY generalizes several disparate algorithms in the literature including: (1) counterexample driven refinement approaches for verification (such as SLAM, BLAST, MAGIC), (2) directed testing approaches (such as DART) and (3) partition refinement approaches (such as Paige-Tarjan and Lee-Yannakakis) algorithms). This paper presents a description of the SYNERGY algorithm, its theoretical properties, detailed comparison with related algorithms, and a prototype implementation in a tool — YOGI.