Description
Francesco Logozzo, a researcher at the Research in Software Engineering (RiSE) group at Microsoft Research, gives a demo of the Static Checker that comes with Code Contracts for .NET tools. The static checker allows you to verify that all the assertions in your code hold without actually running the code!
Francesco also goes to the whiteboard and gives us a short tutorial on Abstract Interpretation, the technique used by the static checker to prove the assertions.
 Try the Code Contracts in your web browser at http://pex4fun.com/absverified!
 Code Contracts Forums
 Code Contracts Home page
The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.
Download
Download this episode
 MP3 (8.8 MB)
 Low Quality MP4
 Mid Quality WMV (159.6 MB)
More episodes in this series
Nikolaj Bjørner and Leonardo de Moura: The Z3 Constraint Solver
Related episodes
Daryl Zuniga and Mike Barnett  Xml Documentation from Code Contracts for .Net
The Verification Corner  Stepwise Refinement
The Verification Corner  Loop Termination
Nikolaj Bjørner and Leonardo de Moura: The Z3 Constraint Solver
MSDN Flash Podcast 013 – Code Contracts at TechEd Europe
Daryl Zuniga  Viewing Code Contracts.NET in Visual Studio
Mike Barnett  Getting started with Code Contracts in Visual Studio 2008
ICSE 2011: Danny Dig  Retrofitting Parallelism into a Sequential World
ICSE 2011: Conversation with Andreas Zeller
Orleans: A Framework for Scalable Client+Cloud Computing
The Discussion

Abstract interpretation and static checking is a real cool thing. Thanks for sharing this and keep pushing in further developments on this!
Cheers, Matthias

Great video and "promo" I've just started using CC.
Thank you very much.

Some remark, or maybe qestion about simple example on whiteboard... since we always entering that loop with x increment we should get postcondition of x > 0 strictly... why do all reasoning with intervals leads to x in [0, +inf] interval?

Hi Andrew,
that's a very good point.
(As far as x is concerned) the loop invariant is x >= 0, as before entering the loop x == 0, and then it is always incremented by one.
At the loop exit, we know that x >=0, but also that x > N (by the negation of the loop guard) and N > 0 (by the method precondition).
As a consequence we can refine the interval for x to [2, +oo].
I haven't mentioned it in the video to keep it simple, but you are right that the tool can prove a stronger assertion after the loop. In fact, if you download the checker, you can see that it proves the assertions x > 0 and x > 1 (but not x > 2 .
Thanks!
f