---
OA_type: closed access
_id: '4577'
abstract:
- lang: eng
  text: While model checking has been successful in uncovering subtle bugs in code,
    its adoption in software engineering practice has been hampered by the absence
    of a simple interface to the programmer in an integrated development environment.
    We describe an integration of the software model checker BLAST into the Eclipse
    development environment. We provide a verification interface for practical solutions
    for some typical program analysis problems - assertion checking, reachability
    analysis, dead code analysis, and test generation - directly on the source code.
    The analysis is completely automatic, and assumes no knowledge of model checking
    or formal notation. Moreover, the interface supports incremental program verification
    to support incremental design and evolution of code.
acknowledgement: This research was supported in part by the NSF grants CCR-0085949,
  CCR-0234690, and ITR-0326577.
article_processing_charge: No
author:
- first_name: Dirk
  full_name: Beyer, Dirk
  last_name: Beyer
- 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, Henzinger TA, Jhala R, Majumdar R. An eclipse plug-in for model checking.
    In: <i>Proceedings of the 12th IEEE International Workshop on Program Comprehension</i>.
    IEEE; 2004:251-255. doi:<a href="https://doi.org/10.1109/WPC.2004.1311069  ">10.1109/WPC.2004.1311069 
    </a>'
  apa: 'Beyer, D., Henzinger, T. A., Jhala, R., &#38; Majumdar, R. (2004). An eclipse
    plug-in for model checking. In <i>Proceedings of the 12th IEEE International Workshop
    on Program Comprehension</i> (pp. 251–255). Bari, Italy: IEEE. <a href="https://doi.org/10.1109/WPC.2004.1311069 
    ">https://doi.org/10.1109/WPC.2004.1311069  </a>'
  chicago: Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “An
    Eclipse Plug-in for Model Checking.” In <i>Proceedings of the 12th IEEE International
    Workshop on Program Comprehension</i>, 251–55. IEEE, 2004. <a href="https://doi.org/10.1109/WPC.2004.1311069 
    ">https://doi.org/10.1109/WPC.2004.1311069  </a>.
  ieee: D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “An eclipse plug-in
    for model checking,” in <i>Proceedings of the 12th IEEE International Workshop
    on Program Comprehension</i>, Bari, Italy, 2004, pp. 251–255.
  ista: 'Beyer D, Henzinger TA, Jhala R, Majumdar R. 2004. An eclipse plug-in for
    model checking. Proceedings of the 12th IEEE International Workshop on Program
    Comprehension. IWPC: Program Comprehension, 251–255.'
  mla: Beyer, Dirk, et al. “An Eclipse Plug-in for Model Checking.” <i>Proceedings
    of the 12th IEEE International Workshop on Program Comprehension</i>, IEEE, 2004,
    pp. 251–55, doi:<a href="https://doi.org/10.1109/WPC.2004.1311069  ">10.1109/WPC.2004.1311069 
    </a>.
  short: D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Proceedings of the
    12th IEEE International Workshop on Program Comprehension, IEEE, 2004, pp. 251–255.
conference:
  end_date: 2004-06-26
  location: Bari, Italy
  name: 'IWPC: Program Comprehension'
  start_date: 2004-06-26
date_created: 2018-12-11T12:09:34Z
date_published: 2004-07-12T00:00:00Z
date_updated: 2026-05-29T08:23:32Z
day: '12'
doi: '10.1109/WPC.2004.1311069  '
extern: '1'
fulldoi: 'https://doi.org/10.1109/WPC.2004.1311069  '
language:
- iso: eng
month: '07'
oa_version: None
page: 251 - 255
publication: Proceedings of the 12th IEEE International Workshop on Program Comprehension
publication_identifier:
  isbn:
  - '0769521495'
  issn:
  - 1092-8138
publication_status: published
publisher: IEEE
publist_id: '129'
quality_controlled: '1'
scopus_import: '1'
status: public
title: An eclipse plug-in for model checking
type: conference
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2004'
...