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...
שמור ב:
| מחבר ראשי: | |
|---|---|
| מחברים אחרים: | |
| פורמט: | Thèse et Mémoire papier |
| שפה: | Français |
| יצא לאור: |
[Lieu de publication inconnu] :
[Éditeur inconnu]
1997.
|
| נושאים: | |
| הערה: |
Thèse : 1997ORLE2005 |
| Autres localisations: | Voir dans le Sudoc |
| סיכום: | 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. |
|---|---|
| תאור פריט: | Thèse : 1997ORLE2005 |
| תיאור פיזי: | 1 vol. (271 p.) ; 30 cm. |
| ביבליוגרפיה: | 110 réf. bibliogr. |