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