{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:53:39Z","timestamp":1790927619114,"version":"4.1.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["NSF CCF 1901069, NSF CCF 1527395"],"award-info":[{"award-number":["NSF CCF 1901069, NSF CCF 1527395"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","award":["PhD Fellowship"],"award-info":[{"award-number":["PhD Fellowship"]}],"id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>\n            We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety\u2014 determining if a heap-manipulating program that allocates and frees memory locations and manipulates heap pointers does not dereference an unallocated memory location. We show that this problem is decidable when the initial allocated heap forms a forest data-structure and when programs are\n            <jats:italic>streaming-coherent<\/jats:italic>\n            , which intuitively restricts programs to make a single pass over a data-structure. Our experimental evaluation on a set of library routines that manipulate forest data-structures shows that common single-pass algorithms on data-structures often fall in the decidable class, and that our decision procedure is efficient in verifying them.\n          <\/jats:p>","DOI":"10.1145\/3371103","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Deciding memory safety for single-pass heap-manipulating programs"],"prefix":"10.1145","volume":"4","author":[{"given":"Umang","family":"Mathur","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adithya","family":"Murali","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Krogmeier","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926454"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178446"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_12"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"e_1_2_2_5_1","unstructured":"S\u00e9bastien Bardin Alain Finkel and David Nowak. 2004. Toward symbolic verification of programs handling pointers. (2004).  S\u00e9bastien Bardin Alain Finkel and David Nowak. 2004. Toward symbolic verification of programs handling pointers. (2004)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_2_7_1","volume-title":"O\u2019Hearn","author":"Berdine Josh","year":"2006","unstructured":"Josh Berdine , Cristiano Calcagno , and Peter W . O\u2019Hearn . 2006 . Smallfoot : Modular Automatic Assertion Checking with Separation Logic. In Formal Methods for Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 115\u2013137. Josh Berdine, Cristiano Calcagno, and Peter W. O\u2019Hearn. 2006. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In Formal Methods for Components and Objects, Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 115\u2013137."},{"key":"e_1_2_2_8_1","volume-title":"Programs with Lists Are Counter Automata","author":"Bouajjani Ahmed","unstructured":"Ahmed Bouajjani , Marius Bozga , Peter Habermehl , Radu Iosif , Pierre Moro , and Tom\u00e1\u0161 Vojnar . 2006. Programs with Lists Are Counter Automata . In Computer Aided Verification, Thomas Ball and Robert B. Jones (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 517\u2013531. Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, and Tom\u00e1\u0161 Vojnar. 2006. Programs with Lists Are Counter Automata. In Computer Aided Verification, Thomas Ball and Robert B. Jones (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 517\u2013531."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_2"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763061"},{"key":"e_1_2_2_11_1","volume-title":"Bradley and Zohar Manna","author":"Aaron","year":"2007","unstructured":"Aaron R. Bradley and Zohar Manna . 2007 . The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag , Berlin, Heidelberg. Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, Berlin, Heidelberg."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781157"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2040235.2040256"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294295"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Nurit Dor Michael Rodeh and Shmuel Sagiv. 2000. Checking Cleanness in Linked Lists. In SAS.  Nurit Dor Michael Rodeh and Shmuel Sagiv. 2000. Checking Cleanness in Linked Lists. In SAS.","DOI":"10.1007\/978-3-540-45099-3_7"},{"key":"e_1_2_2_17_1","volume-title":"Assigning meanings to programs. Mathematical aspects of computer science 19, 19-32","author":"Floyd Robert W.","year":"1967","unstructured":"Robert W. Floyd . 1967. Assigning meanings to programs. Mathematical aspects of computer science 19, 19-32 ( 1967 ), 1. http:\/\/www.cs.ucdavis.edu\/~su\/teaching\/ecs240- s09\/readings\/FloydMeaning.pdf Robert W. Floyd. 1967. Assigning meanings to programs. Mathematical aspects of computer science 19, 19-32 (1967), 1. http:\/\/www.cs.ucdavis.edu\/~su\/teaching\/ecs240- s09\/readings\/FloydMeaning.pdf"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_22"},{"key":"e_1_2_2_19_1","volume-title":"The Programming Languages Enthusiast","author":"Hicks Michael","unstructured":"Michael Hicks . 2014. What is memory safety? , The Programming Languages Enthusiast . http:\/\/www.pl- enthusiast.net\/ 2014\/07\/21\/memory- safety\/ . Accessed: 2019-04-05. Michael Hicks. 2014. What is memory safety?, The Programming Languages Enthusiast. http:\/\/www.pl- enthusiast.net\/ 2014\/07\/21\/memory- safety\/ . Accessed: 2019-04-05."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_21_1","volume-title":"Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference. USENIX Association, 275\u2013288","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim , J Greg Morrisett , Dan Grossman , Michael W Hicks , James Cheney , and Yanling Wang . 2002 . Cyclone: A Safe Dialect of C . In Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference. USENIX Association, 275\u2013288 . Trevor Jim, J Greg Morrisett, Dan Grossman, Michael W Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C. In Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference. USENIX Association, 275\u2013288."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2017.112"},{"key":"e_1_2_2_23_1","volume-title":"TVLA: A System for Implementing Static Analyses","author":"Lev-Ami Tal","year":"2000","unstructured":"Tal Lev-Ami and Mooly Sagiv . 2000 . TVLA: A System for Implementing Static Analyses . In Static Analysis, Jens Palsberg (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 280\u2013301. Tal Lev-Ami and Mooly Sagiv. 2000. TVLA: A System for Implementing Static Analyses. In Static Analysis, Jens Palsberg (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 280\u2013301."},{"key":"e_1_2_2_24_1","volume-title":"A First Order Logic with Frames. CoRR abs\/1910.09089","author":"L\u00f8ding Christof","year":"2019","unstructured":"Christof L\u00f8ding , P. Madhusudan , Adithya Murali , and Lucas Pe. 2019. A First Order Logic with Frames. CoRR abs\/1910.09089 ( 2019 ). arXiv: 1910.09089 https:\/\/arxiv.org\/abs\/1901.09089 Christof L\u00f8ding, P. Madhusudan, Adithya Murali, and Lucas Pe. 2019. A First Order Logic with Frames. CoRR abs\/1910.09089 (2019). arXiv: 1910.09089 https:\/\/arxiv.org\/abs\/1901.09089"},{"key":"e_1_2_2_25_1","volume-title":"Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists","author":"Manevich Roman","unstructured":"Roman Manevich , E. Yahav , G. Ramalingam , and Mooly Sagiv . 2005. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists . In Verification, Model Checking, and Abstract Interpretation, Radhia Cousot (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg , 181\u2013198. Roman Manevich, E. Yahav, G. Ramalingam, and Mooly Sagiv. 2005. Predicate Abstraction and Canonical Abstraction for Singly-Linked Lists. In Verification, Model Checking, and Abstract Interpretation, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 181\u2013198."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290359"},{"key":"e_1_2_2_27_1","volume-title":"What\u2019s Decidable About Program Verification Modulo Axioms? CoRR abs\/1910.10889","author":"Mathur Umang","year":"2019","unstructured":"Umang Mathur , P. Madhusudan , and Mahesh Viswanathan . 2019b. What\u2019s Decidable About Program Verification Modulo Axioms? CoRR abs\/1910.10889 ( 2019 ). arXiv: 1910.10889 https:\/\/arxiv.org\/abs\/1910.10889 Umang Mathur, P. Madhusudan, and Mahesh Viswanathan. 2019b. What\u2019s Decidable About Program Verification Modulo Axioms? CoRR abs\/1910.10889 (2019). arXiv: 1910.10889 https:\/\/arxiv.org\/abs\/1910.10889"},{"key":"e_1_2_2_28_1","volume-title":"Deciding Memory Safety for Single-Pass Heap-Manipulating Programs. CoRR abs\/1910.00298","author":"Mathur Umang","year":"2019","unstructured":"Umang Mathur , Adithya Murali , Paul Krogmeier , P. Madhusudan , and Mahesh Viswanathan . 2019c. Deciding Memory Safety for Single-Pass Heap-Manipulating Programs. CoRR abs\/1910.00298 ( 2019 ). arXiv: 1910.00298 http:\/\/arxiv.org\/abs\/ 1910.00298 Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, and Mahesh Viswanathan. 2019c. Deciding Memory Safety for Single-Pass Heap-Manipulating Programs. CoRR abs\/1910.00298 (2019). arXiv: 1910.00298 http:\/\/arxiv.org\/abs\/ 1910.00298"},{"key":"e_1_2_2_29_1","unstructured":"Umang Mathur Adithya Murali Paul Krogmeier P. Madhusudan and Mahesh Viswanathan. 2019d. StreamVerif : Automata Based Verification of Uninterpreted Programs. https:\/\/github.com\/umangm\/streamverif .  Umang Mathur Adithya Murali Paul Krogmeier P. Madhusudan and Mahesh Viswanathan. 2019d. StreamVerif : Automata Based Verification of Uninterpreted Programs. https:\/\/github.com\/umangm\/streamverif ."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_2_31_1","unstructured":"Microsoft. 2019. 70 Percent of All Security Bugs Are Memory Safety Issues. https:\/\/it.slashdot.org\/story\/19\/02\/11\/2019247\/ microsoft- 70- percent- of- all- security- bugs- are- memory- safety- issues . Accessed: 2019-04-05.  Microsoft. 2019. 70 Percent of All Security Bugs Are Memory Safety Issues. https:\/\/it.slashdot.org\/story\/19\/02\/11\/2019247\/ microsoft- 70- percent- of- all- security- bugs- are- memory- safety- issues . Accessed: 2019-04-05."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.190"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993563"},{"key":"e_1_2_2_35_1","volume-title":"Separation Logic Modulo Theories","author":"Navarro P\u00e9rez Juan Antonio","unstructured":"Juan Antonio Navarro P\u00e9rez and Andrey Rybalchenko . 2013. Separation Logic Modulo Theories . In Programming Languages and Systems, Chung-chieh Shan (Ed.). Springer International Publishing , Cham , 90\u2013106. Juan Antonio Navarro P\u00e9rez and Andrey Rybalchenko. 2013. Separation Logic Modulo Theories. In Programming Languages and Systems, Chung-chieh Shan (Ed.). Springer International Publishing, Cham, 90\u2013106."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065887.1065892"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503286"},{"key":"e_1_2_2_38_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Neider Daniel","unstructured":"Daniel Neider , Pranav Garg , P. Madhusudan , Shambwaditya Saha , and Daejun Park . 2018. Invariant Synthesis for Incomplete Verification Engines . In Tools and Algorithms for the Construction and Analysis of Systems , Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing , Cham , 232\u2013250. Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha, and Daejun Park. 2018. Invariant Synthesis for Incomplete Verification Engines. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 232\u2013250."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250746"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3224423"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_54"},{"key":"e_1_2_2_43_1","volume-title":"Automating Separation Logic with Trees and Data","author":"Piskac Ruzica","unstructured":"Ruzica Piskac , Thomas Wies , and Damien Zufferey . 2014a. Automating Separation Logic with Trees and Data . In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing , Cham , 711\u2013728. Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014a. Automating Separation Logic with Trees and Data. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 711\u2013728."},{"key":"e_1_2_2_44_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.)","author":"Piskac Ruzica","unstructured":"Ruzica Piskac , Thomas Wies , and Damien Zufferey . 2014b. GRASShopper . In Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 124\u2013139. Ruzica Piskac, Thomas Wies, and Damien Zufferey. 2014b. GRASShopper. In Tools and Algorithms for the Construction and Analysis of Systems, Erika \u00c1brah\u00e1m and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 124\u2013139."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_46_1","volume-title":"Saddek Bensalem and Doron A. Peled (Eds.)","volume":"5779","author":"Rosu Grigore","year":"2009","unstructured":"Grigore Rosu , Wolfram Schulte , and Traian Florin Serbanuta . 2009 . Runtime Verification of C Memory Safety. In Runtime Verification (RV\u201909) (Lecture Notes in Computer Science) , Saddek Bensalem and Doron A. Peled (Eds.) , Vol. 5779 . 132\u2013152. Grigore Rosu, Wolfram Schulte, and Traian Florin Serbanuta. 2009. Runtime Verification of C Memory Safety. In Runtime Verification (RV\u201909) (Lecture Notes in Computer Science), Saddek Bensalem and Doron A. Peled (Eds.), Vol. 5779. 132\u2013152."},{"key":"e_1_2_2_47_1","unstructured":"Safe-C. 2019. Safe C Library. https:\/\/rurban.github.io\/safeclib\/doc\/safec- 3.4\/index.html . Accessed: 2019-04-05.  Safe-C. 2019. Safe C Library. https:\/\/rurban.github.io\/safeclib\/doc\/safec- 3.4\/index.html . Accessed: 2019-04-05."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_2_2_49_1","volume-title":"Proceedings of the 2012 USENIX Conference on Annual Technical Conference (USENIX ATC\u201912)","author":"Serebryany Konstantin","year":"2012","unstructured":"Konstantin Serebryany , Derek Bruening , Alexander Potapenko , and Dmitry Vyukov . 2012 . AddressSanitizer: A Fast Address Sanity Checker . In Proceedings of the 2012 USENIX Conference on Annual Technical Conference (USENIX ATC\u201912) . USENIX Association, Berkeley, CA, USA, 28\u201328. http:\/\/dl.acm.org\/citation.cfm?id=2342821.2342849 Konstantin Serebryany, Derek Bruening, Alexander Potapenko, and Dmitry Vyukov. 2012. AddressSanitizer: A Fast Address Sanity Checker. In Proceedings of the 2012 USENIX Conference on Annual Technical Conference (USENIX ATC\u201912). USENIX Association, Berkeley, CA, USA, 28\u201328. http:\/\/dl.acm.org\/citation.cfm?id=2342821.2342849"},{"key":"e_1_2_2_50_1","volume-title":"Memory Tagging and how it improves C\/C++ memory safety. CoRR abs\/1802.09517","author":"Serebryany Kostya","year":"2018","unstructured":"Kostya Serebryany , Evgenii Stepanov , Aleksey Shlyapnikov , Vlad Tsyrklevich , and Dmitry Vyukov . 2018. Memory Tagging and how it improves C\/C++ memory safety. CoRR abs\/1802.09517 ( 2018 ). arXiv: 1802.09517 http:\/\/arxiv.org\/abs\/1802.09517 Kostya Serebryany, Evgenii Stepanov, Aleksey Shlyapnikov, Vlad Tsyrklevich, and Dmitry Vyukov. 2018. Memory Tagging and how it improves C\/C++ memory safety. CoRR abs\/1802.09517 (2018). arXiv: 1802.09517 http:\/\/arxiv.org\/abs\/1802.09517"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.13"},{"key":"e_1_2_2_52_1","unstructured":"The Rust Team. 2019. The Rust programming language. https:\/\/www.rust- lang.org\/  The Rust Team. 2019. The Rust programming language. https:\/\/www.rust- lang.org\/"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.9"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360206"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371103","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371103","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371103","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371103"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371103"],"URL":"https:\/\/doi.org\/10.1145\/3371103","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}