{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:56:18Z","timestamp":1760043378068,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,23]],"date-time":"2020-07-23T00:00:00Z","timestamp":1595462400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,7,23]]},"DOI":"10.1145\/3427761.3428345","type":"proceedings-article","created":{"date-parts":[[2020,11,25]],"date-time":"2020-11-25T02:48:04Z","timestamp":1606272484000},"page":"26-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A separation logic to verify termination of busy-waiting for abrupt program exit"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1048-8735","authenticated-orcid":false,"given":"Tobias","family":"Reinhard","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3605-249X","authenticated-orcid":false,"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,16]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Tada live: Compositional reasoning for termination of ifne-grained concurrent programs. CoRR, abs\/","author":"D'Osualdo Emanuele","year":"1901","unstructured":"Emanuele D'Osualdo , Azadeh Farzan , Philippa Gardner , and Julian Sutherland . Tada live: Compositional reasoning for termination of ifne-grained concurrent programs. CoRR, abs\/ 1901 .05750, 2019. URL htp:\/\/arxiv.org\/abs\/ 1901.05750. Emanuele D'Osualdo, Azadeh Farzan, Philippa Gardner, and Julian Sutherland. Tada live: Compositional reasoning for termination of ifne-grained concurrent programs. CoRR, abs\/ 1901.05750, 2019. URL htp:\/\/arxiv.org\/abs\/ 1901.05750."},{"key":"e_1_3_2_1_2_1","first-page":"152","volume":"48","author":"Filli\u00e2tre Jean-Christophe","unstructured":"Jean-Christophe Filli\u00e2tre , L\u00e9on Gondelman , and Andrei Paskevich . The spirit of ghost code. Formal Methods in System Design , 48 : 152 - 174 , 2016. doi: 10.1007\/s10703-016-0243-x. 10.1007\/s10703-016-0243-x Jean-Christophe Filli\u00e2tre, L\u00e9on Gondelman, and Andrei Paskevich. The spirit of ghost code. Formal Methods in System Design, 48 : 152-174, 2016. doi: 10.1007\/s10703-016-0243-x.","journal-title":"System Design"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_15"},{"key":"e_1_3_2_1_4_1","volume-title":"ECOOP","author":"Hamin Jafar","year":"2019","unstructured":"Jafar Hamin and Bart Jacobs . Transferring obligations through synchronizations . In ECOOP , 2019 . Jafar Hamin and Bart Jacobs. Transferring obligations through synchronizations. In ECOOP, 2019."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_1_6_1","first-page":"41","volume-title":"Verifast: A powerful, sound, predictable, fast verifier for c and java","author":"Jacobs Bart","year":"2011","unstructured":"Bart Jacobs , Jan Smans , Pieter Philippaerts , Fr\u00e9d\u00e9ric Vogels , Willem Penninckx , and Frank Piessens . Verifast: A powerful, sound, predictable, fast verifier for c and java . In M. Bobaru, K. Havelund, G.J. Holzmann, and R. Joshi, editors, NASA Formal Methods (NFM 2011 ), volume 6617 , pages 41 - 55 . Springer , 2011. ISBN 978-3-642-20397-8. doi: 10.1007\/978-3-642-20398-5_4. URL htps:\/\/lirias.kuleuven.be\/95720. 10.1007\/978-3-642-20398-5_4 Bart Jacobs, Jan Smans, Pieter Philippaerts, Fr\u00e9d\u00e9ric Vogels, Willem Penninckx, and Frank Piessens. Verifast: A powerful, sound, predictable, fast verifier for c and java. In M. Bobaru, K. Havelund, G.J. Holzmann, and R. Joshi, editors, NASA Formal Methods (NFM 2011 ), volume 6617, pages 41-55. Springer, 2011. ISBN 978-3-642-20397-8. doi: 10.1007\/978-3-642-20398-5_4. URL htps:\/\/lirias.kuleuven.be\/95720."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3210258"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_1_9_1","volume":"28","author":"Jung Ralf","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ales Bizjak , Lars Birkedal , and Derek Dreyer . Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. , 28 : e20, 2018. doi: 10.1017\/S0956796818000151. 10.1017\/S0956796818000151 Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28 : e20, 2018. doi: 10.1017\/S0956796818000151.","journal-title":"J. Funct. Program."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158108"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1049\/ip-e.1980.0017"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICIEV.2012.6317471"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3427761.3428345"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"}],"event":{"name":"SPLASH '20: Conference on Systems, Programming, Languages, and Applications, Software for Humanity","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual USA","acronym":"SPLASH '20"},"container-title":["Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427761.3428345","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3427761.3428345","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:40Z","timestamp":1750195480000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3427761.3428345"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,23]]},"references-count":20,"alternative-id":["10.1145\/3427761.3428345","10.1145\/3427761"],"URL":"https:\/\/doi.org\/10.1145\/3427761.3428345","relation":{},"subject":[],"published":{"date-parts":[[2020,7,23]]},"assertion":[{"value":"2020-11-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}