Vérification de systèmes paramétrés avec Cubicle

Sylvain Conchon 1, 2 Alain Mebsout 1, 2 Fatiha Zaïdi 1
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs - 2013, Feb 2013, Aussois, France. 2013
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00778832
Contributeur : Ist Inria Saclay <>
Soumis le : lundi 21 janvier 2013 - 14:56:42
Dernière modification le : jeudi 9 février 2017 - 15:55:10
Document(s) archivé(s) le : samedi 1 avril 2017 - 07:46:42

Fichier

jfla2013-02.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : hal-00778832, version 1

Citation

Sylvain Conchon, Alain Mebsout, Fatiha Zaïdi. Vérification de systèmes paramétrés avec Cubicle. Damien Pous and Christine Tasson. JFLA - Journées francophones des langages applicatifs - 2013, Feb 2013, Aussois, France. 2013. 〈hal-00778832〉

Partager

Métriques

Consultations de
la notice

371

Téléchargements du document

195