Paper Info
Title
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.
Year
DOI
Venue
2008
10.1007/978-3-642-03153-3_4
Language Engineering and Rigorous Software Development
Keywords
DocType
Volume
inductive type,structural recursive programming,error detection,programming language,hoare logic,formal study,abstract interpreter,structural abstract interpretation,theorem prover,type theory
Conference
5520
ISSN
Citations 
PageRank 
Dans LERNET Summer School (2008)
6
0.49
References 
Authors
8
1
Name
Order
Citations
PageRank
Yves Bertot144240.82