---
res:
  bibo_abstract:
  - Synchronous programs are easy to specify because the side effects of an operation
    are finished by the time the invocation of the operation returns to the caller.
    Asynchronous programs, on the other hand, are difficult to specify because there
    are side effects due to pending computation scheduled as a result of the invocation
    of an operation. They are also difficult to verify because of the large number
    of possible interleavings of concurrent asynchronous computation threads. We show
    that specifications and correctness proofs for asynchronous programs can be structured
    by introducing the fiction, for proof purposes, that intermediate, non-quiescent
    states of asynchronous operations can be ignored. Then, the task of specification
    becomes relatively simple and the task of verification can be naturally decomposed
    into smaller sub-tasks. The sub-tasks iteratively summarize, guided by the structure
    of an asynchronous program, the atomic effect of non-atomic operations and the
    synchronous effect of asynchronous operations. This structuring of specifications
    and proofs corresponds to the introduction of multiple layers of stepwise refinement
    for asynchronous programs. We present the first proof rule, called synchronization,
    to reduce asynchronous invocations on a lower layer to synchronous invocations
    on a higher layer. We implemented our proof method in CIVL and evaluated it on
    a collection of benchmark programs.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - 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.15479/AT:IST-2018-853-v2-2
  dct_date: 2017^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2664-1690
  dct_language: eng
  dct_publisher: IST Austria@
  dct_title: Synchronizing the asynchronous@
...