Published Articles >> Table of Contents >> Abstract

12th IEEE International Workshop on Program Comprehension (IWPC'04)   p. 251
An Eclipse Plug-in for Model Checking
Dirk Beyer, University of California, Berkeley
Thomas A. Henzinger, University of California, Berkeley
Ranjit Jhala, University of California, Berkeley
Rupak Majumdar, University of California, Los Angeles

Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/WPC.2004.1311069
Send link to a friend

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.
Back to Top Additional Information
Citation:  Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, "An Eclipse Plug-in for Model Checking," iwpc, p. 251,  12th IEEE International Workshop on Program Comprehension (IWPC'04),  2004