FIIL : software model checking
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
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
Cubicle
et
CubicleW
sont accessibles sur vos machines en ajoutant
/public/conchon/
à votre variable
PATH
.
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