Index of /~adl/ens/mc/2017
Initiation au model checking
----------------------------
Enseignants:
- Maximilien Colange <max@lrde.epita.fr>
- Alexandre Duret-Lutz <adl@lrde.epita.fr>
- Étienne Renault <renault@lrde.epita.fr>
Ce cours est validé par un contrôle continu, non pas de votre
connaissance du cours, mais de votre préparation du cours...
On vous demande en effet de lire quelques articles scientifiques, afin
de préparer les cours. Vos lectures seront contrôlées par un QCM ou
le rendu d'une fiche de lecture.
* Articles à lire:
- pour le mardi 21 février (le cours commencera par un QCM sur cet article)
"Efficient Implementation of a BDD Package", par Brace, Rudell, et Bryant.
http://www.ccs.neu.edu/home/pete/courses/Decision-Procedures/2007-Fall/readings/Brace_Rudell_Bryant_Efficient_Implementation_BDD_Package.pdf
Seulement 6 pages, mais ne vous réjouissez pas trop vite: les
articles courts contraignent souvent les auteurs à abréger l'énoncé
du problème pour pouvoir aborder plus rapidement le sujet. Dans le
cas présent, le sujet vous paraitra sans doute obscur si vous n'avez
jamais vu l'ombre d'un BDD. Comme les auteurs s'en doutent
il vous conseillent d'aller lire la référence [13] avant.
À peu près aussi long, mais peut être plus digeste :
http://configit.com/configit_wordpress/wp-content/uploads/2013/07/bdd-eap.pdf
La page wikipedia sur les BDD suffit peut-être.
- pour le mardi 28 février (le cours commencera par un QCM sur cet article)
"Timed Automata" de Rajeev Alur, CAV'99.
https://www.cis.upenn.edu/~alur/Cav99.ps
- pour le mardi 21 mars
rendre une fiche de lecture sur *un* papier à choisir parmi
- "On the Verification of Temporal Properties" par P. Godefroid
et G. Holzmann.
- "On-the-fly Verification of Linear Temporal Logic" par Jean-Michel
Couvreur
- "Comparison of Algorithms for Checking Emptiness on Büchi Automata"
par Andreas Gaiser and Stefan Schwoon
- "Three SCC-based Emptiness Checks for Generalized Buchi Automata"
par E. Renault, A. Duret-Lutz, F. Kordon et D. Poitrenaud
Voyez REVIEW_TEMPLATE.pdf pour un exemple de fiche.