| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Structural abstract interpretation, A formal study using Coq
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.
https://hal.inria.fr/inria-00329572
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
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