Formal-methods tools: proof assistants, model checking, symbolic execution etc.
- CATG - Concolic unit testing engine. Automatically generates unit tests using formal methods.
- Checker Framework - Pluggable type systems. Includes nullness types, physical units, immutability types and more.
- Daikon - Daikon detects likely program invariants and can generate JML specs based on those invariats.
- Java Path Finder (JPF) - JVM formal verification tool containing a model checker and more. Created by NASA.
- JMLOK 2.0 - Detects nonconformances between code and JML specification through the feedback-directed random tests generation, and suggests a likely cause for each nonconformance detected.
- KeY - The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. Uses JML for specification and symbolic execution for verification.
- OpenJML - Translates JML specifications into SMT-LIB format and passes the proof problems implied by the program to backend solvers.