CTL
28 juin 2011 - 14h00
Practical program verification for the working programmer with CodeContracts and Abstract Interpretation
par Francesco Logozzo de Microsoft Research
Abstract: In this talk I will present Clousot, an abstract interpretation-based static analyzer to be used as verifier for the CodeContracts.
Clousot is routinely used every day by many .NET programmers.
In the first part of the talk I will recall what contracts are (essentially preconditions, postconditions and object invariants), why they are almost universally accepted as good software engineering practice.
Nevertheless, their adoption is very low in practice, mainly for two reasons: (i) they require a non-negligible change in the build environment which very few professional programmers are willing to pay (e.g. a new language or a new or non-standard compiler or poor IDE integration ...); (ii) the static verification tools are either absent or they require far too much help and hugely miss automation.
The CodeContracts API is an answer to (i).
Clousot is an answer to (ii).
In the second part of the talk, I will dig deeper into the Clousot architecture, explaining: (i) why unlikely similar tools we decided to base it on abstract interpretation (essentially because of automation, inference power, generality, fine control of the cost/tradeoff ratio ...); and (ii) the new abstract domains (numerical, universal, existential, etc.) we designed and implemented.
The CodeContracts API is part of .NET 4.0. Clousot can be downloaded from the DevLabs: http://msdn.microsoft.com/es-AR/devlabs/dd491992.aspx
