Automated Modular Verification for Relaxed Communication Protocols

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

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

21 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

Network protocols
Data storage equipment
Communication

Cite this

Costea, A., Chin, W., Qin, S., & Craciun, F. (2018). Automated Modular Verification for Relaxed Communication Protocols. In Asian Symposium on Programming Languages and Systems (pp. 284-305). [Chapter 16] (Programming Languages and Systems; Vol. 11275). Springer Verlag. https://doi.org/10.1007/978-3-030-02768-1_16
Costea, Andreea ; Chin, Wei-ngan ; Qin, Shengchao ; Craciun, Florin. / Automated Modular Verification for Relaxed Communication Protocols. Asian Symposium on Programming Languages and Systems. Springer Verlag, 2018. pp. 284-305 (Programming Languages and Systems).
@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 = "10",
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",

}

Costea, A, Chin, W, Qin, S & Craciun, F 2018, Automated Modular Verification for Relaxed Communication Protocols. in Asian Symposium on Programming Languages and Systems., Chapter 16, Programming Languages and Systems, vol. 11275, Springer Verlag, pp. 284-305. https://doi.org/10.1007/978-3-030-02768-1_16

Automated Modular Verification for Relaxed Communication Protocols. / Costea, Andreea; Chin, Wei-ngan; Qin, Shengchao; Craciun, Florin.

Asian Symposium on Programming Languages and Systems. Springer Verlag, 2018. p. 284-305 Chapter 16 (Programming Languages and Systems; Vol. 11275).

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

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 -

Costea A, Chin W, Qin S, Craciun F. Automated Modular Verification for Relaxed Communication Protocols. In Asian Symposium on Programming Languages and Systems. Springer Verlag. 2018. p. 284-305. Chapter 16. (Programming Languages and Systems). https://doi.org/10.1007/978-3-030-02768-1_16