Layered Concurrent Programs

B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102.

OA 2018_LNCS_Kragl.pdf 1.60 MB

Conference Paper | Published | English

Scopus indexed
Series Title
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.
Publishing Year
Date Published
79 - 102
CAV: Computer Aided Verification
Conference Location
Oxford, UK
Conference Date
2018-07-14 – 2018-07-17

Cite this

Kragl B, Qadeer S. Layered Concurrent Programs. In: Vol 10981. Springer; 2018:79-102. doi:10.1007/978-3-319-96145-3_5
Kragl, B., & Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981, pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer.
Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102. Springer, 2018.
B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV: Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102.
Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided Verification, LNCS, vol. 10981. 79–102.
Kragl, Bernhard, and Shaz Qadeer. Layered Concurrent Programs. Vol. 10981, Springer, 2018, pp. 79–102, doi:10.1007/978-3-319-96145-3_5.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
MD5 Checksum

Material in IST:
Dissertation containing IST record


Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar