Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
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
Contributor : David Cachera Connect in order to contact the contributor
Submitted on : Tuesday, February 3, 2015 - 2:34:19 PM
Last modification on : Wednesday, February 2, 2022 - 3:51:00 PM

Links full text



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⟩



Record views