Initiation au model checking ---------------------------- Enseignants: - Alexandre Duret-Lutz - Étienne Renault 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 23 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 1er mars (le cours commencera par un QCM sur cet article) "SAT-solving in practice", par Claessen, Een, Sheeran, et Sörensson. http://www.cse.chalmers.se/edu/year/2012/course/TDA956/Papers/satFinal.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 mardi 15 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 - pour le 22 mars 2016 [pas encore décidé]