Cubicle-W: Parameterized Model Checking on Weak Memory - Laboratoire de Recherche en Informatique. Équipe: Vérification d'Algorithmes, Langages et Systèmes Accéder directement au contenu
Communication Dans Un Congrès Année : 2018

Cubicle-W: Parameterized Model Checking on Weak Memory

Résumé

We present Cubicle-W, a new version of the Cubicle model checker to verify parameterized systems under weak memory models. Its main originality is to implement a backward reachability algorithm modulo weak memory reasoning using SMT. Our experiments show that Cubicle-W is expressive and efficient enough to automatically prove safety of concurrent algorithms, for an arbitrary number of processes, ranging from mutual exclusion to synchronization barriers.
Fichier principal
Vignette du fichier
paper.pdf (426.62 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02420590 , version 1 (20-12-2019)

Identifiants

  • HAL Id : hal-02420590 , version 1

Citer

Sylvain Conchon, David Declerck, Fatiha Zaïdi. Cubicle-W: Parameterized Model Checking on Weak Memory. IJCAR 2018 - International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. pp.152-160. ⟨hal-02420590⟩
109 Consultations
51 Téléchargements

Partager

Gmail Facebook X LinkedIn More