Layered Concurrent Programs Conference Paper

Author(s): Kragl, Bernhard; Qadeer, Shaz
Title: Layered Concurrent Programs
Title Series: LNCS
Affiliation IST Austria
Abstract: We present layered concurrent programs, a compact and expressive notation for specifying refinement proofs of concurrent programs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. These programs are expressed in the ordinary syntax of imperative concurrent programs using gated atomic actions, sequencing, choice, and (recursive) procedure calls. Each concurrent program is automatically extracted from the layered program. We reduce refinement to the safety of a sequence of concurrent checker programs, one each to justify the connection between every two consecutive concurrent programs. These checker programs are also automatically extracted from the layered program. Layered concurrent programs have been implemented in the CIVL verifier which has been successfully used for the verification of several complex concurrent programs.
Conference Title: CAV: Computer Aided Verification
Volume: 10981
Conference Dates: July 14-17, 2018
Conference Location: Oxford, UK
ISBN: 978-3-319-96144-6
Publisher: Springer  
Location: Cham
Date Published: 2018-07-18
Start Page: 79
End Page: 102
Copyright Statement: This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License(, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Sponsor: This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
DOI: 10.1007/978-3-319-96145-3_5
Open access: yes (repository)
IST Austria Authors
  1. Bernhard Kragl
    5 Kragl
Related IST Austria Work