| 09:00 | Norbert Schirmer
and Ernie Cohen From Total Store Order to Sequential Consistency: A Practical Reduction Theorem |
| 09:30 | Freek Verbeek
and Julien Schmaltz Proof Pearl: A formal proof of Duato's condition for deadlock-free adaptive networks |
| 10:30 | Ramana Kumar and Michael Norrish (Nominal) Unification by Recursive Descent with Triangular Substitutions |
| 11:00 | Jean-François Dufourd
and Yves Bertot Formal study of plane Delaunay triangulation |
| 11:30 | Sylvie Boldo
, François Clément
, Jean-Christophe Filliatre
, Micaela Mayero
, Guillaume Melquiond
and Pierre Weis Formal Proof of a Wave Equation Resolution Scheme: the Method Error |
| 12:00 | Anthony Fox and Magnus Myreen A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture |
| 14:00 | David Harel (Weizmann Institute of Science) Amir Pnueli: A Gentle Giant, Lord of the Phi's and the Psi's. |
| 14:30 | Gordon Plotkin (University of Edinburgh) Robin Milner, a Craftsman of Tools for the Mind. |
| 15:30 | Brian Huffman
and Christian Urban Proof Pearl: A New Foundation for Nominal Isabelle |
| 16:00 | John Cowles
and Ruben Gamboa Using a First Order Logic to Verify That Some Set of Reals Has No Lebesgue Measure |
| 16:30 | Tarek Mhamdi, Osman Hasan
and Sofiene Tahar On the Formalization of the Lebesgue Integration Theory in HOL |
| 09:00 | Gerwin Klein (NICTA) A Formally Verified OS Kernel. Now What? |
| 10:30 | Joe Hendrix
, Deepak Kapur
and Jose Meseguer Coverset Induction with Partiality and Subsorts: a Powerlist Case Study |
| 11:00 | Michael Armand, Benjamin Gregoire, Arnaud Spiwack
and Laurent Thery Introducting machine integers and arrays to type theory and its application to SAT verification |
| 11:30 | Moa Johansson, Lucas Dixon
and Alan Bundy Case-Analysis for Rippling and Inductive Proof |
| 12:00 | Panagiotis Manolios
and Daron Vroon Interactive Termination Proofs using Termination Cores |
| 14:00 | Gilles Barthe, Benjamin Grégoire and Santiago Zanella Béguelin Programming language techniques for cryptographic proofs |
| 14:30 | David Cachera
and David Pichardie Proof Pearl: A Certified Denotational Abstract Interpreter |
| 15:30 | Sol Swords and Warren Hunt A Mechanically Verified AIG-to-BDD Conversion Algorithm |
| 16:00 | William Mansky and Elsa Gunter A Framework for Formal Verification of Compiler Optimizations |
| 16:30 | Herman Geuvers
, Adam Koprowski
, Dan Synek
and Eelis van der Weegen Automated Machine-Checked Hybrid System Safety Proofs |
| 09:00 | Georg Gottlob (University of Oxford) Datalog+-: A Family of Logical Query Languages for New Applications. |
| 10:30 | Amy Felty
and Brigitte Pientka Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison |
| 11:00 | Serge Autexier
and Dominik Dietrich A tactic language for declarative proofs |
| 11:30 | Daria Walukiewicz-Chrząszcz
and Jacek Chrząszcz Inductive Consequences in the Calculus of Constructions |
| 12:00 | Magnus O. Myreen Separation logic adapted for proofs by rewriting |
| 12:10 | Douglas Howe Higher-Order Abstract Syntax in Isabelle/HOL |
| 12:20 | Bas Spitters
and Eelis van der Weegen Developing the algebraic hierarchy with type classes in Coq |
| 14:00 | J Strother Moore (University of Texas) Theorem Proving for Verification: The Early Days. |
| 09:00 | Benjamin C. Pierce (University of Pennsylvania) Proof Assistants as Teaching Assistants: A View from the Trenches |
| 10:30 | Matthieu Sozeau Equations: a dependent pattern-matching compiler |
| 11:00 | Arthur Charguéraud The Optimal Fixed Point Combinator |
| 11:30 | Thomas Braibant
and Damien Pous An Efficient Coq Tactic for Deciding Kleene Algebras |
| 12:00 | Peter Lammich and Andreas Lochbihler The Isabelle Collections Framework |
| 14:00 | Jasmin Christian Blanchette and Tobias Nipkow Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder |
| 14:30 | Alexander Krauss
and Andreas Schropp A Mechanized Translation from Higher-Order Logic to Set Theory |
| 15:30 | Chantal Keller
and Benjamin Werner Importing HOL-Light into Coq |
| 16:00 | Sascha Böhme
and Tjark Weber Fast LCF-Style Proof Reconstruction for Z3 |
| 16:30 | Tjark Weber Validating QBF Invalidity in HOL4 |