Marienplatz (city centre)

Englischer Garten
The English Garden

Chinesischer Turm
Chinese Tower (famous beer garden)

Computer science building
The Computer Science building of the TUM

Main hall of the computer science building
The main hall in the CS-building

The river Isar
The Isar river

The conference poster

Preliminary Programme

Pre-Conference Workshop (August 13-15)

Isabelle Developers Workshop

Sunday, August 16


Monday, August 17

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

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)

Coq Workshop

Last modified: Mon Aug 10 16:43:44 CEST 2009 [Validate this page.]