The Java Modeling Language(JML) is a formal specification language that can document detailed designs of Java classes and interfaces. JML has been used by many formal methods researchers in different projects such as the ESC/Java extended static checker, the Daikon invariant detector,the Bogor model-checking framework, and others.
The award from the National Science Foundation to the PI: Gary T. Leavens and Co-PIs Hridesh Rajan and Samik Basu provides support for research aimed at enhancing the JML infrastructure including its type checker, runtime assertion checking compiler, and IDE support. The project will also make JML's software infrastructure more extensible and substantially improve the documentation of the language and its supporting tools.
More information about this project is available here. This is an ongoing project in the Department of Computer Science.