Techniques de vérification et de validation
- Enseignant: Michael Blondin
- Plan de cours
- Horaire:
- jeudi: 15h30 à 17h20 au D4−2021
- vendredi: 10h30 à 11h20 au D4−2021
- Examen final: vendredi 16 déc. de 13h30 à 16h30 au D3-2031
- Disponibilités:
- Par courriel
- Sans rendez-vous:
- jeudi de 10h30 à 11h30 à mon bureau
- lundi de 14h30 à 15h30 sur Teams
- 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 (3 nov. au 10 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)
- Fiches récapitulatives: diaporama | 3 fiches par page | voir annexe des notes pour celles avec liens cliquables
- Examens antérieurs: A21 (énoncé) | A21 (sol.) | A20 (énoncé) | A20 (sol.) | H19 (énoncé) | H19 (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 28 sep.)
- Devoir 2 (notes et corrections affichées sur Genote et Turnin le 20 oct.)
- Devoir 3 (notes et corrections affichées sur Genote et Turnin le 22 nov.)
- Devoir 4 (notes et corrections affichées sur Genote et Turnin le 30 nov.)
- Devoir 5 (notes et corrections affichées sur Genote et Turnin le 14 déc.)