Meeting Program

Tuesday 25 March 2008
09:00–09:45 Registration, coffee available
09:45–10:00 Introduction in the Kohn Centre
10:00–10:45 Robin Milner, Cambridge University
  Memories and Reflections for Mike Gordon
10:45–11:15 Coffee break
11:15–12:00 Michael Gordon, Cambridge University
  Synthesizing Implementations Using a Theorem Prover
12:00–13:15 Lunch
13:15–14:00 J Moore, University of Texas at Austin
  Proof Search Debugging Tools in ACL2
14:00–14:45 Tobias Nipkow, Technical University of Munich
  A Bit of Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite
14:45–15:00 Poster talks: 2 minutes each
  • Sandrine Blazy
  • Paul Curzon, Rimvydas Ruksenas, Jonathan Back and Ann Blandford
  • David Greaves
  • Magnus O. Myreen
  • Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar and Rok Strniša
  • Kong Woei Susanto, Wayne Luk, Jose Gabriel Coutinho and Tim Todman
  • Christian Urban
15:00–15:30 Tea break, during which the poster authors will be on hand
15:30–16:15 Sava Krstić, Intel
  Decision Procedures for Parametric Theories
16:15–17:00 Tom Melham, Oxford University
  A Framework for Algorithm Level Hardware Modelling
17:00–18:00 Pre-dinner drinks in the Marble Hall
18:00–21:00 Banquet in the Dining Room


Wednesday 26 March 2008
08:30–09:15 Coffee available
09:15–10:00 Xavier Leroy, INRIA
  Micro-architecture Verification, Compiler Verification: What Next?
10:00–10:45 John Harrison, Intel
  Formalizing an Analytic Proof of the Prime Number Theorem
10:45–11:15 Coffee break
11:15–12:00 Peter Sewell, Cambridge University
  Network Protocols: The Terror and the Glory
12:00–13:30 Lunch
13:30–14:15 Laurent Théry, INRIA
  Proving and Computing: Certifying Large Prime Numbers
14:15–15:00 Michael Norrish, NICTA
  Defining a C++ Semantics
15:00–15:15 Poster talks: 2 minutes each
  • Nathan Chong and Samin Ishtiaq
  • Anthony Fox
  • Paul B. Jackson and Grant Olney Passmore
  • Scott Owens
  • Julien Schmaltz
  • Balraj Singh, Alexander J. T. Gurney and Timothy G. Griffin
  • Thomas Tuerk
15:15–15:45 Tea break, during which the poster authors will be on hand
15:45–16:30 Larry Paulson, Cambridge University
  Automation for Interactive Proof: Techniques, Lessons and Prospects
16:30–16:45 Close

Poster Presentations

Attendees of TTVSI are invited to submit abstracts for posters, describing research related to the theme of the conference. The abstracts will be reviewed and accepted abstracts will appear in the proceedings of TTVSI.

Poster submissions should be 1 page in length, using LaTeX2e and the LNCS style file. The submission should be an extended abstract summarizing the poster contents. The deadline for submitting poster abstracts is 15 February 2008; instructions on poster preparation will be sent to authors of accepted abstracts by 22 February 2008.

Please email poster abstract submissions to submission email address

Poster authors are responsible for printing their poster and bringing it to the Royal Society. The poster boards are 2 metres high and 0.6 metres wide. Posters should be put up as early as possible on the scheduled day of the poster talk (see the Meeting Program below). Poster authors will have a 2 minute talk slot to advertize their poster, followed by a tea break where they are expected to be next to their poster to answer questions about it.