The meeting is taking place at Kellogg College, in the Mawby Room.
Accommodation and Travel
Kellogg College is within walking distance from the main venues of FLoC (Kellogg College on Google Maps).Please refer to FLoC 2018 website regarding
Note: if you plan to come by car, please note that there no parking on college grounds, so you would need to make arrangements in nearby streets or park in a park and ride.Schedule
Friday 13
08:00-09:00 | welcome coffee |
09:00-10:00 | Yannick: boundaries of automatic program verification (30 minutes) slides |
Radu: selective monitoring (30 min) | |
10:00-10:30 | coffee break |
10:30-12:30 | Gerhard: FastLane is Opaque -- A Case Study in Mechanized Proofs of Opacity (30 min) slides |
Alex: the Axiom Profiler (45 minutes) | |
discussion: verification challenges/competitions/use cases (45 minutes) | |
12:30-14:00 | lunch break |
14:00-16:00 | Tony Hoare: Teaching CS fresh a unified Theory of Programming, based on algebra, logic and geometry (45 minutes) |
Sandrine: teaching with Why3 (30 minutes) slides | |
discussion: teaching program verification (45 minutes) | |
16:00-16:30 | coffee break |
16:30-17:30 | We end the meeting at 4pm so that you can attend Talks in memoriam Mike Gordon at CAV if you wish |
Saturday 14
08:00-09:00 | welcome coffee |
09:00-10:00 | Jan: Resource Analysis for Probabilistic Programs (45 minutes) |
Ernie: probability = nondeterminism + martingales (15 min) | |
10:00-10:30 | coffee break |
10:30-12:30 | Thomas: Compositional Abstractions for Concurrent Data Structures (45 or 30 min) |
Shaz: Compositional testing for dynamic distributed systems (30 min) | |
discussion: What should we be doing about security (e.g. timing side channels)? | |
12:30-14:00 | lunch break |
14:00-16:00 | Shankar: 2020 Newton Institute on Verified Software (30 min) |
Klaus: BDDs on the Run (30 min) slides.pptx | |
Bart: modular verification of programs that perform I/O (30 minutes) | |
discussion: SMT solver ecosystem preservation | |
16:00-16:30 | coffee break |
16:30-17:30 | member-only meeting |
Participants
- Sandrine Blazy
- Ernie Cohen
- Jean-Christophe Filliātre (chair)
- Radu Grigore (invited)
- Jan Hoffmann (invited)
- Klaus Havelund
- Tony Hoare
- Bart Jacobs
- Cliff Jones
- Yannick Moy (invited)
- Peter Müller
- Shaz Qadeer
- Ilya Sergej (invited)
- Natarajan Shankar (secretary)
- Gerhard Schellhorn
- Alex Summers
- Thomas Wies (invited)
- Jim Woodcock (vice-chair)