No.016 The Java Modeling Language (JML)

• Information from Shonan Village Center: http://www.shonan-village.co.jp/svc/access.html
• Google map (click for an enlarged view)
  
• You can check train schedules from the following website:?http://www.hyperdia.com/en/.?Type “ZUSHI” as your destination. If you happen to come via Haneada airport, type “SHINZUSHI” instead (“Shin” means “new” in Japanese).
• You need to take a bus (No. 16) or a taxi at?Zushi (or?Shinzushi) to get to Shonan village center. Buses depart from Zushi?once or twice an hour (see the timetable). Get off the bus at the last stop. You can see?the?list of bus stops here. (Use Google translator.)
  
• A taxi will cost you approx??2,500 ? 3,000 yen. Here are Japanese messages you can show to a taxi driver (taken from a previous Shonan meeting).
• Wonder if I need a visa? Check this out: http://www.mofa.go.jp/j_info/visit/visa/short/novisa.html
• If you want to stay one more night (check out at on 17th), you can do so by filling in an accommodation reservation form. You will get this form by an email from Shonan Village Center at the end of March. Additional costs are as follows:

1. Accomodation fee (breakfast included) 10,500 yen/night
2. [Option] Lunch: 1,200 yen, Dinner: 2,800 yen

• Gary T. Leavens, University of Central Florida, Orlando, FL, USA,?Incorporating Region Logic and Separation Logic into JML Framing
• Peter H. Schmitt, Karlsruhe Institute of Technology, Karlsruhe, Germany, Demo of the KeY system (static verification of JML spec via KeY)
• Jooyong Yi, National University of Singapore, Singapore, On the Specification of the Past (JML extensions to deal with two kinds of the past, i.e., the pre-state and the previous-version state)

• Bernhard Beckert, Karlsruhe Institute of Technology, Germany, Ghost Code and Algorithmic Specification in the Java Modeling Language
• Stefan Blom, University of Twente, The Netherlands,?Generics: an annotation preserving type erasure
• Daniel Bruns, Karlsruhe Institute of Technology, Germany, Proving Information Flow Security with JML and KeY
• Richard Bubel, TU Darmstadt, Germany,?JML & Specifications involving abstract domains (Preliminary Ideas and Experiences)
• Néstor Cataño, The University of Madeira, Portugal, The EventB2Java Tool for Generating JML-Specified Java Implementations of Event-B Models
• Patrice Chalin, Kansas State University, US, JML Syntax and Assertion Semantics Revisited (Spark 2014 experiences)
• David Cok, GrammaTech, Ithaca, NY, US, OpenJML: Status and Challenges
• Werner Dietl, University of Washington, US, JSR 308, the Checker Framework, and JML
• Reiner Hähnle, Technische Universität Darmstadt, Germany, Reuse in JML by Specification Deltas
• Marieke Huisman, University of Twente, The Netherlands, Chair of “JML in academic education”
• K. Rustan M. Leino, Microsoft Research, Redmond, US,?For programs and proofs: ?mo’ specs and mo’ math
• Wojciech Mostowski, University of Twente, Netherland, A Case Study in Formal Verification using Multiple Explicit Heaps
• David Naumann, Stevens Institute of Technology, US, Exploring info flow extensions in a project that targets Android apps
• Erik Poll, Radboud University Nijmegen, The Netherlands,?Extracting models from code??(canceled for personal reasons)
• Robby, Kansas State University, US, Explicating Symbolic Execution (xSymExe): An Evidence-Based?Verification Framework
• Robert Wille, University of Bremen, Germany, Verification of JML Expressions Using UML/OCL-based Approaches
• Daniel Zimmerman, University of Washington Tacoma, US, JMLUnitNG: Present and Future

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

The seminar will pull together and energize the broad community of JML researchers and developers. We plan to have seminar participants work together on JMLs documentation, examples, pedagogical materials, and implementation infrastructure. The meeting will also provide a forum for considering changes to the language, for organizing community efforts, and for discussing recent work on formal methods relating to JML and its semantics. In addition to talks we plan working sessions and interactive discussions. We intend to involve the participants in writing documentation, examples, teaching materials, and library specifications. They will also discuss and debug software infrastructure and recent changes in the semantics for JML. In addition, they will discuss and help organize the JML community.