University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Steps toward usable verification

Steps toward usable verification

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

First, I will provide some background information on CodeContracts, the language-agnostic specification language of .NET 4.x, and on Clousot, the companion abstract interpretation-based verifier. I will explain why we chose abstract interpretation instead of, e.g., using a theorem prover and discuss our experience with its adoption both inside and outside the company. Then, I will cover topics that make the verification usable by the working programmers: inference of necessary preconditions, verified code repairs, refactoring with contracts, and verification modulo versions. En passant, I will present a generalization of Hoare Logic, Algebraic Hoare Logic, and show how the usual conjunction and disjunction rules require extra hypotheses to ensure soundness.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity