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

https://hal.inria.fr/inria-00538772
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

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00538772, version 1

Citation

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⟩

Share

Metrics

Record views

171

Files downloads

54