{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:25Z","timestamp":1750220845054,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100007297","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2787"],"award-info":[{"award-number":["N00014-17-1-2787"]}],"id":[{"id":"10.13039\/100007297","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":[[2019,10,10]]},"abstract":"<jats:p>\n            The modern software engineering process is evolutionary, with commits\/patches begetting new versions of code, progressing steadily toward improved systems. In recent years, program analysis and verification tools have exploited version-based reasoning, where new code can be seen in terms of how it has changed from the previous version. When considering program versions, refinement seems a natural fit and, in recent decades, researchers have weakened classical notions of concrete refinement and program equivalence to capture similarities as well as differences between programs. For example, Benton, Yang and others have worked on state-based\n            <jats:italic>refinement relations<\/jats:italic>\n            .\n          <\/jats:p>\n          <jats:p>\n            In this paper, we explore a form of weak refinement based on\n            <jats:italic>trace<\/jats:italic>\n            relations rather than state relations. The idea begins by partitioning traces of a program\n            <jats:italic>C<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            into trace classes, each identified via a\n            <jats:italic>restriction<\/jats:italic>\n            <jats:italic>r<\/jats:italic>\n            <jats:sub>1<\/jats:sub>\n            . For each class, we specify similar behavior in the other program\n            <jats:italic>C<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            via a separate restriction\n            <jats:italic>r<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            on\n            <jats:italic>C<\/jats:italic>\n            <jats:sub>2<\/jats:sub>\n            . Still, these two trace classes may not yet be equivalent so we further permit a weakening via a binary relation\n            <jats:italic>A<\/jats:italic>\n            on traces, that allows one to, for instance disregard unimportant events, relate analogous atomic events, etc.\n          <\/jats:p>\n          <jats:p>\n            We address several challenges that arise. First, we explore one way to specify trace refinement relations by instantiating the framework to Kleene Algebra with Tests (KAT) due to Kozen. We use KAT intersection for restriction, KAT hypotheses for\n            <jats:italic>A<\/jats:italic>\n            , KAT inclusion for refinement, and have proved compositionality. Next, we present an algorithm for automatically synthesizing refinement relations, based on a mixture of semantic program abstraction, KAT inclusion, a custom edit-distance algorithm on counterexamples, and case-analysis on nondeterministic branching. We have proved our algorithm to be sound. Finally, we implemented our algorithm as a tool called Knotical, on top of Interproc and Symkat. We demonstrate promising first steps in synthesizing trace refinement relations across a hand-crafted collection of 37 benchmarks that include changing fragments of array programs, models of systems code, and examples inspired by the thttpd and Merecat web servers.\n          <\/jats:p>","DOI":"10.1145\/3360604","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Specification and inference of trace refinement relations"],"prefix":"10.1145","volume":"3","author":[{"given":"Timos","family":"Antonopoulos","sequence":"first","affiliation":[{"name":"Yale University, USA"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}]},{"given":"Ton Chanh","family":"Le","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"e_1_2_2_2_1","volume-title":"Retrieved","author":"Antonopoulos Timos","year":"2019","unstructured":"Timos Antonopoulos , Eric Koskinen , and Ton Chanh Le . 2019 a. Experimental Results of Knotical . Retrieved August 14, 2019 from https:\/\/knotical.github.io\/knotical\/results\/SUMMARY.html Timos Antonopoulos, Eric Koskinen, and Ton Chanh Le. 2019a. Experimental Results of Knotical. Retrieved August 14, 2019 from https:\/\/knotical.github.io\/knotical\/results\/SUMMARY.html"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3368626"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/800057.808665"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_2_2_6_1","unstructured":"Gilles Barthe Pedro R D\u2019Argenio and Tamara Rezk. 2004. Secure information flow by self-composition. In CSFW.  Gilles Barthe Pedro R D\u2019Argenio and Tamara Rezk. 2004. Secure information flow by self-composition. In CSFW."},{"key":"e_1_2_2_7_1","volume-title":"Kleene Algebra Modulo Theories. CoRR abs\/1707.02894","author":"Beckett Ryan","year":"2017","unstructured":"Ryan Beckett , Eric Campbell , and Michael Greenberg . 2017. Kleene Algebra Modulo Theories. CoRR abs\/1707.02894 ( 2017 ). arXiv: 1707.02894 http:\/\/arxiv.org\/abs\/1707.02894 Ryan Beckett, Eric Campbell, and Michael Greenberg. 2017. Kleene Algebra Modulo Theories. CoRR abs\/1707.02894 (2017). arXiv: 1707.02894 http:\/\/arxiv.org\/abs\/1707.02894"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_9_1","volume-title":"A survey on tree edit distance and related problems. Theoretical computer science 337, 1-3","author":"Bille Philip","year":"2005","unstructured":"Philip Bille . 2005. A survey on tree edit distance and related problems. Theoretical computer science 337, 1-3 ( 2005 ), 217\u2013239. Philip Bille. 2005. A survey on tree edit distance and related problems. Theoretical computer science 337, 1-3 (2005), 217\u2013239."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_3"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Michael R. Clarkson Bernd Finkbeiner Masoud Koleini Kristopher K. Micinski Markus N. Rabe and C\u00e9sar S\u00e1nchez. 2014. Temporal Logics for Hyperproperties. In POST. 265\u2013284.  Michael R. Clarkson Bernd Finkbeiner Masoud Koleini Kristopher K. Micinski Markus N. Rabe and C\u00e9sar S\u00e1nchez. 2014. Temporal Logics for Hyperproperties. In POST. 265\u2013284.","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183285"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629911.1630034"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092719"},{"key":"e_1_2_2_16_1","first-page":"243","article-title":"Semantic Diff: A Tool for Summarizing the Effects of Modifications","volume":"94","author":"Jackson Daniel","year":"1994","unstructured":"Daniel Jackson and David A Ladd . 1994 . Semantic Diff: A Tool for Summarizing the Effects of Modifications .. In ICSM , Vol. 94. 243 \u2013 252 . Daniel Jackson and David A Ladd. 1994. Semantic Diff: A Tool for Summarizing the Effects of Modifications.. In ICSM, Vol. 94. 243\u2013252.","journal-title":"ICSM"},{"key":"e_1_2_2_18_1","volume-title":"Mathematical Foundations of Computer Science","author":"Kozen Dexter","year":"1990","unstructured":"Dexter Kozen . 1990. On kleene algebras and closed semirings . In Mathematical Foundations of Computer Science 1990 , Branislav Rovan (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg, 26\u201347. Dexter Kozen. 1990. On kleene algebras and closed semirings. In Mathematical Foundations of Computer Science 1990, Branislav Rovan (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 26\u201347."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61042-1_35"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11821069_6"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_17"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_2_2_27_1","volume-title":"Retrieved","author":"Lalire Ga\u00ebl","year":"2009","unstructured":"Ga\u00ebl Lalire , Mathias Argoud , and Bertrand Jeannet . 2009 . Interproc analyzer for recursive programs with numerical variables . Retrieved August 13, 2019 from http:\/\/pop-art.inrialpes.fr\/people\/bjeannet\/bjeannet-forge\/interproc\/index.html Ga\u00ebl Lalire, Mathias Argoud, and Bertrand Jeannet. 2009. Interproc analyzer for recursive programs with numerical variables. Retrieved August 13, 2019 from http:\/\/pop-art.inrialpes.fr\/people\/bjeannet\/bjeannet-forge\/interproc\/index.html"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594326"},{"key":"e_1_2_2_29_1","volume-title":"8th International Seminar on Relational Methods in Computer Science, 3rd International Workshop on Applications of Kleene Algebra, and Workshop of COST Action 274: TARSKI, St. Catharines, ON","author":"Mathieu Vincent","year":"2005","unstructured":"Vincent Mathieu and Jules Desharnais . 2005 . Verification of Pushdown Systems Using Omega Algebra with Domain. In Relational Methods in Computer Science , 8th International Seminar on Relational Methods in Computer Science, 3rd International Workshop on Applications of Kleene Algebra, and Workshop of COST Action 274: TARSKI, St. Catharines, ON , Canada, February 22-26, 2005, Selected Revised Papers . 188\u2013199. Vincent Mathieu and Jules Desharnais. 2005. Verification of Pushdown Systems Using Omega Algebra with Domain. In Relational Methods in Computer Science, 8th International Seminar on Relational Methods in Computer Science, 3rd International Workshop on Applications of Kleene Algebra, and Workshop of COST Action 274: TARSKI, St. Catharines, ON, Canada, February 22-26, 2005, Selected Revised Papers . 188\u2013199."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"volume-title":"Programming from specifications","author":"Morgan Carroll","key":"e_1_2_2_31_1","unstructured":"Carroll Morgan . 1994. Programming from specifications . Prentice Hall ,. Carroll Morgan. 1994. Programming from specifications. Prentice Hall,."},{"key":"e_1_2_2_32_1","volume-title":"Retrieved","author":"Nilsson Joachim","year":"2019","unstructured":"Joachim Nilsson . 2019 . Merecat Embedded Web Server . Retrieved August 13, 2019 from https:\/\/troglobit.com\/projects\/merecat\/ Joachim Nilsson. 2019. Merecat Embedded Web Server. Retrieved August 13, 2019 from https:\/\/troglobit.com\/projects\/merecat\/"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209109"},{"key":"e_1_2_2_35_1","volume-title":"SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings . 238\u2013258","author":"Partush Nimrod","year":"2013","unstructured":"Nimrod Partush and Eran Yahav . 2013 . Abstract Semantic Differencing for Numerical Programs. In Static Analysis - 20th International Symposium , SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings . 238\u2013258 . Nimrod Partush and Eran Yahav. 2013. Abstract Semantic Differencing for Numerical Programs. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings . 238\u2013258."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660245"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_2_2_38_1","volume-title":"CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I . 164\u2013182","author":"Pick Lauren","year":"2018","unstructured":"Lauren Pick , Grigory Fedyukovich , and Aarti Gupta . 2018 . Exploiting Synchrony and Symmetry in Relational Verification. In Computer Aided Verification - 30th International Conference , CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I . 164\u2013182 . Lauren Pick, Grigory Fedyukovich, and Aarti Gupta. 2018. Exploiting Synchrony and Symmetry in Relational Verification. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I . 164\u2013182."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_40_1","volume-title":"Retrieved","author":"Poskanzer Jef","year":"2018","unstructured":"Jef Poskanzer . 2018 . thttpd HTTP server . Retrieved August 13, 2019 from http:\/\/www.acme.com\/software\/thttpd\/ Jef Poskanzer. 2018. thttpd HTTP server. Retrieved August 13, 2019 from http:\/\/www.acme.com\/software\/thttpd\/"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2677007"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677007"},{"key":"e_1_2_2_43_1","volume-title":"Retrieved","author":"Pous Damien","year":"2016","unstructured":"Damien Pous . 2016 . Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests . Retrieved August 13, 2019 from https:\/\/perso.ens-lyon.fr\/damien.pous\/symbolickat\/ Damien Pous. 2016. Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests. Retrieved August 13, 2019 from https:\/\/perso.ens-lyon.fr\/damien.pous\/symbolickat\/"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106279"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_2_46_1","volume-title":"Lahiri","author":"Sousa Marcelo","year":"2018","unstructured":"Marcelo Sousa , Isil Dillig , and Shuvendu K . Lahiri . 2018 . Verified three-way program merge. PACMPL 2, OOPSLA ( 2018), 165:1\u2013165:29. Marcelo Sousa, Isil Dillig, and Shuvendu K. Lahiri. 2018. Verified three-way program merge. PACMPL 2, OOPSLA (2018), 165:1\u2013165:29."},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238211"},{"key":"e_1_2_2_48_1","doi-asserted-by":"crossref","unstructured":"Tachio Terauchi and Alex Aiken. 2005. Secure information flow as a safety problem. In SAS.  Tachio Terauchi and Alex Aiken. 2005. Secure information flow as a safety problem. In SAS.","DOI":"10.1007\/11547662_24"},{"key":"e_1_2_2_49_1","volume-title":"SAS 2017, New York, NY, USA, August 30 -September 1, 2017, Proceedings . 405\u2013427","author":"Trostanetski Anna","year":"2017","unstructured":"Anna Trostanetski , Orna Grumberg , and Daniel Kroening . 2017 . Modular Demand-Driven Analysis of Semantic Difference for Program Versions. In Static Analysis - 24th International Symposium , SAS 2017, New York, NY, USA, August 30 -September 1, 2017, Proceedings . 405\u2013427 . Anna Trostanetski, Orna Grumberg, and Daniel Kroening. 2017. Modular Demand-Driven Analysis of Semantic Difference for Program Versions. In Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, August 30 -September 1, 2017, Proceedings . 405\u2013427."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_30"},{"key":"e_1_2_2_51_1","volume-title":"Cook","author":"Wang Yuepeng","year":"2018","unstructured":"Yuepeng Wang , Isil Dillig , Shuvendu K. Lahiri , and William R . Cook . 2018 . Verifying equivalence of database-driven applications. PACMPL 2, POPL ( 2018), 56:1\u201356:29. Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2018. Verifying equivalence of database-driven applications. PACMPL 2, POPL (2018), 56:1\u201356:29."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_35"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzl009"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360604","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360604","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360604","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360604"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":51,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360604"],"URL":"https:\/\/doi.org\/10.1145\/3360604","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}