Compilation formellement vérifiée de code C de bas-niveau
Cette thèse présente une extension du compilateur CompCert permettant de fournir des garanties formelles de préservation sémantique à des programmes auxquels CompCert n'en donne pas. CompCert est un compilateur pour le langage C vers différentes architectures qui fournit, en plus d'un exéc...
Main Author: | |
---|---|
Other Authors: | |
Language: | en |
Published: |
2016
|
Subjects: | |
Online Access: | http://www.theses.fr/2016REN1S088/document |