An eclipse plug-in for model checking

Author

Beyer, Dirk ; Henzinger, Thomas A. ; Jhala, Ranjit ; Majumdar, Rupak

Author_Institution

Dept. of Electr. Eng. & Comput. Sci., California Univ., Berkeley, CA, USA

fYear

2004

fDate

24-26 June 2004

Firstpage

251

Lastpage

255

Abstract

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.

Keywords

formal verification; program diagnostics; programming environments; BLAST; Eclipse development environment; assertion checking; dead code analysis; eclipse plug-in; incremental design; incremental program verification; integrated development environment; model checking; program analysis; reachability analysis; software engineering; test generation; verification interface; Computer interfaces; Computer science; Explosions; Programming profession; Reachability analysis; Reliability engineering; Runtime; Software engineering; Software quality; Testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Program Comprehension, 2004. Proceedings. 12th IEEE International Workshop on

ISSN

1092-8138

Print_ISBN

0-7695-2149-5

Type

conf

DOI

10.1109/WPC.2004.1311069

Filename

1311069