{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:03:01Z","timestamp":1762459381916,"version":"3.37.3"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,1]],"date-time":"2017-05-01T00:00:00Z","timestamp":1493596800000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"},{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,5,1]],"date-time":"2016-05-01T00:00:00Z","timestamp":1462060800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"European Social Fun, Romanian Government","award":["POSDRU\/159\/1.5\/S\/137750"],"award-info":[{"award-number":["POSDRU\/159\/1.5\/S\/137750"]}]},{"DOI":"10.13039\/100000003","name":"Boeing","doi-asserted-by":"publisher","award":["Formal Analysis Tools for Cyber Security\", 2014-2015"],"award-info":[{"award-number":["Formal Analysis Tools for Cyber Security\", 2014-2015"]}],"id":[{"id":"10.13039\/100000003","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NSF","award":["CCF-1218605, CCF-1318191 and CCF-1421575"],"award-info":[{"award-number":["CCF-1218605, CCF-1318191 and CCF-1421575"]}]},{"DOI":"10.13039\/100006503","name":"SPAWAR Systems Center Pacific, Space and Naval Warfare Systems Command","doi-asserted-by":"publisher","award":["FA8750-12-C-0284"],"award-info":[{"award-number":["FA8750-12-C-0284"]}],"id":[{"id":"10.13039\/100006503","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known whether the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).<\/jats:p>","DOI":"10.1007\/s00165-016-0361-7","type":"journal-article","created":{"date-parts":[[2016,3,7]],"date-time":"2016-03-07T07:28:11Z","timestamp":1457335691000},"page":"469-497","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["A language-independent proof system for full program equivalence"],"prefix":"10.1145","volume":"28","author":[{"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"first","affiliation":[{"name":"Faculty of Computer Science, \u201cAlexandru Ioan Cuza\u201d University, 16, General Berthelot Street, 700483, Iasi, Romania"}]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[{"name":"Faculty of Computer Science, \u201cAlexandru Ioan Cuza\u201d University, 16, General Berthelot Street, 700483, Iasi, Romania"}]},{"given":"Vlad","family":"Rusu","sequence":"additional","affiliation":[{"name":"Inria, Lille, France"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, Champaign, USA"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Amal Ahmed Derek Dreyer Andreas Rossberg (2009) State-dependent representation independence. In POPL 2009 pp 340\u2013353","DOI":"10.1145\/1594834.1480925"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Tamarah Arons Elad Elster Limor Fix Sela Mador-Haim Michael Mishaeli Jonathan Shalev Eli Singerman Andreas Tiemeyer Moshe Y. Vardi Lenore D. Zuck (2005) Formal verification of backward compatibility of microcode. In CAV 2005 volume 3576 of LNCS pp 185\u2013198","DOI":"10.1007\/11513988_20"},{"key":"e_1_2_1_2_3_2","unstructured":"Yves Bertot Pierre Castran (2010) Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions . Springer 1st edition"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Nick Benton (2004) Simple relational correctness proofs for static analyses and program transformations. In POPL 2004 pp 14\u201325","DOI":"10.1145\/982962.964003"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Nick Benton Chung-Kil Hur (2009) Biorthogonality step-indexing and compiler correctness. In ICFP 2009 pp 97\u2013108","DOI":"10.1145\/1631687.1596567"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Denis Bogd\u0103na\u015f Grigore Ro\u015fu (2015) K-Java: A Complete Semantics of Java. In POPL 2015 pp 445\u2013456","DOI":"10.1145\/2775051.2676982"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"\u015etefan Ciob\u00e2c\u0103 Dorel Lucanu Vlad Rusu Grigore Ro\u015fu (2015) A theoretical foundation for programming language aggregation. In WADT 2014 volume 9463 of LNCS pp 30\u201347","DOI":"10.1007\/978-3-319-28114-8_3"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Andrei \u015etef\u0103nescu \u015etefan Ciob\u00e2c\u0103 Radu Mereu\u0163\u0103 Brandon M. Moore Traian Florin \u015eerb\u0103nu\u0163\u0103 Grigore Ro\u015fu (2014) All-path reachability logic. In RTA-TLCA\u201914 volume 8560 of LNCS pp 425\u2013440","DOI":"10.1007\/978-3-319-08918-8_29"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Claudia Elena Chiri\u0163\u0103 Traian Florin \u015eerb\u0103nu\u0163\u0103 (2015) An institutional foundation for the K semantic framework. In WADT 2014 volume 9463 of LNCS pp 9\u201329","DOI":"10.1007\/978-3-319-28114-8_2"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Sagar Chaki Arie Gurfinkel Ofer Strichman (2012) Regression verification for multi-threaded programs. In VMCAI 2012 volume 7148 of LNCS pp 119\u2013135","DOI":"10.1007\/978-3-642-27940-9_9"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"\u015etefan Ciob\u00e2c\u0103 (2014) Reducing partial equivalence to partial correctness. In SYNASC 2014 pp 164\u2013171. IEEE","DOI":"10.1109\/SYNASC.2014.30"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Sorin Cr\u0103ciunescu (2002) Proving the equivalence of CLP programs. In ICLP 2002 volume 2401 of LNCS pp 287\u2013301","DOI":"10.1007\/3-540-45619-8_20"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Chucky Ellison Grigore Ro\u015fu (2012) An executable formal semantics of C with applications. In POPL 2012 pp 533\u2013544","DOI":"10.1145\/2103621.2103719"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-008-0075-2"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1472"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Richard K. Guy (1983) Don\u2019t try to solve these problems. The American Mathematical Monthly 90(1):35\u201338 39\u201341","DOI":"10.1080\/00029890.1983.11971148"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Chung-Kil Hur Derek Dreyer (2011) A kripke logical relation between ML and assembly. In POPL 2011 pp 133\u2013146","DOI":"10.1145\/1925844.1926402"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Chung-Kil Hur Derek Dreyer Georg Neis Viktor Vafeiadis (2012) The marriage of bisimulations and kripke logical relations. In POPL 2012 pp 59\u201372","DOI":"10.1145\/2103621.2103666"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Anne Elisabeth Haxthausen Friederike Nickl (1996) Pushouts of order-sorted algebraic specifications. In AMAST 1996 pp 132\u2013147. Springer-Verlag","DOI":"10.1007\/BFb0014312"},{"key":"e_1_2_1_2_20_2","unstructured":"Chung-Kil Hur Georg Neis Derek Dreyer Viktor Vafeiadis (2014) A Logical Step Forward in Parametric Bisimulations. Technical Report 003 MPI-SWS January"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Sudipta Kundu Zachary Tatlock Sorin Lerner (2009) Proving optimizations correct using parameterized program equivalence. In PLDI 2009 pp 327\u2013337. ACM","DOI":"10.1145\/1543135.1542513"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Shuvendu K. Lahiri Chris Hawblitzel Ming Kawaguchi Henrique Reb\u00ealo (2012) SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In CAV 2012 volume 7358 of LNCS pp 712\u2013717","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Dorel Lucanu Vlad Rusu (2014) Program equivalence by circular reasoning. Formal Aspects of Computing pp 1\u201326","DOI":"10.1007\/978-3-642-38613-8_25"},{"key":"e_1_2_1_2_26_2","unstructured":"Dorel Lucanu Vlad Rusu Andrei Arusoaie A Generic Framework for Symbolic Execution: Theory and Applications. Journal of Symbolic Computation to appear"},{"key":"e_1_2_1_2_27_2","unstructured":"Robin Milner (1989) Communication and concurrency . Prentice Hall"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"John C. Mitchell (1986) Representation independence and data abstraction. In POPL 1986 pp 263\u2013276","DOI":"10.1145\/512644.512669"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Jos\u00e9 Meseguer Grigore Ro\u015fu (2004) Rewriting logic semantics: From language specifications to formal analysis tools. In IJCAR 2004 volume 3097 of LNCS pp 1\u201344","DOI":"10.1007\/978-3-540-25984-8_1"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"George Necula (2000) Translation validation for an optimizing compiler. In PLDI 2000 pp 83\u201394. ACM","DOI":"10.1145\/358438.349314"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Daejun Park Andrei \u015etef\u0103nescu Grigore Ro\u015fu (2015) KJS: A complete formal semantics of JavaScript. In PLDI 2015 pp 346\u2013356","DOI":"10.1145\/2813885.2737991"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Andrew M. Pitts (2002) Operational semantics and program equivalence. In Applied Semantics Summer School volume 2395 of LNCS pp 378\u2013412","DOI":"10.1007\/3-540-45699-6_8"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Grigore Ro\u015fu Andrei \u015etef\u0103nescu (2012) Checking reachability using matching logic. In OOPSLA pp 555\u2013574. ACM","DOI":"10.1145\/2398857.2384656"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Grigore Ro\u015fu Andrei \u015etef\u0103nescu (2012) Towards a unified theory of operational and axiomatic semantics. In ICALP 2012 volume 7392 of LNCS pp 351\u2013363","DOI":"10.1007\/978-3-642-31585-5_33"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Grigore Ro\u015fu Andrei \u015etef\u0103nescu R\u015e;tefan Ciob\u00e2c\u0103 Brandon M. Moore (2013) One-path reachability logic. In LICS 2013 pp 358\u2013367. IEEE","DOI":"10.1109\/LICS.2013.42"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Grigore Ro\u015fu Chucky Ellison Wolfram Schulte (2010) Matching logic: An alternative to Hoare\/Floyd logic. In AMAST 2010 volume 6486 of LNCS pp 142\u2013162","DOI":"10.1007\/978-3-642-17796-5_9"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"John C. Reynolds (2002) Separation logic: A logic for shared mutable data structures. In LICS 2002 pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Grigore Ro\u015fu (2006) Equality of streams is a \u03a020-complete problem. In ICFP 2006 pp 184\u2013191. ACM","DOI":"10.1145\/1160074.1159827"},{"key":"e_1_2_1_2_39_2","unstructured":"Grigore Ro\u015fu (2015) Matching logic\u2014extended abstract. In RTA 2015 volume 36 of LIPIcs pp 5\u201321"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi (2011) Introduction to Bisimulation and Coinduction . Cambridge University Press New York NY USA","DOI":"10.1017\/CBO9780511777110"},{"key":"e_1_2_1_2_41_2","unstructured":"Fabio Somenzi Andreas Kuehlmann (2006) Electronic Design Automation For Integrated Circuits Handbook volume 2 chapter 4: Equivalence Checking. CRC Press"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Davide Sangiorgi Naoki Kobayashi Eijiro Sumii (2011) Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems 33(1):5","DOI":"10.1145\/1889997.1890002"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Traian-Florin \u015eerb\u0103nu\u0163\u0103 Grigore Ro\u015fu Jos\u00e9 Meseguer (2009) A rewriting logic approach to operational semantics. Information and Computation 207(2):305\u2013340","DOI":"10.1016\/j.ic.2008.03.026"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0361-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0361-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0361-7","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0361-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0361-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,17]],"date-time":"2023-08-17T04:20:26Z","timestamp":1692246026000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0361-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":43,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["10.1007\/s00165-016-0361-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0361-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2016,5]]},"assertion":[{"value":"2 June 2015","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 February 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 March 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}