May 1, 2013
Schedule
12th May (Sun)
- 3:00 pm: Hotel check-in (early check-in from 12:00 is negotiable if informed in advance)
- 7:00 pm: Welcome reception (restaurant Katsura at 2F)
13th May (Mon)
- 9:00 am ? 9:45 am: Welcome and introduction
- 9:45 am ? 10:30 am: Session on the current status of JML (Gary T. Leavens)
- 10:30 am ? 11:00 am: Break
- 11:00 am ? 11:45 am: JMLUnitNG: Present and Future (Daniel Zimmerman)
- 12:00 pm ? 2:00 pm: Lunch break
- 2:00 pm ? 2:45 pm: The EventB2Java Tool for Generating JML-Specified Java Implementations of Event-B Models (Néstor Cataño)
- 2:45 pm ? 3:30 pm: Verification of JML Expressions Using UML/OCL-based Approaches (Robert Wille)
- 3:30 pm ? 4:00 pm: Break
- 4:00 pm ? 4:45 pm: Demo of the KeY system (Peter H. Schmitt)
- 4:45 pm – 6:00 pm: OpenJML: Status and Challenges (David Cok)
14th May (Tue)
- 9:00 am – 9:45 am: Ghost Code and Algorithmic Specification in the Java Modeling Language (Bernhard Beckert)
- 9:45 am – 10:30 am: Generics: an annotation preserving type erasure (Stefan Blom)
- 10:30 am – 11:00 am: Break
- 11:00 am – 11:45 am: Reuse in JML by Specification Deltas (Reiner Hähnle)
- 12:00 pm ? 2:00 pm: Lunch break
- 2:00 pm ? 2:45 pm: For programs and proofs: mo’ specs and mo’ math (K. Rustan M. Leino)
- 2:45 pm ? 3:30 pm: JML Syntax and Assertion Semantics Revisited — Spark 2014 experiences (Patrice Chalin)
- 3:30 pm ? 4:00 pm: Break
- 4:00 pm ? 4:45 pm: Explicating Symbolic Execution (xSymExe): An Evidence-Based Verification Framework (Robby)
- 4:45 pm – 5:30 pm: A Case Study in Formal Verification using Multiple Explicit Heaps (Wojciech Mostowski)
- 5:30 pm – 6:00 pm: JML & Specifications involving abstract domains (Richard Bubel)
15th May (Wed)
- 9:00 am – 9:45 am: Exploring info flow extensions in a project that targets Android apps (David Naumann)
- 9:45 am – 10:30 am: Proving Information Flow Security with JML and KeY (Daniel Bruns)
- 10:30 am – 11:00 am: Break
- 11:00 am – 11:45 am: Session on JML in academic education (Marieke Huisman)
- 11:45 am – 12:00 am: Photo shooting
- 12:00 pm ? 1:30 pm: Lunch break
- 1:30 pm – 6:00 pm: Excursion (Kamakura)
- 6:00 pm: Banquet (Kamakura)
16th May (Thu)
- 7:00 am – 9:00 am: Room check-out (Check-out should be done before 10 am.)
- 9:00 am – 9:45 am: JSR 308, the Checker Framework, and JML (Werner Dietl)
- 9:45 am – 10:15 am: On the Specification of the Past (Jooyong Yi)
- 10:15 am – 10:45 am: Break
- 10:45 am – 11:15 am: Incorporating Region Logic and Separation Logic into JML Framing (Gary T. Leavens)
- 11:15 am – 11:45 am: Session on the Future of JML, continued
- 12:00 pm ? 1:30 pm: Lunch
- 1:30 pm: Dismiss