{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:55Z","timestamp":1772164075931,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,19]],"date-time":"2017-10-19T00:00:00Z","timestamp":1508371200000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF- 1218605, CCF-1318191, CCF-1421575"],"award-info":[{"award-number":["CCF- 1218605, CCF-1318191, CCF-1421575"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-C-0284"],"award-info":[{"award-number":["FA8750-12-C-0284"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,10,19]]},"DOI":"10.1145\/2983990.2984027","type":"proceedings-article","created":{"date-parts":[[2016,10,20]],"date-time":"2016-10-20T11:58:54Z","timestamp":1476964734000},"page":"74-91","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":48,"title":["Semantics-based program verifiers for all languages"],"prefix":"10.1145","author":[{"given":"Andrei","family":"Stef\u0103nescu","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Daejun","family":"Park","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Shijiao","family":"Yuwen","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]},{"given":"Yilong","family":"Li","sequence":"additional","affiliation":[{"name":"Runtime Verification, USA"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}]}],"member":"320","published-online":{"date-parts":[[2016,10,19]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"VCC: A verifier for concurrent C. http:\/\/vcc. codeplex.com. Accessed: October 5 2016."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347484"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987212"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1808999"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90185-I"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541977"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_1_12_1","series-title":"LNCS","first-page":"440","volume-title":"RTA","author":"Stef\u0103nescu A.","year":"2014","unstructured":"A. \u00b8 Stef\u0103nescu, S. Ciob\u00e2c\u0103, R. Mereu\u00b8t\u0103, B. M. Moore, T. F. \u00b8 Serb\u0103nu\u00b8t\u0103, and G. Ro\u00b8su. All-path reachability logic. In RTA, volume 8560 of LNCS, pages 425\u2013440, July 2014."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2790449.2790529"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_16_1","first-page":"52","volume-title":"FMCAD","author":"de Moura L. M.","unstructured":"L. M. de Moura and N. Bj\u00f8rner. Generalized, e fficient array decision procedures. In FMCAD, pages 45\u201352. IEEE, 2009."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1795772"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770379"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_22_1","volume-title":"The RAISE Development Method","author":"George C.","year":"1995","unstructured":"C. George, A. E. Haxthausen, S. Hughes, R. Milne, S. Prehn, and J. S. Pedersen. The RAISE Development Method. Prentice Hall, 1995."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-6259-0_10"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2003.07.005"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986314"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111048"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"e_1_3_2_1_32_1","first-page":"184","volume":"3223","author":"Liu H.","year":"2004","unstructured":"H. Liu and J. S. Moore. Java program verification via a JVM deep embedding in ACL2. In TPHOLs, volume 3223 of LNCS, pages 184\u2013200, 2004.","journal-title":"In TPHOLs"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103673"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378851"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763074"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050009"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993563"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_3_2_1_42_1","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"21","volume-title":"RTA","author":"Ro\u00b8su G.","unstructured":"G. Ro\u00b8su. Matching logic \u2014 extended abstract. In RTA, volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5\u201321. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 2015."},{"key":"e_1_3_2_1_43_1","first-page":"367","volume-title":"LICS","author":"Ro\u00b8su G.","unstructured":"G. Ro\u00b8su, A. \u00b8 Stef\u0103nescu, S. Ciob\u00e2c\u0103, and B. M. Moore. Onepath reachability logic. In LICS, pages 358\u2013367. IEEE, 2013."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_2_1_45_1","series-title":"LNCS","first-page":"402","volume-title":"FM","author":"Ros G.","year":"2012","unstructured":"G. Ros, u and A. S, tef\u0103nescu. From Hoare logic to matching logic reachability. In FM, volume 7436 of LNCS, pages 387\u2013 402, 2012."},{"key":"e_1_3_2_1_46_1","series-title":"LNCS","first-page":"363","volume-title":"ICALP","author":"Ros G.","year":"2012","unstructured":"G. Ros, u and A. S, tef\u0103nescu. Towards a unified theory of operational and axiomatic semantics. In ICALP, volume 7392 of LNCS, pages 351\u2013363, 2012."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384656"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946031.1946042"}],"event":{"name":"SPLASH '16: Conference on Systems, Programming, Languages, and Applications: Software for Humanity","location":"Amsterdam Netherlands","acronym":"SPLASH '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2983990.2984027","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2983990.2984027","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2983990.2984027","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:24:15Z","timestamp":1763457855000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2983990.2984027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,19]]},"references-count":48,"alternative-id":["10.1145\/2983990.2984027","10.1145\/2983990"],"URL":"https:\/\/doi.org\/10.1145\/2983990.2984027","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3022671.2984027","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,10,19]]},"assertion":[{"value":"2016-10-19","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}