conference paper published yes Bernhard Kragl author 320FC952-F248-11E8-B48F-1D18A9856A870000-0001-7745-9117 Shaz Qadeer author ToHe department CAV: Computer Aided Verification Formal methods for the design and analysis of complex systems project Rigorous Systems Engineering project 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. https://research-explorer.ista.ac.at/download/160/5705/2018_LNCS_Kragl.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Springer2018Oxford, UK eng 00049148160000510.1007/978-3-319-96145-3_5 1098179 - 102 https://research-explorer.ista.ac.at/record/8332 Kragl, B., &#38; Qadeer, S. (2018). Layered Concurrent Programs (Vol. 10981, pp. 79–102). Presented at the CAV: Computer Aided Verification, Oxford, UK: Springer. <a href="https://doi.org/10.1007/978-3-319-96145-3_5">https://doi.org/10.1007/978-3-319-96145-3_5</a> Kragl, Bernhard, and Shaz Qadeer. <i>Layered Concurrent Programs</i>. Vol. 10981, Springer, 2018, pp. 79–102, doi:<a href="https://doi.org/10.1007/978-3-319-96145-3_5">10.1007/978-3-319-96145-3_5</a>. Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided Verification, LNCS, vol. 10981, 79–102. B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102. Kragl, Bernhard, and Shaz Qadeer. “Layered Concurrent Programs,” 10981:79–102. Springer, 2018. <a href="https://doi.org/10.1007/978-3-319-96145-3_5">https://doi.org/10.1007/978-3-319-96145-3_5</a>. Kragl B, Qadeer S. Layered Concurrent Programs. In: Vol 10981. Springer; 2018:79-102. doi:<a href="https://doi.org/10.1007/978-3-319-96145-3_5">10.1007/978-3-319-96145-3_5</a> B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV: Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102. 1602018-12-11T11:44:57Z2026-04-08T07:23:52Z