Next: About this document ...
Up: Contenu des cours spécifiques
Previous: Première période
- Model-Checking (Approche algorithmique pour la vérification)
- Algorithmes de vérification (décider si un programme satisfait une propriété)
par model-checking,
- Techniques de model-checking symbolique,
- Model-checking pour systèmes temps-réel,
- Outils de vérification automatique.
- Preuve de programmes (Approche déductive pour la vérification)
- Principes généraux de la preuve aidée par ordinateur,
- Preuves de programmes séquentiels (invariants, terminaison),
- Preuves de systèmes réactifs concurrents (invariants, sûreté, vivacité).
- Outils de preuve.
- Analyse Statique de Programmes
- Notion d'interprétation abstraite,
- Techniques d'analyse statique abstraite de programmes,
- Calcul d'invariants, debuggage, typage, optimisation de code.
- Méthodes de Test
- Principes généraux: clear-box (white-box) testing, black-box testing,
- Cas des programmes séquentiels, systèmes concurrents (synchrones / asynchrones - protocoles), systèmes temporisés,
- Techniques algorithmiques pour la génération automatique de cas de test
à partir des spécifications,
- Outils de génération automatique de tests.
- Vérification de la Sécurité
- Vérification de protocoles cryptographiques, protocoles de non-répudiation, etc.
- Vérification et analyse de propriétés sur le controle d'accés, les flots d'information,
noninterference, etc
- Méthodes déductives pour la sécurité.
- Contrôle et ordonnancement
- Algorithmes de synthèse de contrôleurs.
Cas des systèmes temps réels. Lien avec les jeux.
- Problèmes d'ordonnancement de tâches.
Approche basée sur les automates temporisés.
Next: About this document ...
Up: Contenu des cours spécifiques
Previous: Première période
Ahmed Bouajjani
2005-05-22