Automated Modular Verification for Relaxed Communication Protocols

Andreea Costea, Wei-ngan Chin, Shengchao Qin, Florin Craciun

Research output: Chapter in Book/Report/Conference proceedingConference contribution

178 Downloads (Pure)

Abstract

Ensuring software correctness and safety for communication-centric programs is important but challenging. In this paper we introduce a solution for writing communication protocols, for checking protocol conformance and for verifying implementation safety. This work draws on ideas from both multiparty session types, which provide a concise way to express communication protocols, as well as from separation-style logics for shared-memory concurrency, which provide strong safety guarantees for resource sharing. On the one hand, our proposal improves the expressiveness and precision of session types, without sacrificing their conciseness. On the other hand, it increases the applicability of software verification as well as its precision, by making it protocol aware. We also show how to perform the verification of such programs in a modular and automatic fashion.
Original languageEnglish
Title of host publicationAsian Symposium on Programming Languages and Systems
PublisherSpringer Verlag
Pages284-305
DOIs
Publication statusPublished - 22 Oct 2018

Publication series

NameProgramming Languages and Systems
Volume11275
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Automated Modular Verification for Relaxed Communication Protocols'. Together they form a unique fingerprint.

Cite this