(Joint work with Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, and David Pichardie)

Static analysis is the automatic inference and checking of simple properties of all executions of a program. Initially developed in the context of compilers to support code optimization, static analysis is successful today for the formal verification of safety properties of critical software.

Abstract interpretation provides an elegant, powerful mathematical framework to define and reason about static analyses. However, the classic presentation for abstract interpretation, based on Galois connections, is set-theoretic and not constructive. This is an issue when one wants to verify a static analyzer using Coq, Agda, or other provers based on type theory.

In this talk, I will present a type-theoretic account of abstract interpretation, originally developed by David Pichardie, and show how it scales up to the verification of Verasco, a realistic static analyzer for the C language that has been developed and proved correct using Coq as a programming language and as a proof assistant.

For more information: http://compcert.inria.fr/verasco/