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

Accepted Papers

• Andreas Lochbihler. Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL
• Alwen Tiu and Jeremy E. Dawson. Formalising Observer Theory for Environment-Sensitive Bisimulation
• Stefan Berghofer and Markus Reiter. Formalizing the Logic-Automaton Connection
• Stefan Berghofer, Lukas Bulwahn and Florian Haftmann. Turning inductive into equational specifications
• Chad Brown and Gert Smolka. Extended First-Order Logic
• Magnus O. Myreen and Mike Gordon. Verified LISP implementations on ARM, x86 and PowerPC
• Brian Huffman. A Purely Definitional Universal Domain
• Peter Homeier. The HOL-Omega Logic
• Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish. Mind the Gap: A Verification Framework for Low-Level C
• Alexander Schimpf, Stephan Merz and Jan-Georg Smaus. Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• René Thiemann and Christian Sternagel. Certification of Termination Proofs using CeTA
• Stephane Le Roux. Acyclic preferences and existence of sequential Nash equilibria: a formal and constructive equivalence
• Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico Tassi. Hints in unification
• Javier de Dios and Ricardo Pena. Formal Certification of a Resource-Aware Language Implementation
• Dabrowski Frédéric and David Pichardie. A Certified Data Race Analysis for a Java-like Language
• Wouter Swierstra. Proof pearl: The Hoare State Monad
• François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. Packaging Mathematical Structures
• Nick Benton, Andrew Kennedy and Carsten Varming. Some Domain Theory and Denotational Semantics in Coq
• Thomas Tuerk. A Formalisation of Smallfoot in HOL
• Rafal Kolanski and Gerwin Klein. Types, Maps and Separation Logic
• Jesper Bengtson and Joachim Parrow. Psi-calculi in Isabelle
• Ioana Pasca and Nicolas Julien. Formal verification of exact computations using Newton's method
• Scott Owens, Susmit Sarkar and Peter Sewell. A better x86 memory model: x86-TSO
• Andrew McCreight. Practical Tactics for Separation Logic
• Osman Hasan, Sanaz Khan Afshar and Sofiene Tahar. Formal Analysis of Optical Waveguides in HOL
• Jinshuang Wang and Xingyuan Zhang. Liveness Reasoning with Isabelle/HOL
• Keiko Nakata and Tarmo Uustalu. Trace-based coinductive operational semantics for While: Big-step and small step, functional and relational styles

Accepted Papers in the Emerging Trends Section

• Anduo Wang, Boon Thau Loo, Changbin Liu, Oleg Sokolsky and Prithwish Basu. A Theorem Proving Approach Towards Declarative Networking
• Bruno Bernardo. Towards an Implicit Calculus of Inductive Constructions. Extending the Implicit Calculus of Constructions with Union and Subset Types
• Holger Gast. Towards a Modular Extensible Isabelle Interface
• Florian Kammüller and Henry Sudhof. A Mechanized Theory of Aspects
• F.J. Lopez-Fraguas, Stephan Merz and Juan Rodriguez-Hortala. A Formalization of the Semantics of Functional-Logic Programming in Isabelle
• Filip Maric and Predrag Janicic. SAT Solver Verification Project
• Anduo Wang and Boon Thau Loo. Formalizing Metarouting in PVS
• Richard Warburton and Sara Kalvala. Verifying Compiling Optimisations Using Isabelle/HOL