FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Declarative Parameterized Verification of Topology-sensitive Distributed Protocols

Authors: Giorgio Delzanno, Sylvain Conchon and Angelo Ferrando

Paper Information

Title:Declarative Parameterized Verification of Topology-sensitive Distributed Protocols
Authors:Giorgio Delzanno, Sylvain Conchon and Angelo Ferrando
Proceedings:HCVS Papers
Editors: German Vidal and Temesghen Kahsai
Keywords:Parameterized verification, Distributed Protocols, SMT solvers
Abstract:

ABSTRACT. We show that Cubicle,anSMT-basedinfinite-statemodel 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 arbi- trary number of nodes and communication buffers.

Pages:15
Talk:Jul 13 15:00 (Session 87E)
Paper: