Cette thèse s'inscrit dans le cadre de la vérification formelle de systèmes informatiques. Plus exactement nous nous intéressons au calcul de l'ensemble d'accessibilité d'automates étendus par des variables à domaines infinis. Bien que cet ensemble ne soit pas récursif en général, des techniques à base d'accélération permettent de le calculer en pratique. Cependant ces méthodes sont encore mal connues. Nous nous intéressons à l'étude de l'accélération, des points de vue théorique, algorithmique et implantation logicielle.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00131834 |
| Date | 20 October 2005 |
| Creators | Bardin, Sébastien |
| Publisher | École normale supérieure de Cachan - ENS Cachan |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0018 seconds