Towards an industrial grade IVE for Java and next generation research platform for JML

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., Java 5 has yet to be fully supported. This paper presents JML4, our proposal for an Integrated Verification Environment (IVE) for JML that builds upon Eclipse’s support for Java, enhancing it with Runtime Assertion Checking (RAC), Extended Static Checking (ESC) and Full Static Program Verification (FSPV). Though it currently only supports a subset of JML, we believe that JML4 is the first IVE to support such a full range of verification techniques for a mainstream programming language.

• Type: Journal
• Year: 2010
• Where: STTT
• Authors: Patrice Chalin, Robby, Perry R. James, Jooyong Lee, George Karabotsos
• Keywords: Java, Java Modeling Language, Static Program Verification, STTT 2010