We describe the current status of the grand challenge in verified software. After giving a summary of the current state of the art in software verification, we describe some of the pilot projects now underway. These include work on operating system kernels and on a biometric-based security system. The objective is to challenge tool developers to make more advances in automatic verification.

Bio:
Prof. Jim Woodcock (jcpw) (PI) holds the Anniversary Chair of Software Engineering at the University of York; until 2001, he was Professor at the University of Oxford, where he was also Founding Director of the Software Engineering Programme and Centre of Excellence. In collaboration with IBM, Oxford University Computing Laboratory received the Queen's Award for Technological Achievement in 1992 for work carried out by his team. In 1998, he was technical consultant for the first security-critical product certified to ITSEC Level E6. In 2002, he received the Rudolph Christian Karl Diesel Prize for work on railway signalling, and has been a Marktoberdorf Lecturer. He moderates UKCRC's Grand Challenge in Dependable Systems Evolution Woo, and is part of the international Grand Challenge on Verified Software. His current research is in conducting experiments in large-scale verification of industrial software as part of the Grand Challenges. He is a curator of the UK Verified Software Repository and principal investigator of the EPSRC network supporting the work of the repository. He is the author of several textbooks, about 200 papers on software engineering, has given over thirty international keynote talks, and has chaired twenty international programme committees. He is Joint Editor-in-Chief of Springer's Formal Aspects of Computing Journal and is a member of the Executive of the UK Computing Research Committee, a Visiting Fellow at the University of Oxford, and a Visiting Professor at Shanghai Jiao Tong University, the Federal University of Pernambuco, and Trinity College Dublin, where he leads the Formal Methods and Theory Research Group.

Web:
http://www-users.cs.york.ac.uk/~jim/