---
OA_type: closed access
_id: '4523'
abstract:
- lang: eng
  text: 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.
article_processing_charge: No
author:
- first_name: Bhargav
  full_name: Gulavani, Bhargav
  last_name: Gulavani
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Yamini
  full_name: Kannan, Yamini
  last_name: Kannan
- first_name: Aditya
  full_name: Nori, Aditya
  last_name: Nori
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. Synergy: A new algorithm
    for property checking. In: <i>Proceedings of the 14th ACM SIGSOFT International
    Symposium on Foundations of Software Engineering</i>. ACM; 2006:117-127. doi:<a
    href="https://doi.org/10.1145/1181775.1181790">10.1145/1181775.1181790</a>'
  apa: 'Gulavani, B., Henzinger, T. A., Kannan, Y., Nori, A., &#38; Rajamani, S. (2006).
    Synergy: A new algorithm for property checking. In <i>Proceedings of the 14th
    ACM SIGSOFT international symposium on Foundations of software engineering</i>
    (pp. 117–127). Portland, Oregon, United States: ACM. <a href="https://doi.org/10.1145/1181775.1181790">https://doi.org/10.1145/1181775.1181790</a>'
  chicago: 'Gulavani, Bhargav, Thomas A Henzinger, Yamini Kannan, Aditya Nori, and
    Sriram Rajamani. “Synergy: A New Algorithm for Property Checking.” In <i>Proceedings
    of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering</i>,
    117–27. ACM, 2006. <a href="https://doi.org/10.1145/1181775.1181790">https://doi.org/10.1145/1181775.1181790</a>.'
  ieee: 'B. Gulavani, T. A. Henzinger, Y. Kannan, A. Nori, and S. Rajamani, “Synergy:
    A new algorithm for property checking,” in <i>Proceedings of the 14th ACM SIGSOFT
    international symposium on Foundations of software engineering</i>, Portland,
    Oregon, United States, 2006, pp. 117–127.'
  ista: 'Gulavani B, Henzinger TA, Kannan Y, Nori A, Rajamani S. 2006. Synergy: A
    new algorithm for property checking. Proceedings of the 14th ACM SIGSOFT international
    symposium on Foundations of software engineering. FSE: Foundations of Software
    Engineering, 117–127.'
  mla: 'Gulavani, Bhargav, et al. “Synergy: A New Algorithm for Property Checking.”
    <i>Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations
    of Software Engineering</i>, ACM, 2006, pp. 117–27, doi:<a href="https://doi.org/10.1145/1181775.1181790">10.1145/1181775.1181790</a>.'
  short: B. Gulavani, T.A. Henzinger, Y. Kannan, A. Nori, S. Rajamani, in:, Proceedings
    of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering,
    ACM, 2006, pp. 117–127.
conference:
  end_date: 2006-11-11
  location: Portland, Oregon, United States
  name: 'FSE: Foundations of Software Engineering'
  start_date: 2006-11-05
date_created: 2018-12-11T12:09:18Z
date_published: 2006-01-01T00:00:00Z
date_updated: 2026-08-21T10:54:37Z
day: '01'
doi: 10.1145/1181775.1181790
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 117 - 127
publication: Proceedings of the 14th ACM SIGSOFT international symposium on Foundations
  of software engineering
publication_identifier:
  isbn:
  - '9781595934680'
publication_status: published
publisher: ACM
publist_id: '206'
status: public
title: 'Synergy: A new algorithm for property checking'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2006'
...