Skip to Main content Skip to Navigation
Theses

Verasco: a Formally Verified C Static Analyzer

Résumé : Afin de développer des logiciels plus sûrs pour des applications critiques, certains analyseurs statiques tentent d'établir, avec une certitude mathématique, l'absence de certains types de bugs dans un programme donné. Une limite possible à cette approche est l'éventualité d'un bug affectant la correction de l'analyseur lui-même, éliminant ainsi les garanties qu'il est censé apporter. Dans cette thèse, nous proposons d'établir des garanties formelles sur l'analyseur lui-même : nous présentons la conception, l'implantation et la preuve de sûreté en Coq de Verasco, un analyseur statique formellement vérifié utilisant l'interprétation abstraite pour le langage ISO C99 avec l'arithmétique flottante IEEE754 (à l'exception de la récursion et de l'allocation dynamique de mémoire). Verasco a pour but d'établir l'absence d'erreur à l'exécution des programmes donnés. Il est conçu selon une architecture modulaire et extensible contenant plusieurs domaines abstraits et des interfaces bien spécifiées. Nous détaillons le fonctionnement de l'itérateur abstrait de Verasco, son traitement des entiers bornés de la machine, son domaine abstrait d'intervalles, son domaine abstrait symbolique et son domaine abstrait d'octogones. Verasco a donné lieu au développement de nouvelles techniques pour implémenter des structures de données avec partage dans Coq.
Complete list of metadatas

Cited literature [102 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/tel-01327023
Contributor : Jacques-Henri Jourdan <>
Submitted on : Monday, June 6, 2016 - 12:07:50 PM
Last modification on : Thursday, April 26, 2018 - 10:28:01 AM

Licence


Distributed under a Creative Commons Attribution - NonCommercial - ShareAlike 4.0 International License

Identifiers

  • HAL Id : tel-01327023, version 1

Collections

Citation

Jacques-Henri Jourdan. Verasco: a Formally Verified C Static Analyzer. Programming Languages [cs.PL]. Universite Paris Diderot-Paris VII, 2016. English. ⟨tel-01327023⟩

Share

Metrics

Record views

1258

Files downloads

466