{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T23:10:04Z","timestamp":1749769804488,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Translation validation is an undecidable problem. Bisimulation relation based approaches, nevertheless, have been widely successful in translation validation of programs albeit with some drawbacks. These drawbacks include non-termination of the verification methodology and significant restrictions on the structures of programs to be checked for equivalence. We have developed a path based equivalence checker which propagates mismatched values over consecutive paths to alleviate these drawbacks. In this work, we show how a bisimulation relation between a program and its translated version can be constructed from the outputs of such a value propagation based equivalence checker. Moreover, none of the earlier methods that establish equivalence through construction of bisimulation relations has been shown to tackle code motions across loops; the present work demonstrates, for the first time, the existence of a bisimulation relation under such a situation.<\/jats:p>","DOI":"10.1007\/s00165-016-0406-y","type":"journal-article","created":{"date-parts":[[2016,11,29]],"date-time":"2016-11-29T11:02:02Z","timestamp":1480417322000},"page":"365-379","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Deriving bisimulation relations from path based equivalence checkers"],"prefix":"10.1145","volume":"29","author":[{"given":"Kunal","family":"Banerjee","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dipankar","family":"Sarkar","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chittaranjan","family":"Mandal","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Indian Institute of Technology, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Banerjee K Karfa C Sarkar D Mandal C (2012) A value propagation based equivalence checking method for verification of code motion techniques. In: ISED pp 67\u201371","DOI":"10.1109\/ISED.2012.28"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2314392"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2354298"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.62794"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1007506711786"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Floyd RW (1967) Assigning meaning to programs. In: Proceedings the 19th symposium on applied mathematics pp 19\u201332","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Gajski DD Dutt ND Wu AC-H Lin SY-L (1992) High-level synthesis: introduction to chip and system design. Kluwer Academic Publishers Norwell MA","DOI":"10.1007\/978-1-4615-3636-9"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Kundu S Lerner S Gupta R (2008) Validating high-level synthesis. In: CAV pp 459\u2013472","DOI":"10.1007\/978-3-540-70545-1_44"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2010.2042889"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Karfa C Mandal C Sarkar D Pentakota SR Reade C (2006) A formal verification method of scheduling in high-level synthesis. In: ISQED pp 71\u201378","DOI":"10.1109\/ISQED.2006.10"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2209291.2209303"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Knoop J Ruthing O Steffen B (1992) Lazy code motion. In: PLDI pp 224\u2013234","DOI":"10.1145\/143103.143136"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2009.2035542"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2007.913390"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Li T Guo Y Liu W Tang M (2013) Translation validation of scheduling in high level synthesis. In: GLSVLSI pp 101\u2013106","DOI":"10.1145\/2483028.2483070"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Lee C-H Shih C-H Huang J-D Jou J-Y (2011) Equivalence checking of scheduling with speculative code transformations in high-level synthesis. In: ASP-DAC pp 497\u2013502","DOI":"10.1109\/ASPDAC.2011.5722241"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Necula GC (2000) Translation validation for an optimizing compiler. In: PLDI pp 83\u201394","DOI":"10.1145\/358438.349314"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Siegel M Singerman E (1998) Translation validation. In: TACAS pp 151\u2013166","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_1_2_19_2","unstructured":"Rinard M (1999) Credible compilation. Technical report. In: Proceedings of CC 2001: International Conference on Compiler Construction"},{"key":"e_1_2_1_2_20_2","unstructured":"Rahmouni M Jerraya AA (1995) Formulation and evaluation of scheduling techniques for control flow graphs. In: EURO-DAC pp 386\u2013391"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Ruthing O Knoop J Steffen B (2000) Sparse code motion. In: POPL pp 170\u2013183","DOI":"10.1145\/325694.325715"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0406-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0406-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0406-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0406-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T22:34:43Z","timestamp":1749767683000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0406-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3]]},"references-count":21,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["10.1007\/s00165-016-0406-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0406-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,3]]}}}