SYNERGY

TLDR

Property checking for programs with infinite state spaces is undecidable, and while testing can uncover violations, it struggles with coverage, whereas verification can prove correctness but often fails to find errors efficiently. The authors introduce Synergy, an algorithm that integrates testing and verification techniques. Synergy merges counterexample‑guided model checking, directed testing, and partition refinement, and is implemented in the prototype Yogi. The paper demonstrates Synergy’s theoretical properties, compares it to related algorithms, and presents its implementation in Yogi.

Abstract

We consider the problem if a given 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 are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi.