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

Cette année, je ne donnerai ni examen, ni projet.

À la place, il y aura deux QCM et une fiche de lecture au choix.
Pour les QCMs, a lecture d'un article scientifique d'une
quinzaine de pages peut vous prendre une a deux heures. Pour la
fiche de lecture, il faut faire une lecture approfondie et aller
voir les références, cela prend donc 5 à 6 heures. Tout cela vous
demandera oins de temps qu'un projet. Tout cela sert évidement à
vous forcer à lire, mais aussi à pouvoir fournir une note à l'école.
Bien évidement il ne s'agit pas d'apprendre les document au point de
savoir refaire une démonstration qui s'y trouverait.

* Articles à lire:

- pour le 4 mai

  "Efficient Implementation of a BDD Package", par Brace, Rudell, et
  Bryant.
     https://www.lrde.epita.fr/~renault/teaching/imc/bryant-bdd.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 8 juin, fiche de lecture à choisir entre:

   https://www.lrde.epita.fr/~renault/teaching/imc/holzman.pdf
   https://www.lrde.epita.fr/~renault/teaching/imc/couvreur.fm.pdf
   https://www.lrde.epita.fr/~renault/teaching/imc/GS-memics.pdf
   https://www.lrde.epita.fr/~renault/teaching/imc/renault-scc.pdf

   Je vous laisse regarder et ne les commente pas: il s'agit de votre
   boulot!

   Vous penserez à apporter une version imprimée de votre fiche de
   lecture pour le cours.


- pour le 15 juin 
  "SAT-solving in practice", par Claessen, Een, Sheeran, et Sörensson.

  https://www.lrde.epita.fr/~renault/teaching/imc/satFinal.pdf

  Petit papier de 7 pages, mais auto-contenu, et moins technique que
  les papiers que vous avez pu lire la semaine dernière: cet article
  cherche à donner les grandes lignes plutôt que les détails.