The Java Modeling Language (JML)

Others Working on JML Tools

Besides the people working at Iowa State, there are several groups and individuals working on JML. The ones we know about are the following.

• Yoonsik Cheon's group at University of Texas at El Paso.
• The LOOP verification project from Bart Jacobs's SoS group at the Radboud University Nijmegen. This group includes Erik Poll and, over the years, Joachim van den Berg, Marieke Huisman, Engelbert Hubbers, Joe Kiniry, Martijn Oostdijk, Martijn Warnier, and several other contributors.
• Joe Kiniry's group at University College Dublin. This group includes or included contributors Julien Charles, Dermot Cochran, Vieri del Bianco, Fintan Fairmichael, Radu Grigore, Mikolas Janota, Alan Morkan, Dragan Stosic, and many others.
• The ESC/Java2 project, led by Joe Kiniry and David Cok.
• Michael D. Ernst's group at the University of Washington, which has produced the Daikon invariant detector and has worked on other tools and semantics relating to JML and Java, including testing tools, work on Java's type annotations (JSR 308), and the Checker Framework. This group includes Werner Dietl.
• Patrice Chalin's Dependable Software Research Group (DSRG), at Concordia University in Montreal, is working on language improvements (a new assertion semantics, non-null by default and arbitrary precision arithmetic) and their support in the Common (formerly ISU) JML tools and ESC/Java2. This group includes George Karabotsos and Perry James.
• David R. Cok (see pictures), who is an independent contributor, working at Kodak, who has worked on many tools, especially OpenJML, "jmldoc", "jmlspec", and ESC/Java2.
• The SpEx and JMLEclipse projects from the SAnToS Laboratory at Kansas State University, integrated by Matthew Dwyer, John Hatcliff, Robby, and Edwin Rodríguez. The SpEx project aims to extend JML to increase its suitability for the specification of concurrent programs. JMLEclipse is a JML front-end implemented as an Eclipse plugin.
• The KeY Project has theorem prover for Java Dynamic logic which includes a JML front end.
• Stephen Edwards's group at Virginia Tech, who are working on a tool that supports a wrapper approach to runtime assertion checking. This group includes Roy Tan.
• Marieke Huisman and collaborators in the Formal Methods and Tools Group at the University of Twente, Netherlands. Before, Marieke was part of the Everest team at INRIA Sophia-Antipolis, that developed the JACK: Java Applet Correctness Kit environment and the Bytecode Modeling Language (BML), a bytecode variation of JML.
• Jacek Chrzaszcz and Aleksy Schubert, at the Institute of Informatics of Warsaw University, Poland, who develop tools for BML.
• The Imdea Software group in Madrid, Spain, including Gilles Barthe, and Anindya Banerjee.
• Peter Müller at ETH Zurich and his students are working on the Universe type system. They also work on modular verification, including a treatment of frame axioms and a formal verification tool (Jive) that will use JML as its specification language.
• Arnd Poetzsch-Heffter and his students are working on modular verification, including a treatment of frame axioms and a formal verification tool (Jive) that will use JML as its specification language.
• David Naumann and his students are working on the semantics of JML and on using JML static verification tools to specify and check secure information flow properties.
• Claude Marché, Christine Paulin-Mohring, and Xavier Urbain in the Logical group at INRIA Futurs/Université Paris-Sud have produced the Krakatoa tool for verifying JML-annotated Java programs using the theorem prover Coq.
• The TFC (Constraint-based and Formal Techniques) group in Besançon works on Java/JML applications in two different directions. A testing activity, led by Bruno Legeard, works on adding JML/Java as an input to an existing framework for the symbolic animation and the automated test generation from formal models. A verification activity, led by Jacques Julliand, works on the automatic generation of JML annotations from proof obligations for verifying linear temporal properties.
• Tao Xie's group at North Carolina State University is working on testing and verification related projects.
• The Mobius project is a European Commission supported project that is using JML and developing "technology for establishing trust and security" using proof carrying code.
• The Extended Virtual Platform (XVP) project, directed by Suad Alagic, aims to support assertions at the virtual machine level.
• Christoph Csallner and Yannis Smaragdakis at Georgia Tech/University of Oregon.
• Frank Piessens's group at KU Leuven, Belgium, working on "concern-specific specification and verification to improve software quality and security." Besides Frank Piessens, this group includes Bart Jacobs (the younger).
• Timothy Wahls is working on execution of JML specifications (for rapid prototyping and debugging of specifications).
• The JML AOP project, in Ricardo Massa F. Lima's group at the Federal University of Pernambuco (UFPE) in Brazil. This includes Henrique Rebêlo, who is also working on adapting JML using aspect-oriented programming.
• The Contract Guided System Development (ConGu) project is led by Professor Vasco Vasconcelos at the Universidade de Lisboa. This project aims to support the checking of Java classes against property-driven algebraic specifications.
• Daniel Jackson's Software Design Group, which includes Greg Dennis and Kuat Yessenov, who have developed JForge, a front-end to their Forge bounded verification library, that automatically analyzes Java code against full JML specifications.
• Although now disbanded, an important original group working on JML was the former extended static checking project (which includes ESC/Java) at HP SRC Classic (formerly Compaq Systems Research Center). This group included K. Rustan M. Leino, Cormac Flanagan, Mark Lillibridge, Greg Nelson, Raymie Stata, James B. Saxe.

JML is an open project, and we welcome the participation of other groups. If your group is working on JML but not listed above, please send an email to Gary Leavens (leavens@eecs.ucf.edu).

Last modified Thursday, June 25, 2009.