---
_id: '8195'
abstract:
- lang: eng
  text: This paper presents a foundation for refining concurrent programs with structured
    control flow. The verification problem is decomposed into subproblems that aid
    interactive program development, proof reuse, and automation. The formalization
    in this paper is the basis of a new design and implementation of the Civl verifier.
acknowledgement: "Bernhard Kragl and Thomas A. Henzinger were supported by\r\nthe
  Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award)."
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
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
citation:
  ama: 'Kragl B, Qadeer S, Henzinger TA. Refinement for structured concurrent programs.
    In: <i>Computer Aided Verification</i>. Vol 12224. Springer Nature; 2020:275-298.
    doi:<a href="https://doi.org/10.1007/978-3-030-53288-8_14">10.1007/978-3-030-53288-8_14</a>'
  apa: Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2020). Refinement for structured
    concurrent programs. In <i>Computer Aided Verification</i> (Vol. 12224, pp. 275–298).
    Springer Nature. <a href="https://doi.org/10.1007/978-3-030-53288-8_14">https://doi.org/10.1007/978-3-030-53288-8_14</a>
  chicago: Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured
    Concurrent Programs.” In <i>Computer Aided Verification</i>, 12224:275–98. Springer
    Nature, 2020. <a href="https://doi.org/10.1007/978-3-030-53288-8_14">https://doi.org/10.1007/978-3-030-53288-8_14</a>.
  ieee: B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent
    programs,” in <i>Computer Aided Verification</i>, 2020, vol. 12224, pp. 275–298.
  ista: Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent
    programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298.
  mla: Kragl, Bernhard, et al. “Refinement for Structured Concurrent Programs.” <i>Computer
    Aided Verification</i>, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:<a
    href="https://doi.org/10.1007/978-3-030-53288-8_14">10.1007/978-3-030-53288-8_14</a>.
  short: B. Kragl, S. Qadeer, T.A. Henzinger, in:, Computer Aided Verification, Springer
    Nature, 2020, pp. 275–298.
corr_author: '1'
date_created: 2020-08-03T11:45:35Z
date_published: 2020-07-14T00:00:00Z
date_updated: 2026-04-08T07:23:52Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-53288-8_14
external_id:
  isi:
  - '000695276000014'
file:
- access_level: open_access
  content_type: application/pdf
  creator: dernst
  date_created: 2020-08-06T08:14:54Z
  date_updated: 2020-08-06T08:14:54Z
  file_id: '8201'
  file_name: 2020_LNCS_Kragl.pdf
  file_size: 804237
  relation: main_file
  success: 1
file_date_updated: 2020-08-06T08:14:54Z
has_accepted_license: '1'
intvolume: '     12224'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '07'
oa: 1
oa_version: Published Version
page: 275-298
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
publication: Computer Aided Verification
publication_identifier:
  eisbn:
  - '9783030532888'
  eissn:
  - 1611-3349
  isbn:
  - '9783030532871'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '8332'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Refinement for structured 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: 12224
year: '2020'
...