Skip to Main content Skip to Navigation
Journal articles

Programmation d'un interpréteur abstrait certifié en logique constructive

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 static analyzer aims at automatically deducing program properties by examining its source code. Proving the correctness of an analyzer is based on semantic properties, and becomes difficult to ensure when complex analysis techniques are involved. We propose to adapt the general theory of static analysis by abstract interpretation to the framework of constructive logic. Implementing this formalism into the Coq proof assistant then allows for automatic extraction of certified analyzers. We focus here on a simple imperative language and present the computation of fixpoints by widening/narrowing and syntax-directed iteration techniques.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-01112680
Contributor : David Cachera <>
Submitted on : Tuesday, February 3, 2015 - 2:34:19 PM
Last modification on : Tuesday, June 15, 2021 - 4:14:08 PM

Links full text

Identifiers

Citation

David Cachera, David Pichardie. Programmation d'un interpréteur abstrait certifié en logique constructive. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2011, pp.28. ⟨10.3166/tsi.30.381-408⟩. ⟨hal-01112680⟩

Share

Metrics

Record views

561