Second JML Spec-a-thon, November 2009

The Second JML Spec-a-thon will be held on campus at University College Dublin (UCD) for three days, from Wednesday 18 November 2009 to Friday 20 November 2009, with additional activities preceding the event on Monday and Tuesday.

The Second JML Spec-a-thon is a continuation of the Inaugural Spec-a-thon held on 26-28 May 2009 at the University of Washington Tacoma, and is similar in spirit to the JML Winter School that was held in 2008, but is longer, more intense, and geared more toward output production and goal setting than toward education. As part of this Spec-a-thon, there will also be a "keynote"-like talk open to to the public at UCD.

The main focus for all Spec-a-thons is on writing good, usable specifications for many of the modern Java core classes that presently lack them. In OpenJML, we finally have a JML compiler that can take full advantage of generics and the other new language features introduced over the last several years, but the vast majority of available specs are still for Java 1.4 classes, lacking both generics and new APIs. Addressing this situation will help make JML more attractive to developers and more suitable for use in coursework.

The last Spec-a-thon had several super-short talks given by participants in the morning on their current work, available tools, techniques in specification writing, and more. The balance of the day, and often into the night, participants worked as individuals and in small groups on new tools, specifications, and documentation, gave tutorials to each other, and more. For some participants, some of each day also focused on "pair specification writing," which is basically a wacky combination of an OpenBSD Hackathon and formal methods "extreme programming".

A secondary focus of Spec-a-thons is on setting community-wide goals for the coming year in JML-related tool development and research. The second half of 2009 has been a great time for JML, with the Inaugural Spec-a-thon in late May and the Dagstuhl seminar in July. Continued face-to-face coordination of the goals of the JML community can only be helpful.

The Second JML Spec-a-thon is supported by a Formal Methods Europe Small Projects award, as well as local research grants at University College Dublin. There is also an opportunity for students and researchers involved with COST Action IC0701 "Formal Verification of Object-Oriented Software" to participate using COST funds. Participants in this latter category will be obligated to attend the full week of Spec-a-thon activities due to funding agency restrictions. This support allows us to offer travel subsidies to attendees (exact amounts to be determined, but most likely in the $200 to $500 range, similar to the Inaugural Spec-a-thon).

There are currently 13 registered attendees (including the organizers). If you are interested in registering, email jmlspecs dash specathon at lists dot sourceforge dot net.

Information about local accommodations (not yet available), an attendee list and the event schedule (including talks) can be found on dedicated pages.