Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 09292

The Java Modeling Language (JML)

( Jul 12 – Jul 17, 2009 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:





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

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.

  • Bernhard Beckert (Universität Koblenz-Landau, DE) [dblp]
  • Richard Bubel (Chalmers UT - Göteborg, SE) [dblp]
  • Patrice Chalin (Concordia University - Montreal, CA)
  • Curtis Clifton (Rose-Hulman Inst. of Technology - Terre Haute, US)
  • David Cok (Eastman Kodak Comp. - Rochester, US) [dblp]
  • Cormac Flanagan (University of California - Santa Cruz, US) [dblp]
  • Reiner Hähnle (Chalmers UT - Göteborg, SE) [dblp]
  • John Hatcliff (Kansas State University, US) [dblp]
  • Görel Hedin (Lund University, SE) [dblp]
  • Marieke Huisman (University of Twente, NL) [dblp]
  • James J. Hunt (aicas GmbH - Karlsruhe, DE) [dblp]
  • Joseph Roland Kiniry (University College Dublin, IE) [dblp]
  • Gary T. Leavens (University of Central Florida - Orlando, US) [dblp]
  • Jooyong Lee (Kansas State University, US)
  • K. Rustan M. Leino (Microsoft Corporation - Redmond, US) [dblp]
  • Rosemary Monahan (NUI Maynooth, IE) [dblp]
  • Wojciech Mostowski (Radboud University Nijmegen, NL) [dblp]
  • Peter Müller (ETH Zürich, CH) [dblp]
  • David A. Naumann (Stevens Institute of Technology, US) [dblp]
  • Frank Piessens (KU Leuven, BE) [dblp]
  • Erik Poll (Radboud University Nijmegen, NL) [dblp]
  • Robby (Kansas State University, US) [dblp]
  • Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Isabel Tonin (aicas GmbH - Karlsruhe, DE)
  • Mattias Ulbrich (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Ronny Wichers Schreur (Radboud University Nijmegen, NL)
  • Daniel Zimmerman (University of Washington - Tacoma, US)

  • programming languages/compiler
  • semantics/formal methods
  • sw-engineering
  • verification/logic

  • specification language
  • formal methods
  • verification