--- res: bibo_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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Dirk foaf_name: Beyer, Dirk foaf_surname: Beyer - foaf_Person: foaf_givenName: Thomas A foaf_name: Thomas Henzinger foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000−0002−2985−7724 - foaf_Person: foaf_givenName: Ranjit foaf_name: Jhala, Ranjit foaf_surname: Jhala - foaf_Person: foaf_givenName: Ritankar foaf_name: Majumdar, Ritankar S foaf_surname: Majumdar bibo_doi: '10.1109/WPC.2004.1311069 ' dct_date: 2004^xs_gYear dct_publisher: IEEE@ dct_title: An eclipse plug-in for model checking@ ...