Une conférence de Rustan Leino du groupe « Research in Software Engineering » de MSR Redmond aura lieu le 15 janvier à 10 :30 à l’Université d’Orsay.
C’est bien sur public, ouvert à tous!
Détails à : http://www.inria.fr/saclay/actualites/conf-rustan-leino
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.