OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
David R. Cok (GrammaTech, Inc.)
TL;DR
OpenJML is a tool that integrates Java program verification with JML specifications directly into Eclipse, demonstrating practical use in education and small-scale Java program analysis.
Contribution
It presents an integrated verification tool for Java 7 using JML, OpenJDK, and Eclipse, emphasizing IDE integration and automation in specification-based verification.
Findings
Used in college courses for teaching verification
Applied to small Java programs for verification tasks
Demonstrates the feasibility of integrated verification tools
Abstract
OpenJML is a tool for checking code and specifications of Java programs. We describe our experience building the tool on the foundation of JML, OpenJDK and Eclipse, as well as on many advances in specification-based software verification. The implementation demonstrates the value of integrating specification tools directly in the software development IDE and in automating as many tasks as possible. The tool, though still in progress, has now been used for several college-level courses on software specification and verification and for small-scale studies on existing Java programs.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.