Events

15 January 2009

Verification tools at Microsoft
Rustan Leino,
Microsoft Research, Redmond

15 January 2009, 10h30
Amphi du PUIO, bât 640,
Université Paris-Sud

Program verification and other symbolic-execution and static-analysis techniques are being explored and applied to software at Microsoft. In this talk, I will first describe and give a demo of Spec#, an experimental programming system that incorporates code contracts (like pre- and postconditions and invariants) and provides run-time checking and static verification of these code contracts. I will then give an overview of some other tools developed at Microsoft Research and applied to production software.

See http://www.inria.fr/saclay/actualites/conf-rustan-leino