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.
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
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
Sponsors
TTVSI is sponsored by the University of Cambridge Computer Laboratory, Galois, Inc., and Lemma 1 Ltd.