Notes et transparents du cours

• Cours 1 : Model Checking Modulo Theories (version à imprimer)

Les programmes Cubicle du cours :

• ex1.cub
• ex2.cub
• ex3.cub
• ex4.cub
• ex5.cub
• Thèses
• Thèse d'Alain Mebsout sur cubicle
• Thèse de David Declerck sur cubicle-W
• Slides de la thèse de Davis Declerck sur cubicle-W
• Thèse de Mattias Roux sur des extensions de Cubicle
• Cours 2 : Satisfiability Modulo Theories (version à imprimer)
• Compléments
• Notes du cours sur SAT/SMT à l'EJCIM 2018 (S. Conchon / L. Simon)
• Slides sur SMT à l'EJCIM 2018 (S. Conchon)

TP

• TP1 : le protocole MSI (msi_basic.ml, msi.ml) (msi_basic.cub, msi.cub)
• TP2 : L'algorithme de Peterson (peterson_sc.cub, peterson_tso.cub), peterson_tso_fixed.cub)

Examens des années précédentes

• 2015-2016
• TP noté 2017-2018
• 2018-2019