Today's increasingly computer-based society is dependent on the correctness and reliability of crucial infrastructure, such as programming languages, compilers, networks, and microprocessors. One way to achieve the required level of assurance is to use formal specification and proof, and tool support for this approach has steadily grown to the point where the specification and verification of important system infrastructure is now feasible.

To survey the state of the art and discuss future possibilities and challenges, we are pleased to announce a two day research meeting, to be held in honour of Prof. Michael J. C. Gordon FRS on the occasion of his 60th birthday.

Group Photo

Invited Speakers

The following speakers will present their research at the meeting:
  • Michael Gordon, Cambridge University
      Synthesizing Implementations Using a Theorem Prover
  • John Harrison, Intel
      Formalizing an Analytic Proof of the Prime Number Theorem
  • Sava Krstić, Intel
      Decision Procedures for Parametric Theories
  • Xavier Leroy, INRIA
      Micro-architecture Verification, Compiler Verification: What Next?
  • Tom Melham, Oxford University
      A Framework for Algorithm Level Hardware Modelling
  • Robin Milner, Cambridge University
      Memories and Reflections for Mike Gordon
  • J Moore, University of Texas at Austin
      Proof Search Debugging Tools in ACL2
  • Tobias Nipkow, Technical University of Munich
      A Bit of Social Choice Theory in HOL: Arrow and Gibbard-Satterthwaite
  • Michael Norrish, NICTA
      Defining a C++ Semantics
  • Larry Paulson, Cambridge University
      Automation for Interactive Proof: Techniques, Lessons and Prospects
  • Peter Sewell, Cambridge University
      Network Protocols: The Terror and the Glory
  • Laurent Théry, INRIA
      Proving and Computing: Certifying Large Prime Numbers
There will also be poster presentation sessions, in which attendees may present their research. Please refer to the technical program for submission information.

Important Dates

15 February 2008 Poster abstract deadline
22 February 2008 Notification of poster abstract acceptance/rejection
27 February 2008 Early registration deadline
29 February 2008 Final version of abstracts due
14 March 2008 Registration deadline
25–26 March 2008 TTVSI research meeting

Related Events

ETAPS 2008 is March 29 - April 6 in Budapest, Hungary with DCC (Designing Correct Circuits) 2008 as a satellite event on 29-30 March.

Organizers

  • Richard Boulton, Icera Inc.
  • Joe Hurd, Galois Inc.
  • Konrad Slind, University of Utah
For all enquiries about the meeting, please use the email address contact email address

Sponsors

TTVSI is sponsored by the University of Cambridge Computer Laboratory, Galois, Inc., and Lemma 1 Ltd.

University of Cambridge Computer Laboratory Galois, Inc.