Skip to Main content Skip to Navigation
New interface
Conference papers

A formally-verified C static analyzer

Jacques-Henri Jourdan 1 Vincent Laporte 2 Sandrine Blazy 2 Xavier Leroy 1 David Pichardie 2 
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : This paper reports on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO C 1999 language (excluding re-cursion and dynamic allocation). Verasco establishes the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with math-ematical certitude, but also the fact that these guarantees carry over to the compiled code.
Document type :
Conference papers
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Tuesday, October 28, 2014 - 7:17:11 PM
Last modification on : Friday, January 21, 2022 - 3:15:35 AM
Long-term archiving on: : Friday, April 14, 2017 - 11:34:24 AM


Files produced by the author(s)



Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A formally-verified C static analyzer. POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. pp.247-259, ⟨10.1145/2676726.2676966⟩. ⟨hal-01078386⟩



Record views


Files downloads