Automated Modular Verification for Relaxed Communication Protocols

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

doi:10.1007/978-3-030-02768-1_16

Automated Modular Verification for Relaxed Communication Protocols

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

SCEDT School Executive Team

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

315 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 language	English
Title of host publication	Asian Symposium on Programming Languages and Systems
Publisher	Springer Verlag
Pages	284-305
DOIs	https://doi.org/10.1007/978-3-030-02768-1_16
Publication status	Published - 22 Oct 2018

Publication series

Name	Programming Languages and Systems
Volume	11275
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-030-02768-1_16

Accepted manuscriptAccepted author manuscript, 571 KBLicence: CC BY-NC-ND

http://link.springer.com/10.1007/978-3-030-02768-1_16

Cite this

@inproceedings{a2413394d21f451c918959f355819b1b,

title = "Automated Modular Verification for Relaxed Communication Protocols",

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.",

author = "Andreea Costea and Wei-ngan Chin and Shengchao Qin and Florin Craciun",

year = "2018",

month = oct,

day = "22",

doi = "10.1007/978-3-030-02768-1_16",

language = "English",

series = "Programming Languages and Systems",

publisher = "Springer Verlag",

pages = "284--305",

booktitle = "Asian Symposium on Programming Languages and Systems",

address = "Germany",

}

TY - GEN

T1 - Automated Modular Verification for Relaxed Communication Protocols

AU - Costea, Andreea

AU - Chin, Wei-ngan

AU - Qin, Shengchao

AU - Craciun, Florin

PY - 2018/10/22

Y1 - 2018/10/22

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-030-02768-1_16

DO - 10.1007/978-3-030-02768-1_16

M3 - Conference contribution

T3 - Programming Languages and Systems

SP - 284

EP - 305

BT - Asian Symposium on Programming Languages and Systems

PB - Springer Verlag

ER -

Automated Modular Verification for Relaxed Communication Protocols

Abstract

Publication series

Access to Document

Fingerprint

Cite this