Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis
Ce document présente différents outils pour représenter et manipuler des ensembles infinis de n-uplets d'arbres appelés langages de n-uplets d'arbres. Nous avons choisi la programmation logique comme formalisme pour décrire les langages de n-uplets d'arbre (c.à.d. les relations) et le...
Gorde:
| Egile nagusia: | |
|---|---|
| Formatua: | Thèse numérique |
| Hizkuntza: | Français |
| Argitaratua: |
Villeurbanne :
[CCSD]
2010.
|
| Gaiak: | |
| Sarrera elektronikoa: | Accès au texte intégral Accès Université d'Orléans |
| Oharra: |
Description d'après la consultation, 2018-04-26 Titre provenant de l'écran titre Cette édition peut différer de la version de soutenance enregistrée sous le Numéro National de Thèse : 2007ORLE2050 Thèses CCSD |
| Autres localisations: | Voir dans le Sudoc |
| Variante du titre: | Using tree languages for modelise and verify infinite states systems |
| Edition sous un autre format: | • Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis, par Pierre Pillot, [S.l.], [s.n.], 2007, 1 vol. (130 p.) |
| LEADER | 03459nam a22003137a 4500 | ||
|---|---|---|---|
| 001 | 928103 | ||
| 008 | 180502s2010 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN226595161 | ||
| 041 | 0 | |a fre |b fre |b eng | |
| 084 | |a 004 | ||
| 100 | 1 | |a Pillot, Pierre, |d 1979- . | |
| 240 | 1 | 0 | |a Using tree languages for modelise and verify infinite states systems |
| 245 | 1 | 0 | |a Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis |c par Pierre Pillot. |
| 256 | |a Données textuelles | ||
| 260 | |a Villeurbanne : |b [CCSD], |c 2010. | ||
| 500 | |a Description d'après la consultation, 2018-04-26 | ||
| 500 | |a Titre provenant de l'écran titre | ||
| 500 | |a Cette édition peut différer de la version de soutenance enregistrée sous le Numéro National de Thèse : 2007ORLE2050 | ||
| 500 | |a Thèses CCSD | ||
| 502 | |a Texte remanié de. Thèse de doctorat. Informatique. Orléans. 2007 | ||
| 520 | |a Ce document présente différents outils pour représenter et manipuler des ensembles infinis de n-uplets d'arbres appelés langages de n-uplets d'arbres. Nous avons choisi la programmation logique comme formalisme pour décrire les langages de n-uplets d'arbre (c.à.d. les relations) et les techniques de transformations de programmes pour calculer les opérations sur ceux-ci. Dans un premier temps on étudie une classe de relations closes par la plupart des opérations ensemblistes, la classe des relations pseudo-régulières. Grâce à un lien entre programmes logiques et systèmes de réécriture, nous définissons des classes de systèmes de réécriture conditionnelle dont la clôture transitive est une relation pseudo-régulière. On applique ce résultat pour donner une classe décidable de formules du premier ordre basées sur le prédicat de joignabilité où R est un système de réécriture conditionnel pseudo-régulier. Ensuite on étend ce résultat au second ordre, les variables du second ordre étant interprétées comme des relations. A partir d'un algorithme général original décidant de la satisfiabilité de formules du second ordre sous certaines conditions, nous représentons une instance des variables du second ordre en système de réécriture conditionnel. On montre que ce travail peut permettre la synthèse automatique de programme. Dans un dernier temps, nous utilisons des sur-approximations pour des tests d'inconsistances. A cet effet, nous utilisons une classe de programmes logiques non réguliers dont le test du vide est décidable pour effectuer la sur-approximation. Nous appliquons finalement cette méthode à la vérification de protocoles cryptographiques. | ||
| 538 | |a Un logiciel capable de lire un fichier au format PDF | ||
| 650 | |a Langages de programmation logique | ||
| 650 | |a Réécriture, Systèmes de (informatique) | ||
| 650 | |a Thèses et écrits académiques | ||
| 776 | 0 | |0 125260717 |t Utilisation des langages d'arbres pour la modélisation et la vérification des systèmes à états infinis |f par Pierre Pillot |c [S.l.] |n [s.n.] |d 2007 |p 1 vol. (130 p.) | |
| 856 | 4 | |q PDF |u https://tel.archives-ouvertes.fr/tel-00490819 |z Accès au texte intégral | |
| 856 | 4 | |5 452349901:727098012 |u https://ezproxy.univ-orleans.fr/login?qurl=https%3A//tel.archives-ouvertes.fr/tel-00490819 |z Accès Université d'Orléans | |
| 997 | |0 928103 |1 Thèse numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||