Spécification et vérification de programmes orientés objets en logique de séparation
Cette thèse propose une extension de la logique de séparation pour les programmes parallèles et orientés-objets. La logique de séparation est un formalisme récent et prometteur pour vérifier les programmes impératifs. Cependant, jusqu'à présent, la logique de séparation a été appliquée à des pr...
| Main Author: | |
|---|---|
| Language: | ENG |
| Published: |
Université de Nice Sophia-Antipolis
2009
|
| Subjects: | |
| Online Access: | http://tel.archives-ouvertes.fr/tel-00424979 http://tel.archives-ouvertes.fr/docs/00/42/49/79/PDF/these-clement-hurlin.pdf http://tel.archives-ouvertes.fr/docs/00/42/49/79/ANNEX/presentation-soutenance.pdf |