Formal verification of a static analyzer: abstract interpretation in type theory

Xavier Leroy (1)

1 GALLIUM - Programming languages, types, compilation and proofs

This invited talk describes the logical foundations and the status of the ongoing Verasco project, whose aim is to formalize and prove sound a static analyzer for the C programming language based on abstract interpretation, using the Coq proof assistant. (Joint work with David Pichardie, Sandrine Blazy, Jacques-Henri Jourdan, and Vincent Laporte.)

Domaines: Langage de programmation [cs.PL]

Xavier Leroy. Formal verification of a static analyzer: abstract interpretation in type theory. Types - The 2014 Types Meeting, May 2014, Paris, France. ⟨hal-00983847⟩