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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Steps toward usable verification

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Judge Business School, Trumpington Street, Room W2.01 Type the title of a new list here Cambridge Climate Coalition

Other talks

TBC Using numerical simulations for solving spectral geometry problems Title tbc Feedback and the circumgalactic medium Advances in Label-Free High-Resolution Molecular Imaging using J Series III Cluster SIMS Grand Rounds - Equine
 

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