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 metadatas

https://hal.inria.fr/inria-00329572
Contributor : Yves Bertot <>
Submitted on : Monday, October 13, 2008 - 11:03:10 AM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on : Monday, June 7, 2010 - 7:29:13 PM

Files

absint.pdf
Files produced by the author(s)

Identifiers

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

Citation

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

Share

Metrics

Record views

22

Files downloads

49