---
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 computation threads. We present synchronization,
    a new proof rule that simplifies the verification of asynchronous programs by
    introducing the fiction, for proof purposes, that asynchronous operations complete
    synchronously. Synchronization summarizes an asynchronous computation as immediate
    atomic effect. Modular verification is enabled via pending asynchronous calls
    in atomic summaries, and a complementary proof rule that eliminates pending asynchronous
    calls when components and their specifications are composed. We evaluate synchronization
    in the context of a multi-layer refinement verification methodology on a collection
    of benchmark 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
  - 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
  bibo_doi: 10.4230/LIPIcs.CONCUR.2018.21
  bibo_volume: 118
  dct_date: 2018^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/1868-8969
  dct_language: eng
  dct_publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik@
  dct_title: Synchronizing the asynchronous@
...