Steps toward usable verification

September 1, 2014
Francesco Logozzo | MSR Redmond

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.

Speaker Details

Francesco Logozzo is a researcher at Microsoft Research, Redmond. His main research interest are abstract interpretation, verification, and program optimization. He joined MSR in October 2006 as a post-doc. Before moving overseas, he was a post-doc at ENS, Paris with Patrick Cousot, and a Ph.D. student at Ecole Polytechnique under the supervision of Radhia Cousot. Before moving to France, he was a student of the Scuola Normale Superiore of Pisa. He published papers in the most important conferences, gave invited talks in Academic and Industrial conferences, co-chaired SAS and VMCAI, was member of many program committees, but most importantly he is a big lover of both theoretical and experimental cycling.