Program verification has been a topic of research interest far into the history of computing science. Today, it is still a key research focus, see e.g., Hoare’s Verified Compiler Grand Challenge and the Verified Software Initiative. A main facet in this effort is the ability to formally express properties that must be verified. Building on a long line of work in formal methods for reasoning about behavioral specifications of programs, several recent languages balance the desire for completeness and the pragmatics of checkability. In the context of the object-oriented programming paradigm, the Java Modeling Language (JML) is the most widely-adopted specification language in the Java formal methods research community.

The Java Modeling Language (JML) is a formal, behavioral specification language for Java. It describes detailed designs of Java classes and interfaces using pre- and postconditions, invariants, and several more advanced features. JML is used as a common language for many research projects and tools, including a runtime assertion checker (jmlc), tools to help unit testing (jmlunit), an extended static checker (ESC/Java), and several formal verification tools (e.g., LOOP, JACK, KRAKATOA, Jive, and KeY). JML is seeing some use in industry,particularly for financial applications on Java Smart cards and for verifying some security properties of a computer-based voting system.

Since JML is widely understood in the formal methods research community, it provides a shared notation for communicating and comparing many advances, both theoretical and practical, and it serves as a launching pad for research on advanced specification language features and tools. Researchers are using JML to study or express results for a wide variety of problems; these problems include verification logics, side effects (including frame axioms and modifies clauses), invariants, behavioral subtyping, null pointer dereferences, interfacing with theorem provers, information hiding, specifying call sequences in frameworks, multithreading, compilation, resource usage, and security. In addition to the tools mentioned above, JML is also used to express, compare, or study tools for checking specifications, unit testing, and specification inference. JML is used to state research problems for formal specification languages and for general discussions of specification language design. JML has also inspired at least three other similar specification languages, Spec#, BML, and Pipa, and has influenced the design and tools for Eiffel. Representatives of these communities are included in the invitation list. JML tools are used in the implementation of at least two other specification languages: ConGu and Circus. At present, there are at least 19 research groups around the world that are cooperating on JML-related research. These groups, and others, have published well over 100 papers directly related to JML (see www.jmlspecs.org/papers.shtml).

The seminar will pull together and energize the broad community of JML researchers and developers. We plan to have seminar participants work together on JML’s documentation, examples, pedagogical materials, and implementation infrastructure. The meeting will also provide a forum for considering changes to the language, for organizing community efforts, and for discussing recent work on formal methods relating to JML and its semantics. We plan to have fewer talks than an average Dagstuhl seminar and much more interaction and working sessions. We intend to involve the participants in writing documentation, examples, teaching materials, and library specifications. They will also discuss and debug software infrastructure and a novel semantics for JML. In addition, they will discuss and help organize the JML community.