Skip to Main content Skip to Navigation
Conference papers

Parameterized Verification of Topology-sensitive Distributed Protocols goes Declarative

Abstract : We show that Cubicle, an SMT-based infinite-state model checker, can be applied as a verification engine for GLog, a logic-based specification language for topology-sensitive distributed protocols with asynchronous communication. Existential coverability queries in GLog can be translated into verification judgements in Cubicle by encoding relational updates rules as unbounded array transitions. We apply the resulting framework to automatically verify a distributed version of the Dining Philosopher mutual exclusion protocol formulated for an arbitrary number of nodes and communication buffers.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Sylvain Conchon Connect in order to contact the contributor
Submitted on : Thursday, January 31, 2019 - 11:53:42 AM
Last modification on : Tuesday, January 4, 2022 - 5:00:54 AM
Long-term archiving on: : Wednesday, May 1, 2019 - 3:16:30 PM


Files produced by the author(s)


  • HAL Id : hal-02001652, version 1


Sylvain Conchon, Giorgio Delzanno, Angelo Ferrando. Parameterized Verification of Topology-sensitive Distributed Protocols goes Declarative. International Conference on Networked Systems (NETYS), May 2018, Essaouira, Morocco. ⟨hal-02001652⟩



Les métriques sont temporairement indisponibles