Francesco's Blog on CodeContracts, Static analysis, Abstract Interpretation, etc.

Some tricks to optimize CodeContracts usage, and on static analysis in general

False myth: Abstract interpretation can only do "easy" properties as nonnull

When demoing the CodeContracts static checker, often people ask me what's underneath. I tell them...

Date: 11/13/2014

Inter-procedural inference of conditions to error in cccheck

Today we pushed out a new release of CodeContracts. Among the many improvements, bug fixes, etc. we...

Date: 11/07/2014

How to prove properties of finite state machines with cccheck

In the previous post we saw how to use cccheck to prove that we did not forgot any case in a switch...

Date: 09/19/2014

How to use cccheck to prove no case is forgotten

Today we use the CodeContracts static checker to prove that no case is missing in a switch...

Date: 09/12/2014

Welcome to my blog!

Hello. I've decided to start a blog to help CodeContracts users, present some tricks to get the best...

Date: 09/03/2014