Sciweavers

Share
SIGSOFT
2006
ACM

SYNERGY: a new algorithm for property checking

12 years 2 months ago
SYNERGY: a new algorithm for property checking
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 partiti...
Bhargav S. Gulavani, Thomas A. Henzinger, Yamini K
Added 20 Nov 2009
Updated 20 Nov 2009
Type Conference
Year 2006
Where SIGSOFT
Authors Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, Sriram K. Rajamani
Comments (0)
books