Certified Static Analysis by Abstract Interpretation
Résumé
A certified static analysis is an analysis whose semantic validity has been formally proved correct with a proof assistant. We propose a tutorial on building a certified static analysis in Coq. We study a simple bytecode language for which we propose an interval analysis that allows to verify statically that no array-out-of-bounds accesses will occur.
Domaines
Langage de programmation [cs.PL]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...