Analyse automatique de terminaison

Cours

S1

• Justifier informellement la terminaison de tous les algorithmes présentés dans cette fiche
• A lire : Proving Program Termination (Byron Cook, Andreas Podelski et Andrey Rybalchenko)

S2

• Résumé de l'article Proving Program Termination
• Etude de la preuve (Christopher Strachey) de l'indécidabilité du problème de l'arrêt

S3

• Rappels (Christine Paulin-Mohring) sur les ordres
• Terminer l'étude de l'article Proving Program Termination
• A lire Eventual Linear Ranking Functions (Roberto Bagnara et Fred Mesnard), transparents

S4

• Etude de l'article Eventual Linear Ranking Functions (Roberto Bagnara et Fred Mesnard), transparents
• Exercices

S5

• Justifier la terminaison de tous les algorithmes présentés dans cette fiche, utilisation du démonstrateur Z3
• A lire : Proving programs terminate using well orderings, Ramsey Theory, and Matrices (William Gasarch)

S6

• Résumé l'article Proving programs terminate using well orderings, Ramsey Theory, and Matrices
• A lire : Transition Invariants and Transition Predicate Abstraction for Program Termination (Andreas Podelski et Andrey Rybalchenko)

S7

• Transition Invariants and Transition Predicate Abstraction (transparents)

Evaluation

En contrôle continu, un partiel écrit 50% + un exposé 50% (un étudiant par exposé, 15 minutes, transparents en français, démo éventuelle)