Intervenants : Patrick Cousot, Radu Iosif, Sandrine Blazy, Sébastien Bardin

Dates : 9 – 12 janvier 2012 – ENS Lyon

Programme (prévisionnel)

1- Interprétation abstraite : application à la vérification (P. Cousot)

  • Interprétation abstraite
  • Estimation de la précision de logiciels numériques
  • Vérification de systèmes complexes intégrés sur puce
  • Vérifications statiques sur des logiciels critiques embarqués temps-réel
  • Vérification de la sécurité de protocoles cryptographiques

2- Model-checking (R. Iosif)

  • Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
  • Relationship between Weak Monadic Second-Order Logic and finite automata. Infinite automata on words (Buechi, Mueller) and on trees (Rabin) automata, and their relationship with Monadic Second-Order Logic.
  • LTL Model Checking and applications

3- Certified compilation (S. Blazy)

  • Formally verified compiler
  • Software proof codesign
  • Translation validation
  • Proof carrying code

4- Test (S. Bardin)

  • Couverture structurelle et mutations
  • Tests de régression
  • Exécution dynamique symbolique
  • Bounded model-checking

Correspondant local : Ch. Alias
Page web de l’école