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.)
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [6 references]  Display  Hide  Download

https://hal.inria.fr/hal-00983847
Contributor : Xavier Leroy <>
Submitted on : Friday, April 25, 2014 - 7:18:32 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Document(s) archivé(s) le : Friday, July 25, 2014 - 12:30:21 PM

File

invited-2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00983847, version 1

Collections

Citation

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

Share

Metrics

Record views

349

Files downloads

130