{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:47:10Z","timestamp":1777348030653,"version":"3.51.4"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415901","type":"print"},{"value":"9783319415918","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41591-8_5","type":"book-chapter","created":{"date-parts":[[2016,6,23]],"date-time":"2016-06-23T13:27:27Z","timestamp":1466688447000},"page":"61-75","source":"Crossref","is-referenced-by-count":3,"title":["Refinement-Based Verification of Communicating Unstructured Code"],"prefix":"10.1007","author":[{"given":"Nils","family":"J\u00e4hnig","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"G\u00f6thel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sabine","family":"Glesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,23]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Bartels, B., Glesner, S.: Verification of distributed embedded real-time systems and their low-level implementation using timed CSP. In: APSEC 2011, pp. 195\u2013202. IEEE Computer Society (2011)","DOI":"10.1109\/APSEC.2011.52"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-319-06200-6_8","volume-title":"NASA Formal Methods","author":"B Bartels","year":"2014","unstructured":"Bartels, B., J\u00e4hnig, N.: Mechanized, compositional verification of low-level code. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 98\u2013112. Springer, Heidelberg (2014)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Gardner, W.B., Gumtie, A., Carter, J.D.: Supporting selective formalism in CSP++ with process-specific storage. In: ICESS 2015, pp. 1057\u20131065 (2015)","DOI":"10.1109\/HPCC-CSS-ICESS.2015.265"},{"issue":"8","key":"5_CR5","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"J\u00e4hnig, N., G\u00f6thel, T., Glesner, S.: A denotational semantics for communicating unstructured code. In: FESCA 2015. EPTCS, vol. 178, pp. 9\u201321 (2015)","DOI":"10.4204\/EPTCS.178.2"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-45949-9_1","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: The basics. In: Nipkow, T., Paulson, L.C., Wenzel, M. (eds.) Isabelle\/HOL. LNCS, vol. 2283, p. 3. Springer, Heidelberg (2002)"},{"key":"5_CR8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511626364","volume-title":"Theories of Programming Languages","author":"JC Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)"},{"key":"5_CR9","volume-title":"Concurrent and Real Time Systems: The CSP Approach","author":"S Schneider","year":"1999","unstructured":"Schneider, S.: Concurrent and Real Time Systems: The CSP Approach. Wiley, New York (1999)"},{"issue":"1","key":"5_CR10","first-page":"151","volume":"156","author":"A Saabas","year":"2005","unstructured":"Saabas, A., Uustalu, T.: A compositional natural semantics and hoare logic for low-level languages. SOS 156(1), 151\u2013168 (2005). Elsevier","journal-title":"SOS"},{"key":"5_CR11","unstructured":"Tews, H.: Verifying Duff\u2019s device: a simple compositional denotational semantics for goto and computed jumps. Technical report, Technische Universit\u00e4t Dresden (2004)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Compositionality, Concurrency, and Partial Correctness: Proof Theories for Networks of Processes, and Their Relationship","author":"J Zwiers","year":"1989","unstructured":"Zwiers, J.: Compositionality, Concurrency, and Partial Correctness. LNCS, vol. 321. Springer, Heidelberg (1989)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41591-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T12:57:25Z","timestamp":1498309045000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41591-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415901","9783319415918"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41591-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}