meets
meets
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:
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).
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.
– Program Schedule as of October 31, 2016 –
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? |
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) |
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 – |
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
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.
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.
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).
