Page du cours de Software Verification, partie 1

Le cours est enseigné par Vincent Penelle, le lundi de 11h à 12h20 et le mercredi de 9h30 à 12h20.

Matériel de cours

Le poly (en anglais) est ici.

Exercices et bases de code

Tutorial sur OCaml. (pdf) (HTML) (English pdf) (English HTML).
TP sur les SMT-solvers: (pdf) (HTML) (English pdf) (English HTML) Base de code
TP concernant l’implémentation de la sémantique des control-flow automata: (pdf) (HTML) (English pdf) (English HTML) Base de code
TP concernant l’implémentation du Bounded Model-Checking: (pdf) (HTML) (English pdf) (English HTML) Base de code

Pour travailler au CREMI :

Vous devez tapez les commandes suivantes dans un terminal pour compiler le travail du cours :

export OPAMROOT=/opt/local/opam
eval $(opam env)

Si vous travaillez sur vs-code, lancez vs-code ensuite dans le même terminal. Nous vous conseillons de travailler avec l’extension OCaml-platform de vs-code.

Pour travailler chez vous :

Il vous faut installer les paquets que nous utilisons dans ce cours.

Pour cela, vous avez tout d’abord besoin d’installer opam via votre gestionnaire de paquet. Vous trouverez plus d’informations ici.

Une fois cela fait, il faut initialiser opam avec la commande opam init, puis installer les paquets nécessaires avec la commande suivante :

opam install z3 dune menhir odoc zarith

Tout comme au CREMI, nous vous conseillons d’utiliser vs-code et l’extension OCamlPlatform. Pour en tirer le meilleur parti (en particulier le typage à la volée), nous vous conseillons d’installer en plus les paquets suivants :

opam install ocamlformat ocaml-lsp-server

Vous n’aurez à faire tout ce qui précède qu’une fois.

Attention cependant, par défaut, les paquet installés via opam ne sont pas dans votre PATH. Il faut (dans chaque terminal où vous souhaitez travailler sur le cours) de taper la commande suivante :

eval $(opam env)

Quelques ressources:

Quelques références:

L’article introduisant le Bounded Model Checking (sur des systèmes finis).
L’article expliquant comment appliquer le BMC sur des systèmes infinis.
CBMC: un outil qui fait du Bounded Model Checking sur du code C.
Une école d’été sur la vérification de 2008, dont les transparent de Clark Barrett ont servi d’inspiration à la partie sur les SMT-solveurs.

(Obsolète) Transparents servant de base au cours avant l’écriture du poly:

Attention, ce matériel est assez fragmentaire (le poly est un peu plus complet).