The Verified Software Initiative

 

The VSI manifesto

The Verified Software Initiative (VSI) is a fifteen-year, cooperative, international project directed at the scientific challenges of large-scale software verification. This initiative also includes UKCRC's Grand Challenge 6, i.e. Dependable Systems Evolution. A related IFIP Working Group on Verified Software, i.e. IFIP WG 1.9/2.14, has been recently established. The full VSI manifesto can be accessed here.


IFIP Working Group 1.9/2.14

The inaugural meeting of IFIP Working Group 1.9/2.14 took place on June 15-16 at SRI Palo Alto. Presentations arising from the meeting can be accessed here.





The VSTTE Conference Series

The Verified Software Initiative has it’s own dedicated conference: Verified Software: Theories, Tools and Experiments (VSTTE). The goal of this conference series is to advance the state of the art in the science and technology of software verification through the interaction of theory development, tool evolution, and experimental validation.


To date there have been three VSTTE conferences:


  1. •2005: ETH Zurich (Switzerland)

  2. •2008: University of Toronto (Canada)

  3. •2010: Heriot-Watt University (Scotland)


The Challenge Experiments

The initiative is driven by a set of grand challenges, which are projects at the fringe of what current techniques and tools can solve. The current set of challenges include:


  1. •POPLMark

  2. •Tokeneer

  3. •POSIX file system

  4. •medical devices


For more details about grand challenges see:


  1. •The Verified Software Repository

  2. •VSR - QPQ Deductive Repository


Microsoft Research Verified Software Milestone Award

At the 3rd International Conference on Verified Software: Theories, Tools and Experiments (VSTTE 2010), it was announced that Microsoft Research would sponsor an award that recognises significant technological advances towards the goals of the Verified Software Initiative. Full details of the Award remit, procedure and committee can be accessed here.


2011 Microsoft Research Verified Software Milestone Award


We are delighted to announce that the recipients of the inaugural Microsoft Research Verified Software Milestone Award are Janet Barnes and Rod Chapman for the Tokeneer Project.


The formal presentation of the Award will be made to Janet and Rod at AVoCS 2011, which is being hosted by Newcastle University this September.


"Congratulations to Janet and Rod as well-deserved recipients of this award. And thanks to Altran Praxis and the US National Security Agency for their commitment to their project.  It has given a persuasive demonstration of the cost effectiveness of formal methods in application to security software, and complements similar experience at Microsoft"

(Prof. Sir Tony Hoare, Microsoft Research).


The full award citation can be accessed here.



VSI website coordinators: Gudmund Grov & Leo Freitas        Last updated:  12 October 2011