Index of /~adl/ens/mc/2016

	Name	Last modified	Size	Description
	Parent Directory		-
	README	2021-05-20 16:04	2.3K
	US48_nocurves.svg	2021-05-20 16:04	55K
	fiche-lecture.pdf	2021-05-20 16:04	28K
	intro-1.pdf	2021-05-20 16:04	241K

Initiation au model checking
----------------------------

Enseignants:
   - 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 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é]