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
|