Structural abstract interpretation, A formal study using Coq
| dc.creator | Bertot, Yves | |
| dc.date | 2008-10-13 | |
| dc.date | 2008-10-20 | |
| dc.date.accessioned | 2026-07-07T10:11:13Z | |
| dc.date.available | 2026-07-07T10:11:13Z | |
| dc.description | 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. | |
| dc.identifier | https://arxiv.org/abs/0810.2179 | |
| dc.identifier | http://arxiv.org/abs/0810.2179 | |
| dc.identifier | Dans LERNET Summer School (2008) | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/171795 | |
| dc.subject | Logic in Computer Science | |
| dc.title | Structural abstract interpretation, A formal study using Coq | |
| dc.type | text |