loading...
An Eclipse Plug-in for Model Checking
Bari, Italy June 24-June 26
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/WPC.2004.131106912th IEEE International Workshop on P ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, "An Eclipse Plug-in for Model Checking," International Conference on Program Comprehension, pp. 251, 12th IEEE International Workshop on Program Comprehension (IWPC'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/WPC.2004.1311069,
author = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar},
title = {An Eclipse Plug-in for Model Checking},
journal ={International Conference on Program Comprehension},
volume = {0},
year = {2004},
issn = {1092-8138},
pages = {251},
doi = {http://doi.ieeecomputersociety.org/10.1109/WPC.2004.1311069},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - International Conference on Program Comprehension
TI - An Eclipse Plug-in for Model Checking
SN - 1092-8138
SP
EP
A1 - Dirk Beyer,
A1 - Thomas A. Henzinger,
A1 - Ranjit Jhala,
A1 - Rupak Majumdar,
PY - 2004
KW - null
VL - 0
JA - International Conference on Program Comprehension
ER -
 
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
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.
Citation:
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, "An Eclipse Plug-in for Model Checking," icpc, pp.251, 12th IEEE International Workshop on Program Comprehension (IWPC'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.