Formal verification of a synchronous data-flow compiler : from Signal to C

Formal verification of a synchronous data-flow compiler : from Signal to C

Show other versions (2)

Les langages synchrones tels que Signal, Lustre et Esterel sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation er...

Full description

Bibliographic Details
Main Author: Ngô, Van Chan
Other Authors: Rennes 1
Language:en
Published: 2014
Subjects:
Vérification formelle
Validation de la traduction
Compilateur validé
Programmes synchrones
Modèles polychrones
Systèmes embarqués
Systèmes critiques
Détection des blocages
Compilation
Polychrony
Graphiques de dépendance
SMT solving
Valeur-graphiques
Graphique réécriture.
Formal verification
Translation validation
Validated Compiler
Synchronous Programs
Polychronous Models
Embedded systems
Safety-critical systems
Deadlock detection
Dependency graphs
Value-graphs
Graph rewriting.
Online Access:http://www.theses.fr/2014REN1S034/document

Internet

http://www.theses.fr/2014REN1S034/document

Similar Items