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.  For more details follow this link.


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. More details about current set of challenges can be found here.


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.


2013 Microsoft Research Verified Software Milestone Award


The Microsoft Research Verified Software Milestone Award is made to Roope Kaivola (Intel Corporation, Oregon, USA) with regards to the Intel Core i7 verification project.  While formal methods were applied within a number of areas of the Core i7 project, the award is being given in recognition for Kaivola's role as intellectual leader of the core execution cluster as well as his leadership of the verification team.


The formal presentation of the Award will be made to Roope at POPL 2014, which takes place in San Diego - January 22-24.


"Microsoft Research is delighted to celebrate the advances made in verified software with the Intel Core i7 Project. It is a real milestone when formal

verification is used as the primary validation and coverage driven testing was entirely dropped. We salute Roope Kaivola and his team for some twenty 

person years of verification work, one of the most ambitious formal verification efforts in the hardware industry to date."


 Dr. Judith Bishop, Principal Research Director, Computer Science, 

Microsoft Research, Redmond

The full citation can be accessed here


2012 Microsoft Research Verified Software Milestone Award


We are delighted to announce that the recipient of the 2012 Microsoft Research Verified Software Milestone Award is Xavier Leroy of the Paris-Rocquencourt research center of INRIA, France, for the CompCert Project. Specifically, the award is given in recognition for Xavier's role as architect of the CompCert C Verified Compiler as well as his leadership of the development team.


The formal presentation of the Award will be made to Xavier at POPL 2013, which takes place in Rome - January 23-25, 2013.


"Microsoft Research is delighted to celebrate the advances made by Dr Leroy in the vital field of software verification. Compilers are the basis for all the

 software we generate, and by ruling out compiler-introduced bugs, the CompCert project has taken a huge leap in producing strengthening guarantees for

 reliable critical embedded software across platforms. We congratulate Dr Leroy on his significant achievement in winning this Award."


 Dr. Judith Bishop, Principal Research Director, Computer Science, 

Microsoft Research, Redmond

The full citation 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.



Please contact Gudmund Grov if you have any questions related to this site.