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

  • Article

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...

Author: Francesco Logozzo 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...

Author: Francesco Logozzo 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...

Author: Francesco Logozzo 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...

Author: Francesco Logozzo 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...

Author: Francesco Logozzo Date: 09/03/2014