Program correctness is difficult and expensive to ensure. In the limit, formal program verification has been proposed as a solution, but for several reasons it has not been embraced in the software engineering community.

The last decade has seen a wave of progress in verification tools, in part due to more powerful satisfiability-modulo-theories (SMT) solvers. In this talk, I will give a sense where program verification is today, demonstrating the use of one state-of-the-art system (Dafny) and mentioning some applications in both academia and industry.

Dafny is a programming language and program verifier. The language is C#-like, but builds in specification constructs, which let a programmer record the intended behavior of the program. Dafny's SMT-based static program verifier, which is run continuously in the background as the program is being developed, enforces the consistency of a program and its specifications.

Dafny has been used to verify a number of challenging algorithms. It is also being used in teaching, and the web version of the tool recently passed 250,000 submitted program-verification attempts. Dafny was a popular choice in the VSTTE 2012 program verification competition, and two of those teams received medals. Dafny's open-source implementation, which builds on the program verification engine Boogie, has also been used as a foundation for other verification tools.

Dafny homepage: http://research.microsoft.com/dafny

Try Dafny on the web: http://www.rise4fun.com/Dafny

When: June 10 at 14:30 -16:00 pm
Where: Microsoft Development Center Copenhagen, Frydenlunds Allé 6, 2950 Vedbæk

Sign up here: https://msevents.microsoft.com/CUI/EventDetail.aspx?EventID=1032554922&C...