Index of /~adl/ens/mc/2014
Initiation au model checking
----------------------------
Cette année, je ne donnerai ni examen, ni projet.
À la place, chaque semaine, je donnerai un document à lire pour
préparer le cours la semaine suivante. Le document sera soit un
article scientifique, soit des notes de cours. Le cours suivant
commencera par un QCM sur le document en question, avant
d'appronfondir le sujet. La lecture d'un article scientifique d'une
quinzaine de pages peut vous prendre une a deux heures, donc en lire 6
vous demandera moins de temps qu'un projet. Le QCM sert évidement à
vous forcer à lire, mais aussi à pouvoir fournir une note à l'école.
Bien évidement il ne s'agit pas d'apprendre le document au point de
savoir refaire une démonstration qui s'y trouverait.
* Articles à lire:
- pour le mecredi 19 février
"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 25 février
"SAT-solving in practice", par Claessen, Een, Sheeran, et Sörensson.
http://een.se/niklas/sat_pract.pdf
Même taille que le précédent, mais auto-contenu, et moins technique:
cet article cherche à donner les grandes lignes plutôt que les
détails.
- pour le lundi 3er mars
"Reflections on trusting trust", par Ken Thompson
http://dl.acm.org/citation.cfm?id=358210
Un grand classique, bien que pas très en rapport avec le cours.
Disons que c'est un papier très court qui vous permettra de prendre
de l'avance sur l'article de la semaine suivante (plus long).
Si vous souhaitez creuser un peu plus le sujet de la sécurité des
compilateurs, vous pouvez lire (c'est facultatif)
http://www.acsa-admin.org/2005/abstracts/47.html
- pour le lundi 10 mars
"Constructing Automata from Temporal Logic Formulas: A Tutorial"
par Pierre Wolper
http://orbi.ulg.ac.be/bitstream/2268/18956/2/Wol00-fmpa.pdf
- pour le lundi 17 mars
"On the verification of temporal properties" par P. Godefroid et
G. Holzmann. http://spinroot.com/gerard/pdf/pstv93.pdf
- pour le lundi 24 mars
"Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly
LTL Model Checking"
https://www.lrde.epita.fr/~adl/dl/adl/duret.11.atva.pdf