Techniques de vérification et de validation
- Enseignant: Michael Blondin
- Plan de cours:
- Horaire:
- jeudi: 08h30 à 10h20 au D4−2022
- vendredi: 10h30 à 11h20 au D4−2021
- Disponibilités:
- Par courriel
- Sans rendez-vous:
- mardi de 14h30 à 16h00 à mon bureau
- autre moment: à mon bureau si la porte est entrouverte
- Avec rendez-vous: à mon bureau ou sur Teams
Annonces
- Vous êtes encouragé·e·s à remplir la rétroaction de mi-session (2 nov. au 9 nov., anonyme et non officielle)
Calendrier
Matériel
Références
Matériel d'étude
- Structure de l'examen
- Matériel permis: une seule feuille de notes recto verso au format 8½" × 11" (rédigée à la main ou l'ordinateur) + les fiches récapitulatives qui seront annexées à l'examen
- Fiches récapitulatives: diaporama | 3 fiches par page | voir annexe des notes pour celles avec liens cliquables
- Examens antérieurs: A22 (énoncé) | A22 (sol.) | A21 (énoncé) | A21 (sol.) | A20 (énoncé) | A20 (sol.)
- Exercices: voir la fin de chaque chapitre des notes (plusieurs solutions sont en annexe)
Références complémentaires
- Capsules vidéos de 2020 (attention: contenu similaire mais pas nécessairement identique à celui de cette session)
- Javier Esparza, David Hansel, Peter Rossmanith, Stefan Schwoon: Efficient algorithms for model checking pushdown systems. Proc. 12th International Conference on Computer Aided Verification (CAV), pp. 232–247, 2000.
- Henrik Reif Andersen: An Introduction to Binary Decision Diagrams, 1997.
- Christel Baier, Joost-Pieter Katoen: Principles of Model Checking. MIT Press, 2008. (Errata )
Devoirs
- Devoir 1 (notes et corrections affichées sur Genote et Turnin le 29 sep.)
- Devoir 2 (notes et corrections affichées sur Genote et Turnin le 24 oct.)
- Devoir 3 (notes et corrections affichées sur Genote et Turnin le 13 nov.)
- Devoir 4 (notes et corrections affichées sur Genote et Turnin le 21 nov.)
- Devoir 5 (notes et corrections affichées sur Genote et Turnin le 9 déc.)