This award supports the Third IFIP Working Conference on "Verified Software: Theories, Tools, and Experiments (VSTTE 2010)", August 16-19, 2010, hosted by Heriot-Watt University, Edinburgh Scotland. The construction of reliable software poses one of the most significant scientific and engineering challenges of the 21st century. Professor Tony Hoare of Microsoft Research has proposed the creation of a program verifier as a grand challenge for computer science and outlined an international program of research combining many disciplines such as the theory and implementation of programming languages, formal methods, program analysis, and automated theorem proving. The VSTTE conference series was established by the research community in response to this challenge. The VSTTE 2010 program includes two workshops focusing on the areas of: (1) theories, and (2) tools and experiments. This award is enabled through support provided by the NITRD High Confidence Software and Systems (HCSS) interagency Coordinating Group.

Project Report

The Third Conference on Verified Software: Theories, Tools, and Experiments was held at Edinburgh, Scotland during August 16-19, 2010. The conference featured the main conference, a summer school, workshops, and a newly introduced Verified Software Competition. The invited speakers at the workshop included Dr. Tom Ball (Microsoft Research), Dr. Gerwin Klein (NICTA Australia), and Matthew Parkinson (U. of Cambridge). Lecturers at the summer school included Robert Atkey (University of Strathclyde) & Ewen Maclean (Heriot-Watt University), Alan Bundy & Lucas Dixon (University of Edinburgh), Cliff Jones (University of Newcastle), Gerwin Klein (National ICTA Australia), Jane Hesketh (Edinburgh), J Strother Moore (University of Texas at Austin), Natarajan Shankar (SRI) , and Graham Steel (INRIA). The Verified Software Competition featured eleven teams and 33 solutions for five challenge problems. NSF funding was used to support the invited speakers and students. The fourth Conference on Verified Software: Theories, Tools, and Experiments was held during January 2013 at Philadelphia. It was co-located with POPL 2012 and featured contributed papers, invited talks by Dr. Rupak Majumdar (MPI) and Dr. Wolfgang Paul (Saarbruecken) and invited tutorials by Dr. Rustan Leino (MSR) and Dr. Francesco Lugozzo (MSR). The conference also included the presentation of the awards for the second Verified Software Competition. The fifth Conference on Verified Software: Theories, Tools, and Experiments was held during May 2013 at Menlo College in Atherton, California. The conference featured contributed talks, invited talks by Dr. Nikhil Swamy (MSR), Dr. Alex Aiken (Stanford), and Dr. Andre Platzer (CMU), and an invited tutorial by Dr. Sandrine Blazy (Rennes). Future meetings of VSTTE will be co-located with CAV, and the next one will be at Vienna in 2014.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Network Systems (CNS)
Type
Standard Grant (Standard)
Application #
1033105
Program Officer
David Corman
Project Start
Project End
Budget Start
2010-09-01
Budget End
2013-08-31
Support Year
Fiscal Year
2010
Total Cost
$49,900
Indirect Cost
Name
Sri International
Department
Type
DUNS #
City
Menlo Park
State
CA
Country
United States
Zip Code
94025