Résumé : Cubicle est un model-checker pour vérifier des propriétés de sureté d'algorithmes faisant intervenir un nombre quelconque de processus. Ces algorithmes sont d écrits sous forme de systèmes de transitions dits paramètres. Les propriétés de sureté ainsi que les états du système sont décrits par des formules logiques du premier ordre. Pour vérifier ces propriétés, Cubicle met en oeuvre un algorithme d'atteignabilité par chaînage arrière qui utilise un démonstrateur SMT (Satisabilité Modulo Théories). Les expériences, menées sur la vérification d'algorithmes d'exclusion mutuelle et de protocoles de cohérence de cache, montrent que Cubicle est efficace et compétitif avec les model checkers de la même famille. Cubicle est un logiciel libre d éveloppé en OCaml. Il utilise le démonstrateur Alt-Ergo zero, une version allégée et améliorée d'Alt-Ergo. Une implantation parallèle se reposant sur la bibliothèque Functory est également proposée.
https://hal.inria.fr/hal-00778832
Contributor : Ist Inria Saclay
<>
Submitted on : Monday, January 21, 2013 - 2:56:42 PM
Last modification on : Thursday, October 3, 2019 - 2:04:03 PM
Long-term archiving on : Saturday, April 1, 2017 - 7:46:42 AM
Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. JFLA - Journées francophones des langages applicatifs - 2013, Damien Pous and Christine Tasson, Feb 2013, Aussois, France. ⟨hal-00778832⟩
