---
_id: '160'
abstract:
- lang: eng
  text: 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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
citation:
  ama: '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>'
  apa: '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>'
  chicago: 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>.
  ieee: 'B. Kragl and S. Qadeer, “Layered Concurrent Programs,” presented at the CAV:
    Computer Aided Verification, Oxford, UK, 2018, vol. 10981, pp. 79–102.'
  ista: 'Kragl B, Qadeer S. 2018. Layered Concurrent Programs. CAV: Computer Aided
    Verification, LNCS, vol. 10981, 79–102.'
  mla: 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>.
  short: B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102.
conference:
  end_date: 2018-07-17
  location: Oxford, UK
  name: 'CAV: Computer Aided Verification'
  start_date: 2018-07-14
date_created: 2018-12-11T11:44:57Z
date_published: 2018-07-18T00:00:00Z
date_updated: 2026-04-08T07:23:52Z
day: '18'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-319-96145-3_5
external_id:
  isi:
  - '000491481600005'
file:
- access_level: open_access
  checksum: c64fff560fe5a7532ec10626ad1c215e
  content_type: application/pdf
  creator: dernst
  date_created: 2018-12-17T12:52:12Z
  date_updated: 2020-07-14T12:45:04Z
  file_id: '5705'
  file_name: 2018_LNCS_Kragl.pdf
  file_size: 1603844
  relation: main_file
file_date_updated: 2020-07-14T12:45:04Z
has_accepted_license: '1'
intvolume: '     10981'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 79 - 102
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '7761'
quality_controlled: '1'
related_material:
  record:
  - id: '8332'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Layered Concurrent Programs
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10981
year: '2018'
...