There have been a number of important breakthroughs in Java verification in the last years, but we believe that research must be taken to the next level:
The workshop will take place on the Radboud University campus. The address of the venue is:
The ESF Exploratory Workshop is a "by invitation only" event. The registered participants are:
| 9:00-9:30 | Introduction |
| Reiner Hähnle - Welcome | |
| Kaisa Sere - Presentation of the European Science Foundation | |
| 9:30-10:30 | Session 1a: Verification Frameworks |
| Bernhard Beckert - Dynamic Logic with Non-rigid Functions | |
| Kurt Stenzel - Refinement of Abstract Specifications to Java Code | |
| 10:30-11:00 | Coffee Break |
| 11:00-12:00 | Session 1b: Verification Frameworks |
| Mariela Pavlova - Java Bytecode Verification | |
| Martin Giese - A Logic with Subtypes to talk about Java Objects | |
| 12:00-13:30 | Lunch |
| 13:30-15:00 | Session 2: Concurrency |
| Vladimir Klebanov - A Dynamic Logic for Verification of Concurrent Programs | |
| Bart Jacobs - A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs | |
| Marieke Huisman - Formalising the Java Memory Model | |
| 15:00-15:30 | Coffee Break |
| 15:30-17:00 | Discussion 1: Unsolved problems in Java Verification |
| See Discussions below |
| 9:00-10:00 | Session 3: Tools |
| Joe Kiniry - Usable Formal Tools | |
| Robby - Bogor/Kiasan - Combining Symbolic Execution, Model Checking, and Theorem Proving | |
| 10:00-10:30 | Coffee Break |
| 10:30-12:00 | Session 4: Applications |
| Jean-Louis Lanet/Pierre Girard - New Challenges in Java Verification for Tiny Devices | |
| Wojciech Mostowski - Verifying Real Java Programs - API Calls vs. Language Semantics, Official Specs vs. Implementations | |
| Peter Müller - Specification and Verification Challenges | |
| 12:00-13:30 | Lunch |
| 13:30-15:00 | Session 5: Loops |
| Reiner Hähnle - Verification of Loops by Parallelization | |
| Steffen Schlager - A Method for Loop Verification Based on Fixed Points | |
| Angela Wallenburg - Using Induction in Interactive Verification | |
| 15:00-15:30 | Coffee Break |
| 15:30-16:30 | Discussion 2: Challenges |
| See Discussions below | |
| 16:30-17:00 | Discussion 3: Follow-up Activities |
| See Discussions below |
| 9:00-10:00 | Session 6: Encapsulation |
| Arnd Poetzsch-Heffter - The Box-Model: A Modular Semantics for Modular Verification | |
| Rustan Leino - Going Beyond Simple Ownership System in Spec# | |
| 10:00-10:30 | Coffee Break |
| 10:30-12:00 | Session 7a: Specification and Verification Techniques |
| Adam Darvas - Verification Technique for Method Calls in Specifications | |
| Erik Poll/Christian Haack - Immutable Objects in Java | |
| Philipp Rümmer - Disproving in Dynamic Logic for Java | |
| 12:00-13:30 | Lunch |
| 13:30-14:30 | Session 7b: Specification and Verification Techniques |
| Ronald Middelkoop - Invariants for Non-Hierarchical Object Structures | |
| Claude Marché - Algebraic Specifications for Modeling Java Programs (Example) | |
| 14:30-15:00 | Coffee Break |
| 15:00-16:30 | Discussion 4: Past Experience and Lessons for the Future |
| See Discussions below | |
| 16:30 | Closing |
Abstract: What are the most important problems in Java program verification for which we don't yet have good solutions? What are the current means of attack? Can we identify areas where we can collaborate?
Moderator: Arnd Poetzsch-Heffter
Abstract: What are the strategic directions our field should be headed to? How can we make most impact with our limited resources? Should we try to organize ourselfves more systematically (COST action, etc.)?
Moderator: Peter Schmitt
Abstract: How to proceed with the cooperation within the group of participants to support ESF efforts?
Moderator: Reiner Hähnle
Abstract: Many of us actively took part in the development of a verification tool for OO languages. As in all research tools one has to make design and technology decisions that in the end may turn out to be suboptimal. Are there things that we can learn from each other? Which mistakes did we make in designing our verification tool? Which technologies worked and which didn't? Which lessons did we learn for the future?
Moderator: Joe Kiniry
Brief statements by:
Workshop participants will be placed in two hotels in the center of Nijmegen. There is no need for the participants to contact the hotels, places will be arranged by the organizers and information sent out to the participants. The hotels are:
The workshop dinner will take place on Tuesday, 19:00, in the restaurant De Waagh on Grote Markt, see map.
Update: The most suitable way to travel from Schiphol Airport to Nijmegen is by train with a change in Utrecht Central. Both trains (from Schipol to Utrecht, and from Utrecht to Nijmegen) run every 30 minutes during the day. The price for the ticket is around 17 Euro for single trip and 30 Euro for a return trip. Train schedules can be checked at:
Important notes: ticket machines in the Netherlands do not accept Master Card or Visa cards, nor do they accept bank notes. You can use coins, international Maestro cards, or dutch Chip-Knip cards. You can also buy the ticket at the ticket office at the train station at the airport. Since recently getting on a train in the Netherlands without a valid ticket will always cost you extra 30 Euro of penalty.
You can ride on a bus with a nation wide blue Strippenkaart, which can be bought at a train station, for example, at the book/newspaper store. Most trips within Nijmegen Center/University cost two stripes on the card. The bus driver stamps the card. You can also buy the ticket from the driver.
Apollo Hotel: This hotel is within walking distance from the train station (see the map link below)
Hotel Atlanta: Update: This hotel is also reachable by foot from the train station (approximately 800 meters walk), but it's also possible to take the bus number 6 (direction Neerbosch Oost) and get off at Plein 1944 (see map link below). The bus trip takes 3 minutes. Other possible buses that go to Plein 1944 from the train station: number 2 direction St. Maartenskliniek, number 8 direction Berg en Dal.
Apollo Hotel: Update: The best bus to go to the University from the train station would be bus number 10, unfortunately it does not go before 9:00. The buses that you can take are the following (do not confuse bus directions - the same bus can go in two different directions from the same stand):
| Bus number | Direction | Time | Travel Time | In time for the first session? |
| 4 | Wijchen | 8:34 | 6 minutes | Yes |
| 83 | Venlo | 8:42 | 7 minutes | Yes |
| 6 | Brabantse Poort | 8:39 | 6 minutes | Yes |
| 6 | Brabantse Poort | 8:54 | 6 minutes | No |
| 3 | Wijchen | 8:47 | 8 minutes | Maybe |
For the first time, be in good time before at the train station - the bus stop there is one the most confusing things I have seen in my life. You should get off at the bus stop marked on the University campus map. The bus stop name is Tandheelkunde.
Atlanta Hotel: Update: Take bus number 6 from Plein 1944 (direction Brabantse Poort) and get off at the bus stop (Tandheelkunde) marked on the campus map. The bus trip takes 9 minutes. You can also take bus number 3, direction Wijchen, but this one can make you late:
| Bus number | Direction | Time | Travel Time | In time for the first session? |
| 6 | Brabantse Poort | 8:36 | 9 minutes | Yes |
| 6 | Brabantse Poort | 8:51 | 9 minutes | No |
| 3 | Wijchen | 8:50 | 5 minutes | Maybe |
You can also walk to the train station (or take any bus that go there) and take any of the buses that go from there, just remember not to confuse bus directions (see note above).
Just take the bus (3, 4 (train station only), 6, 10 (train station only)) from the bus stop on the opposite side of the road.