Contribution à la validation de programmes concurrents avec contraintes
Considerant, d'une part le paradigme cc propose par vijay saraswat, et d'autre part les methodes de preuves en programmation logique developpees par pierre deransart, l'objectif de la these est de tenter de rapprocher ces deux univers en proposant une contribution a la validation de p...
Bewaard in:
| Hoofdauteur: | |
|---|---|
| Andere auteurs: | |
| Formaat: | Thèse et Mémoire papier |
| Taal: | Français |
| Gepubliceerd in: |
[Lieu de publication inconnu] :
[Éditeur inconnu]
1997.
|
| Onderwerpen: | |
| Opmerking: |
Thèse : 1997ORLE2005 |
| Autres localisations: | Voir dans le Sudoc |
| LEADER | 02200nam a22003017a 4500 | ||
|---|---|---|---|
| 001 | 184052 | ||
| 008 | 990313s1997 xxe ||| |||| 00| 0 fre d | ||
| 009 | PPN043710956 | ||
| 041 | 0 | |a fre |b fre | |
| 082 | |a 005.115 |z fre | ||
| 084 | |a 004 | ||
| 100 | 1 | |a Chambre, Pascal. | |
| 245 | 1 | 0 | |a Contribution à la validation de programmes concurrents avec contraintes |c Pascal Chambre ; sous la direction de Pierre Deransart. |
| 260 | |a [Lieu de publication inconnu] : |b [Éditeur inconnu], |c 1997. | ||
| 300 | |a 1 vol. (271 p.) ; |c 30 cm. | ||
| 500 | |a Thèse : 1997ORLE2005 | ||
| 502 | |a Thèse de doctorat. Informatique. Orléans. 1997 | ||
| 504 | |a 110 réf. bibliogr. | ||
| 520 | |a Considerant, d'une part le paradigme cc propose par vijay saraswat, et d'autre part les methodes de preuves en programmation logique developpees par pierre deransart, l'objectif de la these est de tenter de rapprocher ces deux univers en proposant une contribution a la validation de programmes concurrents avec contraintes. Nous definissons d'abord une nouvelle classe de cc permettant de donner une semantique arborescente aux programmes concurrents similaire a celle des arbres de preuve pour les programmes logiques : la semantique des arbres de comportement. Nous definissons ensuite de nouvelles methodes de preuve pour programmes logiques permettant de valider des proprietes dynamiques dans des arbres de preuve incomplets. Enfin ces nouvelles methodes sont appliquees dans le cadre de la nouvelle semantique proposee pour les programmes concurrents avec contraintes permettant de faire des preuves de proprietes specifiques a la concurrence telle l'absence de deadlock. | ||
| 650 | |a Logiciels |x Validation | ||
| 650 | |a Concurrence | ||
| 650 | |a Programmation par contraintes | ||
| 650 | |a Sémantique | ||
| 650 | |a Théorie de la démonstration | ||
| 650 | |a Thèses et écrits académiques | ||
| 700 | 1 | |a Deransart, Pierre, |d 1945- |4 ths | |
| 710 | 2 | |a Université d'Orléans. |4 dgg | |
| 997 | |0 184052 |1 Thèse et Mémoire papier |a Ressource papier |c 0/Orléans/ |c 1/Orléans/BU Sciences, Technologies, STAPS/ |z Orléans, BU Sciences, Technologies, STAPS, TS 19-1997-5 |z Orléans, BU Sciences, Technologies, STAPS, TS 19-1997-5 b | ||