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