{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:32Z","timestamp":1750220672695,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":26,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,1,17]],"date-time":"2021-01-17T00:00:00Z","timestamp":1610841600000},"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":[[2021,1,18]]},"DOI":"10.1145\/3441296.3441396","type":"proceedings-article","created":{"date-parts":[[2020,12,23]],"date-time":"2020-12-23T00:32:44Z","timestamp":1608683564000},"page":"44-57","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Counterexample generation for program verification based on ownership refinement types"],"prefix":"10.1145","author":[{"given":"Hideto","family":"Ueno","sequence":"first","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Toman","sequence":"additional","affiliation":[{"name":"Certora, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0537-0604","authenticated-orcid":false,"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[{"name":"University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"Chiba University, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,1,17]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Conference Record of POPL 2003 : The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans","author":"Ball Thomas","year":"2003","unstructured":"Thomas Ball , Mayur Naik , and Sriram K. Rajamani . 2003. From symptom to cause: localizing errors in counterexample traces . In Conference Record of POPL 2003 : The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans , Louisisana, USA , January 15-17, 2003 , Alex Aiken and Greg Morrisett (Eds.). ACM, 97-105. htps:\/\/doi.org\/10.1145\/640128.604140 Thomas Ball, Mayur Naik, and Sriram K. Rajamani. 2003. From symptom to cause: localizing errors in counterexample traces. In Conference Record of POPL 2003 : The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003, Alex Aiken and Greg Morrisett (Eds.). ACM, 97-105. htps:\/\/doi.org\/10.1145\/640128.604140"},{"volume-title":"Fields of Logic and Computation II (LNCS","author":"Bj\u00f8rner Nikolaj","key":"e_1_3_2_1_2_1","unstructured":"Nikolaj Bj\u00f8rner , Arie Gurfinkel , Kenneth L. McMillan , and Andrey Rybalchenko . 2015. Horn Clause Solvers for Program Verification . In Fields of Logic and Computation II (LNCS , Vol. 9300 ). Springer , 24-51. htps:\/\/doi.org\/10.1007\/978-3-319-23534-9_2 Nikolaj Bj\u00f8rner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II (LNCS, Vol. 9300 ). Springer, 24-51. htps:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"volume-title":"Proc","author":"Foster Jefrey S.","key":"e_1_3_2_1_4_1","unstructured":"Jefrey S. Foster , Tachio Terauchi , and Alex Aiken . 2002. Flow-Sensitive Type Qualifiers . In Proc . of PLDI. ACM Press , 1-12. Jefrey S. Foster, Tachio Terauchi, and Alex Aiken. 2002. Flow-Sensitive Type Qualifiers. In Proc. of PLDI. ACM Press, 1-12."},{"key":"e_1_3_2_1_5_1","first-page":"77","volume-title":"IEEE Computer Security Foundations Workshop (CSFW-15)","author":"Andrew","unstructured":"Andrew D. Gordon and Alan Jefrey. 2002. Types and Efects for Asymmetric Cryptographic Protocols .. In IEEE Computer Security Foundations Workshop (CSFW-15) . 77 - 91 . Andrew D. Gordon and Alan Jefrey. 2002. Types and Efects for Asymmetric Cryptographic Protocols.. In IEEE Computer Security Foundations Workshop (CSFW-15). 77-91."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"e_1_3_2_1_7_1","first-page":"343","volume-title":"The SeaHornVerification Framework. In CAV 2015, Proceedings, Part I (LNCS","volume":"9206","author":"Gurfinkel Arie","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge A. Navas . 2015 . The SeaHornVerification Framework. In CAV 2015, Proceedings, Part I (LNCS , Vol. 9206 ). Springer , 343 - 361 . htps:\/\/doi.org\/ 10.1007\/978-3-319-21690-4_20 Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHornVerification Framework. In CAV 2015, Proceedings, Part I (LNCS, Vol. 9206 ). Springer, 343-361. htps:\/\/doi.org\/ 10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.01.004"},{"key":"e_1_3_2_1_9_1","first-page":"1","volume-title":"The ELDARICA Horn Solver. In FMCAD 2018","author":"Hojjat Hossein","year":"2018","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer . 2018 . The ELDARICA Horn Solver. In FMCAD 2018 , Nikolaj Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE , 1 - 7 . htps:\/\/doi.org\/10.23919\/FMCAD. 2018.8603013 Hossein Hojjat and Philipp R\u00fcmmer. 2018. The ELDARICA Horn Solver. In FMCAD 2018, Nikolaj Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE, 1-7. htps:\/\/doi.org\/10.23919\/FMCAD. 2018.8603013"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1145\/503272.503303","article-title":"Resource Usage Analysis","author":"Igarashi Atsushi","year":"2002","unstructured":"Atsushi Igarashi and Naoki Kobayashi . 2002 . Resource Usage Analysis . In Proceedings of POPL. 331 - 342 . Atsushi Igarashi and Naoki Kobayashi. 2002. Resource Usage Analysis. In Proceedings of POPL. 331-342.","journal-title":"Proceedings of POPL."},{"key":"e_1_3_2_1_11_1","volume-title":"Walz","author":"Johnson Gregory F.","year":"1986","unstructured":"Gregory F. Johnson and Janet A . Walz . 1986 . A Maximum-Flow Approach to Anomaly Isolation in Unification-Based Incremental Type Inference. In POPL 1986. ACM Press , 44-57. htps:\/\/doi.org\/10.1145\/ 512644.512649 Gregory F. Johnson and Janet A. Walz. 1986. A Maximum-Flow Approach to Anomaly Isolation in Unification-Based Incremental Type Inference. In POPL 1986. ACM Press, 44-57. htps:\/\/doi.org\/10.1145\/ 512644.512649"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40007-3_26"},{"key":"e_1_3_2_1_14_1","volume-title":"Clarke","author":"Komuravelli Anvesh","year":"2013","unstructured":"Anvesh Komuravelli , Arie Gurfinkel , Sagar Chaki , and Edmund M . Clarke . 2013 . Automatic abstraction in SMT-based unbounded software model checking. In International Conference on Computer Aided Verification. Springer , 846-862. Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, and Edmund M. Clarke. 2013. Automatic abstraction in SMT-based unbounded software model checking. In International Conference on Computer Aided Verification. Springer, 846-862."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349230"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983994"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_20_1","first-page":"128","volume-title":"Fractional Ownerships for Safe Memory Deallocation. In APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings (Lecture Notes in Computer Science","volume":"5904","author":"Suenaga Kohei","year":"2009","unstructured":"Kohei Suenaga and Naoki Kobayashi . 2009 . Fractional Ownerships for Safe Memory Deallocation. In APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings (Lecture Notes in Computer Science , Vol. 5904 ), Zhenjiang Hu (Ed.). Springer , 128 - 143 . htps:\/\/doi.org\/10.1007\/978-3-642-10672-9_11 Kohei Suenaga and Naoki Kobayashi. 2009. Fractional Ownerships for Safe Memory Deallocation. In APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings (Lecture Notes in Computer Science, Vol. 5904 ), Zhenjiang Hu (Ed.). Springer, 128-143. htps:\/\/doi.org\/10.1007\/978-3-642-10672-9_11"},{"key":"e_1_3_2_1_21_1","first-page":"1","article-title":"Checking race freedom via linear programming","author":"Terauchi Tachio","year":"2008","unstructured":"Tachio Terauchi . 2008 . Checking race freedom via linear programming . In Proc. of PLDI. 1 - 10 . Tachio Terauchi. 2008. Checking race freedom via linear programming. In Proc. of PLDI. 1-10.","journal-title":"Proc. of PLDI."},{"key":"e_1_3_2_1_22_1","first-page":"119","article-title":"Dependent types from counterexamples","author":"Terauchi Tachio","year":"2010","unstructured":"Tachio Terauchi . 2010 . Dependent types from counterexamples . In Proceedings of POPL. ACM , 119 - 130 . Tachio Terauchi. 2010. Dependent types from counterexamples. In Proceedings of POPL. ACM, 119-130.","journal-title":"Proceedings of POPL. ACM"},{"key":"e_1_3_2_1_23_1","first-page":"684","volume-title":"ConSORT: Context-and Flow-Sensitive Ownership Refinement Types for Imperative Programs. In ESOP 2020, Proceedings (LNCS","volume":"12075","author":"Toman John","year":"2020","unstructured":"John Toman , Ren Siqi , Kohei Suenaga , Atsushi Igarashi , and Naoki Kobayashi . 2020 . ConSORT: Context-and Flow-Sensitive Ownership Refinement Types for Imperative Programs. In ESOP 2020, Proceedings (LNCS , Vol. 12075 ). Springer , 684 - 714 . htps:\/\/doi.org\/10.1007\/978-3-030-44914-8_25 John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi, and Naoki Kobayashi. 2020. ConSORT: Context-and Flow-Sensitive Ownership Refinement Types for Imperative Programs. In ESOP 2020, Proceedings (LNCS, Vol. 12075 ). Springer, 684-714. htps:\/\/doi.org\/10.1007\/978-3-030-44914-8_25"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512648"},{"key":"e_1_3_2_1_26_1","article-title":"Program Slicing","volume":"10","author":"Weiser Mark","year":"1984","unstructured":"Mark Weiser . 1984 . Program Slicing . IEEE Trans. Software Eng. 10 , 4 ( 1984 ), 352-357. htps:\/\/doi.org\/10.1109\/TSE. 1984.5010248 Mark Weiser. 1984. Program Slicing. IEEE Trans. Software Eng. 10, 4 ( 1984 ), 352-357. htps:\/\/doi.org\/10.1109\/TSE. 1984.5010248","journal-title":"IEEE Trans. Software Eng."},{"key":"e_1_3_2_1_27_1","first-page":"569","volume-title":"POPL","author":"Zhang Danfeng","year":"2014","unstructured":"Danfeng Zhang and Andrew C. Myers . 2014. Toward general diagnosis of static errors . In POPL 2014 , Suresh Jagannathan and Peter Sewell (Eds.). ACM , 569 - 582 . htps:\/\/doi.org\/10.1145\/2535838.2535870 Danfeng Zhang and Andrew C. Myers. 2014. Toward general diagnosis of static errors. In POPL 2014, Suresh Jagannathan and Peter Sewell (Eds.). ACM, 569-582. htps:\/\/doi.org\/10.1145\/2535838.2535870"}],"event":{"name":"POPL '21: The 48th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Denmark","acronym":"POPL '21"},"container-title":["Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3441296.3441396","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3441296.3441396","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:04Z","timestamp":1750197784000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3441296.3441396"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,17]]},"references-count":26,"alternative-id":["10.1145\/3441296.3441396","10.1145\/3441296"],"URL":"https:\/\/doi.org\/10.1145\/3441296.3441396","relation":{},"subject":[],"published":{"date-parts":[[2021,1,17]]},"assertion":[{"value":"2021-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}