Réécriture et compilation de confiance

Abstract : Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations.
Document type :
Theses
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01752777
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 1:57:41 PM
Last modification on : Tuesday, April 24, 2018 - 1:30:13 PM

File

2006_REILLES_A.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01752777, version 1

Collections

Citation

Antoine Reilles. Réécriture et compilation de confiance. Autre [cs.OH]. Institut National Polytechnique de Lorraine, 2006. Français. ⟨NNT : 2006INPL084N⟩. ⟨tel-01752777⟩

Share

Metrics

Record views

27

Files downloads

46