JML Workshop 2016 – Bad Herrenalb

JML  meets  Black Forest Cake

International Working Meeting on the Java Modeling Language
Java Modeling Language (JML):
Specification Language Semantics and Use Cases
Wednesday 2 – Friday 4 November 2016
Bad Herrenalb, Germany
The workshop continues the series of JML workshops which already took place in Dagstuhl, Shonan, and Leiden.

Minutes: jml-workshop-2016-minutes.pdf


General Information · Programme · Travel information · Dinner

Scientific Topic

This workshop will put a particular focus on the semantics of JML in face of its diverse application areas like runtime assertion checking, regression testing, static checking, and interactive verification. A preliminary semantical framework will enable us to look into and discuss issues in the semantics of JML. We aim at refinement of the semantical framework targetted an appendix to the JML reference manual.

Moreover, the agenda will also cover the following points:

  • Keeping up with time: JML and Java language features,
  • Broadening horizons: Specifying security (information flow) or concurrency (locksets, permissions) with JML
  • Outlook on tool support
  • A book on JML: Exploring its potential

Venue

This year's JML meeting will take place in a convention centre ("Haus der Kirche") in Bad Herrenalb, a scenic town with 7500 inhabitants in the northern Black Forest, less than 30 km south of Karlsruhe. The centre provides wireless internet access.

The Convention Centre "Haus der Kirche" belongs to the Protestant Church of Baden and combines the expectations of a modern convention and teaching centre with the Christian tradition of hospitality. The centre has been certified by the German Hotel Association and by EMAS (Eco-Managemant and Audit Scheme).

Costs

The workshop fee will be approx. 180€ covering the costs for accomodation (two nights), meals, and facilities in the convention centre. If you stay fewer or more nights, the costs will change accordingly. The costs are directly paid at the center on check-in.

Organisers

David Cok (GrammaTech)
Marieke Huisman (U Twente)
Gary Leavens (UCF)
Mattias Ulbrich (KIT)

Preliminary Programme

– Program Schedule as of October 31, 2016 –

Download Programme as PDF

Wednesday, November 2nd

9.30 – 10.00

– Welcome coffees with snack (Bretzeln) –

10.00 – 11.15

Welcome

JML Tools

David Cok: OpenJML status and outlook (30 min)

Dominic Scheurer: KeY status and outlook (30 min)

11.15 – 11.30

– Break –

11.30 – 12.30

Combining Approaches and Tools

Nikolai Kosmatov: Combinations of static and dynamic analyses in Frama-C (45 min)

Discussion: Combination of JML approaches and tools

12.30 – 14.00

– Lunch –

14.00 – 15.00

JML Semantics

Mattias Ulbrich: Proposition of a semantical framework for JML (45 min)

Discussion

15.00 – 15.15

– Break –

15.15 – 15.45

Breakout discussions

15.45 – 16.00

– Break –

16.00 – 18.00

Presentation of group results and plenum discussion

Discussion: Where and how should a formal semantics for JML be anchored?

Thursday, November 3rd

9.15 – 10.30

Broadening Horizons

Gary Leavens: Specifying and Verifying Advanced Control Features (45 min)

John Singleton: A Layered System for Specification Authoring, Sharing, and Usage (30 min)

10.30 – 11.00

– Break –

11.00 – 12.30

Mihai Herda: Specifying Information Flow Properties in KeY (30 min)

Short Exchange on specification of security properties

Malte Schwerhoff: Viper’s support for iterated separating conjunctions (30 min)

Short Exchange on specification of concurrency properties

12.30 – 14.00

– Lunch –

14.00 – 15.30

Discussion: What specification artifacts should we add in future versions of JML?

How can we deal with Java 5 and later?

15.30 – 16.00

– Break –

16.00 – 17.30

Extending the Reach

JML (and similar) in teaching:

Experience reports, tools, literature, examples, exercises, assignments, a common repository, …

JML (and similar) in industry:

Experiences, expectations, contacts, …

18.40

(Meeting at front door to walk to restaurant)

19.00 – 21.00

Dinner at Klosterscheuer (klosterscheuer.de)

Friday, November 4th

9.00 – 10.30

The Framing Challenge

Yuyan Bao: Unified Fine-Grained Region Logic as a Foundation for Framing JML (30 min)

Discussion: Specifying Frames in JML, class invariant semantics

Open discussion points

10.30 – 11.00

– Break –

11.00 – 12.30

A book on JML:

Discussion about benefits, required and available resources, possible format, contents, authors, ….

Discussion and decisions about next steps and the next meeting

Closing

12.30 – 14.00

– Lunch –


Travel Information

Bad Herrenalb is approx. 24 km south of Karlsruhe downtown.

The address of the centre is: Haus der Kirche - Evangelische Akademie Baden, Dobler Str. 51, 76332 Bad Herrenalb

Arriving by public transport

Karlsruhe is connected to the high-speed train net (ICE) and can be reached from the nearest aiports Frankfurt/Main and Stuttgart. In Karlsruhe catch a commuter train "S1 Ettlingen/Bad Herrenalb" which departs in front of the main station. The terminal stop is Bad Herrenalb (sometimes you have to change in Ettlingen). Tickets can be bought on the train from a ticket machine (4,70€, cash only).

Caution: The first of November is a public holiday in the state of Baden-Württemberg. Train service is according to the Sunday schedule. You can plan your journal at bahn.de.

Arriving by car

Coming from Frankfurt or Basle, take Autobahn A5, exit "Ettlingen", then follow signs to "Bad Herrenalb".
Coming from Stuttgart, take Autobahn A8, exit "Karlsbad/Bad Herrenalb", then follow signs to "Bad Herrenalb".

Caution: There are closed roads and diversions within Bad Herrenalb due to an upcoming garden exhibition in 2017.

Walk from the train station (Bahnhof Bad Herrenalb) (approx. 5-10 min)

Click to enlarge
Click to enlarge

The convention center is situated behind the church St. Bernhard at the mountain towards Dobel. The red sandstone church is already visible from the station Bad Herrenalb.

We recommend to take the Bahnhofstraße at the mini-golf course from the station towards Ettlingerstraße. At Ettlingerstraße cross the street at the pedestrian crossing and turn left to continue on Bleichweg for approx. 50m. Then turn right into Flachstreichweg and continue until the end of the road.

The convention center is situated at your right-hand side on the hill. Please ring the bell at the backdoor. If you prefer the main entrance, please walk around the house to the parking lot. From there you will find a path to the main entrance.

Taxis are available at the station only if preordered by phone (e.g., Tel. +49 7083 75 66 or +49 7083 24 82).

Dinner at Restaurant "Klosterscheuer"

On Thursday, 3rd of November, we will have dinner at Restaurant "Klosterscheuer". It is in walking distance from the convention center.
Click to enlarge
Click to enlarge