Skip to Main content Skip to Navigation
New interface
Conference papers

A Certified Denotational Abstract Interpreter

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 : Abstract Interpretation proposes advanced techniques for static analysis of programs that raise specific challenges for machine-checked soundness proofs. Most classical dataflow analysis techniques iterate operators on lattices without infinite ascending chains. In contrast, abstract interpreters are looking for fixpoints in infinite lattices where widening and narrowing are used for accelerating the convergence. Smart iteration strategies are crucial when using such accelerating operators because they directly impact the precision of the analysis diagnostic. In this paper, we show how we manage to program and prove correct in Coq an abstract interpreter that uses iteration strategies based on program syntax. A key component of the formalization is the introduction of an intermediate semantics based on a generic least-fixpoint operator on complete lattices and allows us to decompose the soundness proof in an elegant manner.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : David Pichardie Connect in order to contact the contributor
Submitted on : Friday, November 19, 2010 - 1:57:54 PM
Last modification on : Thursday, January 20, 2022 - 4:20:12 PM
Long-term archiving on: : Friday, October 26, 2012 - 4:01:37 PM


Publisher files allowed on an open archive


  • HAL Id : inria-00537810, version 1


David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. pp.9-24. ⟨inria-00537810⟩



Record views


Files downloads