Title: Formal verification of a static analyzer: abstract interpretation in type theory
Abstract: 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.)