No.016 The Java Modeling Language (JML)

Icon

NII Shonan Meeting Seminar 016

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

Category: Schedule

Tagged:

Comments are closed.