---
OA_type: closed access
_id: '4581'
abstract:
- lang: eng
  text: We have extended the software model checker BLAST to automatically generate
    test suites that guarantee full coverage with respect to a given predicate. More
    precisely, given a C program and a target predicate p, BLAST determines the set
    L of program locations which program execution can reach with p true, and automatically
    generates a set of test vectors that exhibit the truth of p at all locations in
    L. We have used BLAST to generate test suites and to detect dead code in C programs
    with up to 30 K lines of code. The analysis and test vector generation is fully
    automatic (no user intervention) and exact (no false positives).
article_processing_charge: No
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- first_name: Adam
  full_name: Chlipala, Adam
  last_name: Chlipala
- 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: Ranjit
  full_name: Jhala, Ranjit
  last_name: Jhala
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
citation:
  ama: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. Generating tests from
    counterexamples. In: <i>Proceedings of the 26th International Conference on Software
    Engineering</i>. IEEE; 2004:326-335. doi:<a href="https://doi.org/10.1109/ICSE.2004.1317455">10.1109/ICSE.2004.1317455</a>'
  apa: 'Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004).
    Generating tests from counterexamples. In <i>Proceedings of the 26th International
    Conference on Software Engineering</i> (pp. 326–335). Edinburgh, United Kingdom:
    IEEE. <a href="https://doi.org/10.1109/ICSE.2004.1317455">https://doi.org/10.1109/ICSE.2004.1317455</a>'
  chicago: Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar
    Majumdar. “Generating Tests from Counterexamples.” In <i>Proceedings of the 26th
    International Conference on Software Engineering</i>, 326–35. IEEE, 2004. <a href="https://doi.org/10.1109/ICSE.2004.1317455">https://doi.org/10.1109/ICSE.2004.1317455</a>.
  ieee: D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “Generating
    tests from counterexamples,” in <i>Proceedings of the 26th International Conference
    on Software Engineering</i>, Edinburgh, United Kingdom, 2004, pp. 326–335.
  ista: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. Generating
    tests from counterexamples. Proceedings of the 26th International Conference on
    Software Engineering. ICSE: Software Engineering, 326–335.'
  mla: Beyer, Dirk, et al. “Generating Tests from Counterexamples.” <i>Proceedings
    of the 26th International Conference on Software Engineering</i>, IEEE, 2004,
    pp. 326–35, doi:<a href="https://doi.org/10.1109/ICSE.2004.1317455">10.1109/ICSE.2004.1317455</a>.
  short: D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings
    of the 26th International Conference on Software Engineering, IEEE, 2004, pp.
    326–335.
conference:
  end_date: 2004-05-28
  location: Edinburgh, United Kingdom
  name: 'ICSE: Software Engineering'
  start_date: 2004-05-23
date_created: 2018-12-11T12:09:35Z
date_published: 2004-07-26T00:00:00Z
date_updated: 2026-05-29T07:46:59Z
day: '26'
doi: 10.1109/ICSE.2004.1317455
extern: '1'
fulldoi: https://doi.org/10.1109/ICSE.2004.1317455
language:
- iso: eng
month: '07'
oa_version: None
page: 326 - 335
publication: Proceedings of the 26th International Conference on Software Engineering
publication_identifier:
  isbn:
  - '0769521630'
  issn:
  - 0270-5257
publication_status: published
publisher: IEEE
publist_id: '128'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Generating tests from counterexamples
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...