Technical Program
DAY1 - monday 22 august 2011
08:30 - 09:00 Welcome
09:00 - 10:00 Invited talk - mike kishinevsky
10:00 - 10:30 break
Challenges in verifying communication fabrics
10:30 - 12:00 session 1 - Formal verification
seL4 Enforces Integrity
Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein.
A verified runtime for a verified theorem prover
Magnus O. Myreen and Jared Davis.
Towards Robustness Analysis using PVS
Renaud Clavel, Laurence Pierre and Regis Leveugle.
12:00 - 13:30 lunch
13:30 - 14:00 session 2 -rough diamonds
Composable Discovery Engines for Interactive Theorem Proving
Phil Scott and Jacques Fleuriot.
Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers
Matej Urbas and Mateja Jamnik.
14:00 - 15:30 session 3 - proof tools
Termination of Isabelle Functions via Termination of Rewriting
Alexander Krauss, Christian Sternagel, René Thiemann, Carsten Fuhs and Jürgen Giesl.
Automatic Differentiation in ACL2
Peter Reid and Ruben Gamboa.
Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
Tobias Nipkow.
15:30 - 16:00 break
16:00 - 17:30 system demo - acl2
Warren Hunt
DAY2 - tuesday 23 august 2011
09:00 - 10:00 Invited talk - don batory
10:00 - 10:30 break
Towards verification of product lines
10:30 - 12:00 session 4 - Formal verification
Animating the Formalised Semantics of a Java-like Language
Andreas Lochbihler and Lukas Bulwahn.
Verifying object-oriented programs with higher-order separation logic in Coq
Jesper Bengtson, Jonas Braband Jensen, Filip Sieczkowski and Lars Birkedal.
Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments
Peter Gammie.
12:00 - 13:30 lunch
13:30 - 14:00 session 5 -rough diamonds
Lightweight Tools for Heavyweight Semantics
Scott Owens, Peter Boehm, Francesco Zappa Nardelli and Peter Sewell.
LCF-style Bit-Blasting in HOL4
Anthony Fox.
14:00 - 15:00 session 6 -formalizing mathematics
Three Chapters of Measure Theory in Isabelle/HOL
Johannes Hölzl and Armin Heller.
Formalization of Entropy Measures
Tarek Mhamdi, Osman Hasan and Sofiene Tahar.
15:00 - 15:30 break
15:30 - 17:00 system demo - Key
Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Peter H. Schmitt
17:00 - 18:00 business meeting
DAY3 - wednesday 24 august 2011
09:00 - 10:00 Invited talk - bart jacobs
10:00 - 10:30 break
Logical formalisation and analysis of the Mifare Classic card in PVS
10:30 - 12:00 session 7 - Formalizing mathematics
A Formalization of Polytime Functions
Sylvain Heraud and David Nowak.
Mechanised Computability
Michael Norrish.
Point-free, set-free concrete linear algebra
Georges Gonthier.
12:00 - 13:00 lunch
13:00 - 18:30 social event - kröller Müller museum in arnhem
18:30 - 22:00 conference dinner - het rijk van nijmegen
DAY4 - thursday 25 august 2011
09:00 - 10:00 Invited talk - georges gonthier
10:00 - 10:30 break
Advances in the formalization of the Odd Order Theorem
10:30 - 12:00 session 8 - Formalizing mathematics
A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions (Proof Pearl)
Chunhan Wu, Xingyuan Zhang and Christian Urban.
On the Generation of Positivstellensatz Witnesses in Degenerate Cases
David Monniaux and Pierre Corbineau.
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial Polynomials
Laureano Lambán, Francisco-Jesús Martín-Mateos, Julio Rubio and Jose-Luis Ruiz-Reina.
12:00 - 13:30 lunch
13:30 - 14:30 session 9 - applications
Relational decomposition
Lennart Beringer.
Structural Analysis of Narratives with the Coq Proof Assistant
Anne-Gwenn Bosser, Pierre Courtieu, Julien Forest and Marc Cavazza.
14:30 - 15:00 break
15:00 - 16:00 session 10 - Quantified boolean formulas
Proving Valid Quantified Boolean Formulas in HOL Light
Ondřej Kunčar.
Validating QBF Validity in HOL4
Ramana Kumar and Tjark Weber.
16:00 - 16:15 closing
(Chair: Julien Schmaltz)
(Chair: Tobias Nipkow)
(Chair: Magnus Myreen)
(Chair: Michael Norrish)
(Chair: Julien Schmaltz)
(Chair: Reiner Hänle)
(Chair: Julien Schmaltz)
(Chair: Sandrine Blazy)
(Chair: Assia Mahboubi)
(Chair: Marko van Eekelen)
(Chair: Herman Geuvers)
(Chair: José Luis Ruiz Reina)
(Chair: Freek Wiedijk)
(Chair: Yves Bertôt)
(Chair: Stefan Berghofer)
(Chair: Christine Paulin)
SLIDES
SLIDES
SLIDES
SLIDES
SLIDES
SLIDES
SLIDES
SLIDES
