FIIL : software model checking
Les 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
Cours 2 :
Satisfiability Modulo Theories
(version à
imprimer
)
TP
Cubicle
est accessible sur vos machines en ajoutant
/public/kn/bin
à votre variable
PATH
.
TP1 :
le protocole MSI
(
msi_basic.ml
,
msi.ml
) (
msi.cub
,
msi2.cub
,
msi3.cub
)
TP noté :
L'algorithme de Szymanski