Initiation à la vérification de programme

L'objectif de ce cours est d'initier les étudiants à la vérification de programme et plus généralement aux techniques formelles qui sont utilisées dans ces approches. L'objectif essentiel est de présenter les grands principes de la vérification et du test logiciel, les modèles sous-jacents, et de présenter quelques outils associés, et les techniques formelles utilisées. Quelques éléments étudiés: 

- Overview des méthodes et outils de validation
- Systèmes et synchronisation d'automates
- Logique temporelle
- Vérification et model-checking
- Propriétés classiques / Etudes de cas
- Introduction au test logiciel
- Techniques formelles dans le test

Initier les étudiants à la vérification de programme et plus généralement aux techniques formelles qui sont utilisées dans ces approches. 

module « logique et preuve » au S5