{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:04:19Z","timestamp":1776373459994,"version":"3.51.2"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995263","type":"print"},{"value":"9783030995270","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a bounded equivalence verification technique for higher-order programs with local state. This technique combines fully abstract <jats:italic>symbolic environmental bisimulations<\/jats:italic> similar to symbolic game semantics, novel <jats:italic>up-to techniques<\/jats:italic>, and lightweight <jats:italic>state invariant annotations<\/jats:italic>. This yields an equivalence verification technique with no false positives or negatives. The technique is bounded-complete, in that all inequivalences are automatically detected given large enough bounds. Moreover, several hard equivalences are proved automatically or after being annotated with state invariants. We realise the technique in a tool prototype called <jats:sc>Hobbit<\/jats:sc> and benchmark it with an extensive set of new and existing examples. <jats:sc>Hobbit<\/jats:sc> can prove many classical equivalences including all Meyer and Sieber examples.<\/jats:p>","DOI":"10.1007\/978-3-030-99527-0_10","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:37:21Z","timestamp":1648535841000},"page":"178-195","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3970-2486","authenticated-orcid":false,"given":"Vasileios","family":"Koutavas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5783-9454","authenticated-orcid":false,"given":"Yu-Yang","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8509-8059","authenticated-orcid":false,"given":"Nikos","family":"Tzevelekos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Dreyer, D., Rossberg, A.: State-dependent representation independence. In: POPL. Association for Computing Machinery (2009)","DOI":"10.1145\/1480881.1480925"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS. Springer, Berlin Heidelberg (1999)","DOI":"10.21236\/ADA360973"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normal-form bisimilarity for state. In: FOSSACS 2019, ETAPS 2019, Prague, Czech Republic. Springer (2019)","DOI":"10.1007\/978-3-030-17127-8_6"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A computationally sound mechanized prover for security protocols. In: IEEE Symposium on Security and Privacy (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bohr, N., Birkedal, L.: Relational reasoning for recursive types and references. In: Kobayashi, N. (ed.) APLAS. LNCS, vol.\u00a04279, pp. 79\u201396. Springer (2006)","DOI":"10.1007\/11924661_5"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: TACAS. Springer, Berlin Heidelberg (2004)","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Cordeiro, L., Kroening, D., Schrammel, P.: JBMC: Bounded model checking for Java Bytecode. In: TACAS. Springer (2019)","DOI":"10.1007\/978-3-030-17502-3_17"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Dimovski, A.: Program verification using symbolic game semantics. TCS 560 (2014)","DOI":"10.1016\/j.tcs.2014.01.016"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Felsing, D., Grebing, S., Klebanov, V., R\u00fcmmer, P., Ulbrich, M.: Automating regression verification. In: ACM\/IEEE ASE \u201914. ACM (2014)","DOI":"10.1145\/2642937.2642987"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45(6) (2008)","DOI":"10.1007\/s00236-008-0075-2"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: DAC. ACM (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Hopkins, D., Murawski, A.S., Ong, C.L.: Hector: An equivalence checker for a higher-order fragment of ML. In: CAV. LNCS, Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_63"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Hur, C.K., Dreyer, D., Neis, G., Vafeiadis, V.: The marriage of bisimulations and Kripke logical relations. SIGPLAN Not. (2012)","DOI":"10.1145\/2103656.2103666"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Jaber, G.: SyTeCi: Automating contextual equivalence for higher-order programs with references. Proc. ACM Program. Lang. 4(POPL) (2020)","DOI":"10.1145\/3371127"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Jaber, G., Tabareau, N.: Kripke open bisimulation - A marriage of game semantics and operational techniques. In: APLAS. Springer (2015)","DOI":"10.1007\/978-3-319-26529-2_15"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: POPL. ACM (2006)","DOI":"10.1145\/1111037.1111050"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In: CAV. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"10_CR18","unstructured":"Laird, J.: A fully abstract trace semantics for general references. In: ICALP, Wroclaw, Poland. LNCS, Springer (2007)"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Lassen, S.B., Levy, P.B.: Typed normal form bisimulation. In: Computer Science Logic. Springer, Berlin Heidelberg (2007)","DOI":"10.1109\/LICS.2008.26"},{"key":"10_CR20","unstructured":"Lin, Y., Tzevelekos, N.: Symbolic execution game semantics. In: FSCD. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables. In: POPL. Association for Computing Machinery (1988)","DOI":"10.1145\/73560.73577"},{"key":"10_CR22","unstructured":"Morris, Jr., J.H.: Lambda Calculus Models of Programming Languages. Ph.D. thesis, MIT, Cambridge, MA (1968)"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 337\u2013340. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Murawski, A.S., Ramsay, S.J., Tzevelekos, N.: A contextual equivalence checker for IMJ*. In: ATVA. Springer (2015)","DOI":"10.1007\/978-3-319-24953-7_19"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Murawski, A.S., Tzevelekos, N.: Nominal game semantics. FTPL 2(4) (2016)","DOI":"10.1561\/2500000017"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Patterson, D., Ahmed, A.: The next 700 compiler correctness theorems (functional pearl). Proc. ACM Program. Lang. 3(ICFP) (2019)","DOI":"10.1145\/3341689"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Pous, D.: Coinduction all the way up. In: ACM\/IEEE LICS. ACM (2016)","DOI":"10.1145\/2933575.2934564"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Pous, D., Sangiorgi, D.: Enhancements of the bisimulation proof method. In: Advanced Topics in Bisimulation and Coinduction. CUP (2012)","DOI":"10.1017\/CBO9780511792588"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: LICS. IEEE Computer Society (2007)","DOI":"10.1109\/LICS.2007.17"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienm\u00fcller, T.: Successful use of incremental BMC in the automotive industry. In: FMICS (2015)","DOI":"10.1007\/978-3-319-19458-5_5"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99527-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,12]],"date-time":"2024-03-12T08:46:56Z","timestamp":1710233216000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99527-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995263","9783030995270"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99527-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}