Skip to Main content Skip to Navigation
Conference papers

Comparing Techniques for Certified Static Analysis

David Cachera 1 David Pichardie 1 
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : A certified static analysis is an analysis whose semantic validity has been formally proved correct with a proof assistant. The recent increasing interest in using proof assistants for mechanizing programming language metatheory has given rise to several approaches for certification of static analysis. We propose a panorama of these techniques and compare their respective strengths and weaknesses.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : David Pichardie Connect in order to contact the contributor
Submitted on : Tuesday, November 23, 2010 - 11:53:51 AM
Last modification on : Wednesday, February 2, 2022 - 3:50:44 PM
Long-term archiving on: : Friday, October 26, 2012 - 4:35:24 PM


Files produced by the author(s)


  • HAL Id : inria-00538772, version 1


David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. pp.111-115. ⟨inria-00538772⟩



Record views


Files downloads