[isabelle] TTVSI call for participation, registration, and posters


Tools and Techniques for Verification of System Infrastructure (TTVSI)


  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 Krstic, Intel
  Decision Procedures for Parametric Theories

* Xavier Leroy, INRIA
  Micro-architecture Verification, Compiler Verification: What Next?

* Tom Melham, Oxford University

* Robin Milner, Cambridge University
  Memories and Reflections: Whose Proofs Need a Machine?

* J Moore, University of Texas at Austin
  Proof Search Debugging Tools in ACL2

* Tobias Nipkow, Technical University of Munich
  Linear Quantifier Elimination

* Michael Norrish, NICTA
  Defining a C++ Semantics

* Larry Paulson, Cambridge University
  Automatic Proof for Theorems On Transcendental Functions

* Larry Paulson, Cambridge University
  Automatic Proof for Theorems On Transcendental Functions

* Peter Sewell, Cambridge University
  Network Protocols: The Terror and the Glory

* Laurent Thery, INRIA
  Proving and Computing: Certifying Large Prime Numbers

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. Posters will be presented in sessions during the

FORMAT. Poster submissions should be 1 page in length, using LNCS
article format. The submission should be an extended abstract
summarizing the poster contents. Please email the submission to
program at ttvsi.org by the poster abstract deadline. All received
poster abstracts will be acknowledged by email. Instructions on
poster preparation will be sent to authors of accepted abstracts.

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


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

Other Information.

To contact the organizers please use the email address info at ttvsi.org.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.