JML Workshop 2016 – Bad Herrenalb
meets
Specification Language Semantics and Use Cases
Bad Herrenalb, Germany
Minutes: jml-workshop-2016-minutes.pdf
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 –
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)
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).
