Rod Chapman - The Tokeneer ID Station - a demonstration of high-assurance software development
This presentation will describe the development of the Tokeneer ID Station software - a demonstration project undertaken by Praxis for the US NSA. The project's background, development and results will be described. In the longer term, Praxis hope to contribute the project materials to the verified software repository for further study. The presentation will close with a short list of possible challenges that other researchers might undertake.

Will Harwood - Some roadblocks to the application of verification to product software
Engineering software products for the mass market present a different set of challenges to engineering bespoke software systems for a single customer. The talk will outline some of these challenges and how they affect the introduction of formal methods and verification technologies into such industries. In the process of doing this challenge problems will be discussed that illustrate the difficulties.

Colin O’Halloran - Realising commercial benefit from dependable systems evolution Grand Challenge
This presentation will draw on the experiences of the Technology Strategy Board funded Evolutionary Validation of Complex Systems project to highlight why this Grand Challenge is commercially and economically important. The application of tools to a slice of the Apache web server indicates how some of the commercial value can be realised from the scientific benefits.

Thomas Santen - The Microsoft Hypervisor verification project
The goal of the Hypervisor Verification Project is to develop an industrially viable methodology for verifying system code, and to use this methodology to verify the functional correctness of the Microsoft Hypervisor (a 60KLOC C and assembler program that turns a single MP x64 machine into a number of virtual MP x64 machines). The talk presents some particularly challenging aspects of the project and outlines techniques that will be used to address them.

Peter Sewell - Rigorous views of real-world network protocols
I'll describe our work of the last few years on specifying and validating network protocols, especially TCP and an optically switched network MAC protocol, and speculate on their suitability as verification challenges. This is joint work with many people, most recently with Tom Ridge and Michael Norrish, with papers in FM, ICNP, POPL, and SIGCOMM.