## Synergy: A New Algorithm for Property Checking

*Bhargav Gulavani,
Thomas A. Henzinger,
Yamini Kannan, Aditya Nori, and Sriram K. Rajamani*

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.

*Proceedings of the
14th Annual Symposium on Foundations of Software Engineering*
(FSE), ACM Press, 2006, pp. 117-127.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2006 ACM.