Marienplatz (city centre)
The English Garden
Chinese Tower (famous beer garden)
The Computer Science building of the TUM
The main hall in the CS-building
The Isar river
The conference poster
|
Preliminary Programme
Pre-Conference Workshop (August 13-15)
Isabelle Developers Workshop
Sunday, August 16
18:00-20:00 RECEPTION and REGISTRATION |
Monday, August 17
8:00-9:00 | REGISTRATION |
9:00-10:00 | INVITED TALK 1 (Session Chair: ) | |
| David Basin. Let's Get Physical: Models and Methods for
Real-World Security Protocols | |
10:00-10:30 | COFFEE |
10:30-12:10 | SESSION 1 (Session Chair: ) | |
| Assia Mahboubi, Georges Gonthier, Laurence Rideau and François Garillot.
Packaging Mathematical Structures | |
| Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico
Tassi. Hints in unification | |
| Ioana Pasca and Nicolas Julien. Formal verification of exact
computations using Newton's method | |
| Osman Hasan, Sanaz Khan Afshar and Sofiene Tahar. Formal Analysis of
Optical Waveguides in HOL | |
12:10-13:40 | LUNCH |
13:40-15:20 | SESSION 2 (Session Chair: ) | |
| Wouter Swierstra. Proof pearl: The Hoare State Monad | |
| Keiko Nakata and Tarmo Uustalu. Trace-based coinductive operational
semantics for While: Big-step and small-step, functional and relational styles | |
| Andreas Lochbihler. Formalising FinFuns - Generating Code for Functions
as Data from Isabelle/HOL | |
| Stephane Le Roux. Acyclic preferences and existence of sequential Nash
equilibria: a formal and constructive equivalence | |
15:20-15:50 | COFFEE |
15:50-17:30 | SESSION 3 (Session Chair: ) | |
| Jesper Bengtson and Joachim Parrow. Psi-calculi in Isabelle | |
| Jeremy E. Dawson and Alwen Tiu. Formalising Observer Theory for
Environment-Sensitive Bisimulation | |
| Brian Huffman. A Purely Definitional Universal Domain | |
| Nick Benton, Andrew Kennedy and Carsten Varming. Some Domain Theory and
Denotational Semantics in Coq | |
Tuesday, August 18
8:00-9:00 | INVITED TUTORIAL 1 (Session Chair: ) |
| John Harrison. HOL Light: an overview | |
9:00-10:00 | INVITED TALK 2 (Session Chair: ) | |
| Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michal Moskal,
Thomas Santen, Wolfram Schulte and Stephan Tobies. VCC: A Practical System
for Verifying Concurrent C | |
10:00-10:30 | COFFEE |
10:30-12:10 | SESSION 4 (Session Chair: ) | |
| Rene Thiemann and Christian Sternagel. Certification of Termination
Proofs using CeTA | |
| Jinshuang Wang, Xingyuan Zhang and Huabing Yang. Liveness Reasoning with
Isabelle/HOL/Isar | |
| Dabrowski Frederic and David Pichardie. A Certified Data Race Analysis
for a Java-like Language | |
| Stefan Berghofer, Lukas Bulwahn and Florian Haftmann. Turning inductive
into equational specifications | |
12:10-13:40 | LUNCH |
13:40-15:20 | POSTER SESSION | |
15:20-16:00 | COFFEE |
16:00-17:00 | BUSINESS MEETING | |
Wednesday, August 19
8:00-9:00 | INVITED TUTORIAL 2 (Session Chair: ) |
| Adam Naumowicz. A Brief Overview of Mizar | |
9:00-10:00 | INVITED TALK 3 (Session Chair: ) | |
| John Harrison. Without Loss of Generality | |
10:00-10:30 | COFFEE |
10:30-11:45 | SESSION 5 (Session Chair: ) | |
| Rafal Kolanski and Gerwin Klein. Types, Maps and Separation Logic | |
| Andrew McCreight. Practical Tactics for Separation Logic | |
| Thomas Tuerk. A Formalisation of Smallfoot in HOL | |
11:45-13:00 | LUNCH |
13:00-23:00 | EXCURSION | |
Thursday, August 20
8:00-9:00 | INVITED TUTORIAL 3 (Session Chair: ) |
| Ana Bove, Ulf Norell and Peter Dybjer. A Brief Overview of Agda
- A Functional Language with Dependent Types | |
9:00-10:00 | INVITED TUTORIAL 4 (Session Chair: ) | |
| Carsten Schürmann. The Twelf Proof Assistant | |
10:00-10:30 | COFFEE |
10:30-12:10 | SESSION 6 (Session Chair: ) | |
| Scott Owens, Susmit Sarkar and Peter Sewell. A better x86 memory model:
x86-TSO | |
| Magnus O. Myreen and Mike Gordon. Verified LISP implementations on ARM,
x86 and PowerPC | |
| Javier de Dios and Ricardo Pena. Formal Certification of a
Resource-Aware Language Implementation | |
| Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock
and Michael Norrish. Mind the Gap: A Verification Framework for Low-Level C | |
12:10-13:40 | LUNCH |
13:40-15:20 | SESSION 7 (Session Chair: ) | |
| Peter Homeier. The HOL-Omega Logic | |
| Chad Brown and Gert Smolka. Extended First-Order Logic | |
| Alexander Schimpf, Stephan Merz and Jan-Georg Smaus. Construction of
Büchi Automata for LTL Model Checking Verified in Isabelle/HOL | |
| Stefan Berghofer and Markus Reiter. Formalizing the Logic-Automaton
Connection | |
15:20-15:50 | COFFEE |
Post-Conference Workshops (Friday, August 21)
PLMMS
Coq Workshop
|