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...

Full description

Bibliographic Details
Main Author: Cornilleau, Pierre-Emmanuel
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