Model checking

Le model checking est une technique de vérification de programmes. Le problème de model checking est comme suit :

• entrée
  • un programme
  • une spécification qui décrit le comportement attendu du programme
• sortie :
  • une attestation que le programme vérifie la spécification, ou alors une exécution contre-exemple qui montre que le programme ne fonctionne pas bien.

Généralement, le model checking est utilisé sur des systèmes réactifs simples (des systèmes de transition qui ressemblent à des automates finis) et des propriétés temporelles (e.g. "une infinité de fois, x prend la valeur 0). Ici, on s'intéresse à faire du model checking sur des programmes C, avec l'outil efficient SMT-based context-bounded model checker (EBSMC, disponible ici https://github.com/esbmc/esbmc). SMT signifie satisfiability modulo theory, vous allez voir partiellement en cours de logique, ou alors dans un cours de vérification formelle en M1 ou M2, ou jamais.

La documentation est là : http://esbmc.org/

Comment écrire la spécification

Deux solutions :

• assert(x == 10) pour dire qu'ici x doit valoir 10
• __VERIFIER_assume(x < 5); pour dire que l'on suppose que x < 5

Ainsi un code comme cela :

int main() {
    int x;
    __VERIFIER_assume(x < 5);
    
    // calcul sur x

    assert(x == 10)
}

signifie que la spécification est *si x < 5 au début, alors x == 10 à la fin.

Utilisation

        esbmc programme.c

Il y a aussi des flags pour contrôler la façon dont fonctionne le model checker :

        esbmc programme.c --incremental-bmc
        esbmc programme.c --data-races-check --context-bound 3