--- res: bibo_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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Bernhard foaf_name: Kragl, Bernhard foaf_surname: Kragl foaf_workInfoHomepage: http://www.librecat.org/personId=320FC952-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0001-7745-9117 - foaf_Person: foaf_givenName: Shaz foaf_name: Qadeer, Shaz foaf_surname: Qadeer bibo_doi: 10.1007/978-3-319-96145-3_5 bibo_volume: 10981 dct_date: 2018^xs_gYear dct_identifier: - UT:000491481600005 dct_language: eng dct_publisher: Springer@ dct_title: Layered Concurrent Programs@ ...