OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
arXiv:1404.6608 · doi:10.4204/EPTCS.149.8
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.
In Proceedings F-IDE 2014, arXiv:1404.5785
References in corpus (2)
Cited by in corpus (9)
- The Dafny Integrated Development Environment
- VerifyThis 2019: A Program Verification Competition (Extended Report)
- Verifying Functional Correctness Properties At the Level of Java Bytecode
- SPEEDY: An Eclipse-based IDE for invariant inference
- Formal Reasoning Using an Iterative Approach with an Integrated Web IDE
- Explaining Counterexamples with Giant-Step Assertion Checking
- Reasoning About Exceptional Behavior At the Level of Java Bytecode
- Next Steps in LLM-Supported Java Verification
- Treating for-Loops as First-Class Citizens in Proofs