• G.: An integrated verification...

*Result*: G.: An integrated verification environment for JML: Architecture and early results

Title:
G.: An integrated verification environment for JML: Architecture and early results
Authors:
Patrice Chalin, Perry R. James, George Karabotsos
Contributors:
The Pennsylvania State University CiteSeerX Archives
Source:
http://www.cs.iastate.edu/~leavens/SAVCBS/2007/papers/Chalin-James-Karabotsos.pdf.
Publication Year:
2007
Collection:
CiteSeerX
Subject Terms:
Design, Languages, Theory, Verification. Keywords Integrated Verification Environment, Java Modeling Language, Eclipse, JML4
Document Type:
*Academic Journal* text
File Description:
application/pdf
Language:
English
Relation:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.7340
Availability:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.120.7340
http://www.cs.iastate.edu/~leavens/SAVCBS/2007/papers/Chalin-James-Karabotsos.pdf
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.F8CBAB5
Database:
BASE

*Further Information*

*Tool support for the Java Modeling Language (JML) is a very pressing problem. A main issue with current tools is their architecture: the cost of keeping up with the evolution of Java is prohibitively high: e.g., almost three years following its release, Java 5 has yet to be fully supported. This paper presents the architecture of JML4, an Integrated Verification Environment (IVE) for JML that builds upon Eclipse’s support for Java, enhancing it with Extended Static Checking (ESC), an early form of Runtime Assertion Checking (RAC) and JML’s non-null type system. Early results indicate that the synergy of complementary verification techniques (being made available within a single tool) can help developers be more effective; we demonstrate new bugs uncovered in JML annotated Java source—like ESC/Java2— which is routinely verified using first generation JML tools.*