|
Sunday, August 17
|
17:00-19:00
|
REGISTRATION
WELCOME
RECEPTION
|
|
Monday, August 18
|
8:00
– 9:00
|
REGISTRATION
|
9:00
– 10:00
|
KEYNOTE
I
(Session Chair: Sofiène Tahar)
|
10:00 – 10:30
|
COFFEE BREAK
|
10:30 – 12:00
|
RESEARCH PAPERS (Session
Chair: Tobias
Nipkow)
- Lukas
Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkok and John
Matthews. Imperative Functional
Programming with Isabelle/HOL
- Sascha
Böhme, Rustan Leino and Burkhart Wolff. HOL-Boogie --- An Interactive Prover for the Boogie
Program-Verifier
- Holger
Gast. Lightweight
Separation
|
12:00-14:00
|
LUNCH
|
14:00-16:00
|
RESEARCH PAPERS (Session
Chair: Cesar
Munoz)
- Jens
Brandt and Klaus Schneider. Formal Reasoning about Causality Analysis
- David
Cock, Gerwin Klein and Thomas Sewell. Secure Microkernels, State
Monads and Scalable Refinement
Emerging Trends
- Maria
Spichkova. Focus
on Isabelle: From Specification to Verification
- Magnus
O. Myreen. Verification of LISP Interpreters
- Serguei
A. Mokhov, Joey Paquet. Formally Specifying
Operational
Semantics and Language Constructs of Forensic Lucid in Higher-Order
Intensional Logic
- Stephane
Lescuyer, Sylvain
Conchon. A reflexive formalization of a SAT
solver in Coq
- Harald
Hiss. Checking
the Satisfiability of XML-Specifications
- Thomas
Tuerk. Separation
Logic Framework in HOL
|
16:00-17:00
|
COFFEE BREAK + POSTERS
|
|
Tuesday,
August 19
|
8:00
– 9:00
|
TUTORIAL I (Session Chair:
Yves Bertot)
|
9:00
– 10:00
|
|
10:00 – 10:30
|
COFFEE BREAK
|
10:30 – 12:00
|
RESEARCH PAPERS (Session
Chair: Bukhart
Wolff)
- Klaus
Aehlig, Florian Haftmann and Tobias Nipkow. A Compiled Implementation of
Normalization by Evaluation
- Pierre Courtieu,
Julien Forest and Xavier Urbain. Certifying
a Termination Criterion Based on Graphs, without Graphs
- Yves
Bertot, Georges Gonthier, Sidi
Ould Biha and Ioana Pasca. Canonical
Big Operators
|
12:00-14:00
|
LUNCH
|
14:00-16:00
|
RESEARCH PAPERS (Session
Chair: John
Matthews)
- Ana Bove and
Venanzio Capretta. A
Type of Partial Recursive Functions
- Daniel
Wasserrab and Andreas Lochbihler. Formalizing a Framework for Dynamic Slicing of
Program Dependence Graphs in Isabelle/HOL
Emerging Trends
- Osman
Hasan. Probabilistic
Analysis using Theorem Proving
- Patrice
Chalin, Perry James,
George Karabotsos. Using Isabelle/HOL for
Static Program Verification in JML4
- Ayesha
Yasmeen, Elsa L. Gunter. Implementing Secure
Broadcast
Ambients in Isabelle using Nominal Logic
- Amjad
Gawanmeh. Theorem
Proving based Framework for Verification of Group Key Protocols
- Brian
Huffman. Reasoning
with Powerdomains in Isabelle/HOLCF
- Alexander
Krauss. Shallow Dependency Pairs
|
16:00-17:00
|
COFFEE BREAK + POSTERS
|
|
Wednesday,
August 20
|
8:00
– 9:00
|
TUTORIAL III (Session
Chair: Matt Kaufmann)
|
9:00
– 10:00
|
TUTORIAL IV (Session
Chair: Jens Brandt)
|
10:00 – 10:30
|
COFFEE BREAK
|
10:30 – 12:00
|
RESEARCH PAPERS (Session
Chair: Sam Owre)
- Sayan
Mitra
and K. Mani Chandy. A Formalized
Theory for Verifying Stability and Convergence of Automata in PVS
- Polyvios
Pratikakis, Jeff Foster, Michael Hicks and Iulian Neamtiu. Formalizing Soundness of Contextual Effects
- Matthieu
Sozeau and Nicolas Oury. First-Class
Type Classes
|
12:00-14:00
|
LUNCH
|
14:00-16:30
|
Visit to
Point-a-Caillère Museum
|
16:30-18:00
|
Free time to visit Old
Montreal
|
18:00-23:00
|
CRUISE
+ CONFERENCE
DINNER
|
|
Thursday, August 21
|
8:00
– 9:00
|
TUTORIAL V
(Session
Chair: Peter Homeir)
|
9:00
– 10:00
|
KEYNOTE II (Session Chair:
Otmane Ait
Mohamed)
|
10:00 – 10:30
|
COFFEE BREAK
|
10:30 – 12:00
|
RESEARCH PAPERS (Session
Chair: Mike
Gordon)
- David
Lester. Real Number Calculations and Theorem
Proving: Validation and Use of an Exact Arithmetic
- Russell
O'Connor. Certified Exact Transcendental Real
Number Computation in Coq
- Stefan
Berghofer and Christian Urban. Nominal
Inversion Principles
|
12:00-14:00
|
LUNCH
|
14:00-15:00
|
RESEARCH PAPERS (Session
Chair: Konrad
Slind)
- Hasan
Amjad. LCF-style
Propositional Simplification With BDDs and SAT Solvers
- Laurent
Thery. Proof Pearl.
Revisiting
the Mini-Rubik in Coq
|
15:00-16:00
|
|
16:00-16:30
|
COFFEE BREAK + CLOSING
REMARKS
|
16:30-18:30
|
Isabelle informal meeting
|