Initiation au model checking ---------------------------- Enseignants: - Maximilien Colange - 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 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.