HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Structural abstract interpretation, A formal study using Coq

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Abstract interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to describe an abstract interpreter using the type-theory based theorem prover Coq, using inductive types for syntax and structural recursive programming for the abstract interpreter's kernel. The abstract interpreter can then be proved correct with respect to a Hoare logic for the programming language.
Document type :
Conference papers
Complete list of metadata

Contributor : Yves Bertot Connect in order to contact the contributor
Submitted on : Monday, October 20, 2008 - 4:17:06 PM
Last modification on : Thursday, January 20, 2022 - 5:30:45 PM
Long-term archiving on: : Tuesday, September 21, 2010 - 5:32:20 PM


Files produced by the author(s)


  • HAL Id : inria-00329572, version 2
  • ARXIV : 0810.2179



Yves Bertot. Structural abstract interpretation, A formal study using Coq. LERNET Summer School, Ana Bove and Jorge Sousa Pinto, Feb 2008, Piriapolis, Uruguay. ⟨inria-00329572v2⟩



Record views


Files downloads