Techniques de vérification et de validation
- Enseignant: Michael Blondin
- Plan de cours:
- Horaire:
- mardi: 13h30 à 14h20 au D3-2029
- jeudi: 15h30 à 17h20 au D3-2033
- Disponibilités:
- Par courriel
- Sans rendez-vous à mon bureau (D4-1024-1):
- mardi de 14h30 à 15h30
- jeudi de 11h30 à 12h30
- autre moment si ma porte est entrouverte
- Avec rendez-vous à mon bureau ou sur Teams
Annonces
- Vous êtes encouragé·e·s à remplir la rétroaction de mi-session (29 oct. au 6 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écap.: diaporama | 3 fiches par page | voir annexe pour celles avec liens cliquables
- Examens antérieurs: A23 | A23 (sol.) | A22 | A22 (sol.) | A21 | A21 (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: similaire mais pas nécessairement identique à 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 30 sep.)
- Devoir 2 (notes et corrections affichées sur Genote et Turnin le 18 oct.)
- Devoir 3 (notes et corrections affichées sur Genote et Turnin le 6 nov.)
- Devoir 4 (notes et corrections affichées sur Genote et Turnin le 19 nov.)
- Devoir 5 (notes et corrections affichées sur Genote et Turnin le 9 déc.)