Certification of static analysis in many-sorted first-order logic
Static program analysis is a core technology for both verifying and finding errors in programs but most static analyzers are complex pieces of software that are not without error. A Static analysis formalised as an abstract interpreter can be proved sound, however such proofs are significantly harde...
Main Author: | |
---|---|
Language: | ENG |
Published: |
École normale supérieure de Cachan - ENS Cachan
2013
|
Subjects: | |
Online Access: | http://tel.archives-ouvertes.fr/tel-00846347 http://tel.archives-ouvertes.fr/docs/00/84/63/47/PDF/Cornilleau2013.pdf |