An eclipse plug-in for model checking
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.
Download
No fulltext has been uploaded. References only!
Conference Paper
| Published
| English
Scopus indexed
Author
Beyer, Dirk;
Henzinger, Thomas AISTA
;
Jhala, Ranjit;
Majumdar, Ritankar
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.
Publishing Year
Date Published
2004-07-12
Proceedings Title
Proceedings of the 12th IEEE International Workshop on Program Comprehension
Publisher
IEEE
Acknowledgement
This research was supported in part by the NSF grants CCR-0085949, CCR-0234690, and ITR-0326577.
Page
251 - 255
Conference
IWPC: Program Comprehension
Conference Location
Bari, Italy
Conference Date
2004-06-26 – 2004-06-26
ISBN
ISSN
IST-REx-ID
Cite this
Beyer D, Henzinger TA, Jhala R, Majumdar R. An eclipse plug-in for model checking. In: Proceedings of the 12th IEEE International Workshop on Program Comprehension. IEEE; 2004:251-255. doi:10.1109/WPC.2004.1311069
Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2004). An eclipse plug-in for model checking. In Proceedings of the 12th IEEE International Workshop on Program Comprehension (pp. 251–255). Bari, Italy: IEEE. https://doi.org/10.1109/WPC.2004.1311069
Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “An Eclipse Plug-in for Model Checking.” In Proceedings of the 12th IEEE International Workshop on Program Comprehension, 251–55. IEEE, 2004. https://doi.org/10.1109/WPC.2004.1311069 .
D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “An eclipse plug-in for model checking,” in Proceedings of the 12th IEEE International Workshop on Program Comprehension, Bari, Italy, 2004, pp. 251–255.
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.
Beyer, Dirk, et al. “An Eclipse Plug-in for Model Checking.” Proceedings of the 12th IEEE International Workshop on Program Comprehension, IEEE, 2004, pp. 251–55, doi:10.1109/WPC.2004.1311069 .