De la sémantique opérationnelle à la spécification formelle de compilateurs (Record no. 59373)

005 - numéro d'identification de la version
identification de la version 20200818032923.0
009 - PPN
PPN 114133158
099 ## - Informations locales
date creation notice (koha) 2005-10-26
date modification notice (koha) 2011-05-20
100 ## - données générales de traitement
données générales de traitement 20070425d2004 k y0frey50 ba
200 1# - titre
Titre propre De la sémantique opérationnelle à la spécification formelle de compilateurs
indication générale du type de document Texte imprimé
Sous-titre l'exemple des boucles en Esterel
Auteur principal par Olivier Tardieu
Auteur(s) secondaire(s) sous la direction de Gérard Berry
210 ## - éditeur
Lieu de publication [S.l.]
Nom de l'éditeur [s.n.]
Date de publication 2004
215 ## - Description matérielle
Caractéristiques matérielles 1 vol. (130 p.)
Format 30 cm
310 ## - note
texte de la note Publication autorisée par le jury
320 ## - note
texte de la note Bibliogr. 86 réf.
328 #0 - note
Détails sur la thèse ou le mémoire dont le type de diplôme Thèse de doctorat
Discipline Informatique temps réel, robotique et automatique
Organisme donnant le diplôme Paris, ENMP
Date du diplôme 2004
330 ## - résumé
texte de la note Esterel est un langage impératif synchrone pour la programmation de systèmes réactifs orientés contrôle. De façon à dériver une description formelle de compilateur Esterel à partir d’une sémantique opérationnelle du langage, nous proposons une nouvelle sémantique qui exclut les exécutions non déterministes. Puis nous nous concentrons sur les problèmes posés par la compilation des boucles. Les primitives du langage à l’exception de l’instruction « pause » s’exécutent sans consommer de temps logique. Par conséquent les boucles peuvent conduire à la répétition instantanée d’un même bloc de code, d’où de possibles blocages (répétition infinie) et des comportements difficiles à implémenter correctement (répétition finie). À l’aide d’une nouvelle instruction de saut non instantané « gotopause » et en combinant analyse statique et réécriture de code, nous spécifions un schéma de compilation des boucles à la fois portable, performant et sûr. Nous démontrons sa correction.
330 ## - résumé
texte de la note Esterel is a synchronous imperative design language for the specification of control-oriented reactive systems. In order to formally derive the specification of an Esterel compiler from the operational semantics of the language, we first describe a new semantics for Esterel that discards non-deterministic executions. Then, we show how to understand and solve the problems in compilers raised by the “loop” construct of Esterel. All primitive instructions except for “pause” execute in zero time. Thus, because of loops, a given piece of code may be executed several times in a single instant, potentially leading to complex (finite loop) or incorrect (infinite loop) behaviors. Using a new non-instantaneous jump instruction called “gotopause”, and combining program rewriting with static analysis techniques, we build a safe code generation scheme for loop structures that rejects incorrect loops and compiles correct loops very efficiently. We formalize and prove the correctness of this scheme.
541 ## - titre traduit ajouté par le catalogueur
titre traduit Loops in Esterel
complément du titre from Operational Semantics to Formally Specified Compilers
langue du titre traduit eng
610 ## - sujets
sujet SEMANTIQUE
610 ## - sujets
sujet LANGAGE ESTEREL
610 ## - sujets
sujet COMPILATION
610 ## - sujets
sujet Analyse statique
610 ## - sujets
sujet Concurrence
610 ## - sujets
sujet Langage ESTEREL
610 ## - sujets
sujet Sémantique
610 ## - sujets
sujet Transformation programme
610 ## - sujets
sujet Transformation de programme
606 ## - sujets
-- ba0yba0y
-- frefre
sujet Logiciels
subdivision du sujet Vérification
code du système d'indexation rameau
606 ## - sujets
-- ba0yba0y
sujet Algorithmes
-- frefre
subdivision du sujet Thèses et écrits académiques
code du système d'indexation rameau
606 ## - sujets
-- ba0yba0y
sujet Algorithmes
-- frefre
606 ## - sujets
-- ba0yba0y
sujet Temps réel (informatique)
-- frefre
subdivision du sujet Thèses et écrits académiques
code du système d'indexation rameau
606 ## - sujets
-- ba0yba0y
sujet Compilation (informatique)
-- frefre
subdivision du sujet Thèses et écrits académiques
code du système d'indexation rameau
700 #1 - auteur
Lien 391072
numéro de la notice d'autorité 114133492
Auteur Tardieu
_ Olivier
dates 1976-....
code de fonction Auteur
712 0# - collectivité - mention de responsabilité secondaire
-- ba0yba0y
élément d'entrée
élément ajouté au nom ou qualificatif Paris
numéro de la notice d'autorité 026375249
code de fonction Organisme de soutenance
702 #1 - nom de personne - mention de responsabilité secondaire
Lien 386211
-- ba0yba0y
élément d'entrée Berry
partie du nom autre que l'élément d'entrée Gérard
dates 1948-....
numéro de la notice d'autorité 059760214
code de fonction Directeur de thèse
856 ## - accès
Texte intégral <a href="http://pastel.archives-ouvertes.fr/pastel-00001336">http://pastel.archives-ouvertes.fr/pastel-00001336</a>
909 ## - Type de document
Type de document Thèses
Holdings
Perdu Site d'origine Localisation Numero d'inventaire cote Statut de l'exemplaire note sur l'exemplaire Propri
Présent Bib. Paris Bib. Paris EMP 152.369 CCL.TH.1111 EMP 152.369 CCL.TH.1111 Empruntable Thèse en ligne Publications de l'Ecole
Présent Bib. Paris Bib. Paris EMP 152.368 CCL.TH.1111 EMP 152.368 CCL.TH.1111 Empruntable Thèse en ligne Publications de l'Ecole
Présent Centre de recherche en informatique Centre de recherche en informatique   04 TAR Sur demande Thèse en ligne Centre de Recherche en Informatique
Présent Sophia Antipolis Sophia Antipolis EMS T-CMA-055 EMS T-CMA-055 Sur demande Thèse en ligne Sophia-Antipolis

Powered by Koha