conference paper published yes Bernhard Kragl author 320FC952-F248-11E8-B48F-1D18A9856A870000-0001-7745-9117 Shaz Qadeer author Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 ToHe department CONCUR: International Conference on Concurrency Theory Rigorous Systems Engineering project Moderne Concurrency Paradigms project 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. https://research-explorer.ista.ac.at/download/133/5368/IST-2018-853-v2+2_concur2018.pdf application/pdfno Schloss Dagstuhl - Leibniz-Zentrum für Informatik2018Beijing, China eng 1868-896910.4230/LIPIcs.CONCUR.2018.21 118 https://research-explorer.ista.ac.at/record/6426 https://research-explorer.ista.ac.at/record/8332 yes Kragl, B., Qadeer, S., &#38; Henzinger, T. A. (2018). Synchronizing the asynchronous (Vol. 118). Presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a> B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Kragl B, Qadeer S, Henzinger TA. 2018. Synchronizing the asynchronous. CONCUR: International Conference on Concurrency Theory, LIPIcs, vol. 118, 21. Kragl, Bernhard, et al. <i>Synchronizing the Asynchronous</i>. Vol. 118, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">10.4230/LIPIcs.CONCUR.2018.21</a>. Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Synchronizing the Asynchronous,” Vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">https://doi.org/10.4230/LIPIcs.CONCUR.2018.21</a>. Kragl B, Qadeer S, Henzinger TA. Synchronizing the asynchronous. In: Vol 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2018. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2018.21">10.4230/LIPIcs.CONCUR.2018.21</a> B. Kragl, S. Qadeer, and T. A. Henzinger, “Synchronizing the asynchronous,” presented at the CONCUR: International Conference on Concurrency Theory, Beijing, China, 2018, vol. 118. 1332018-12-11T11:44:48Z2026-04-08T07:23:52Z