{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:00:17Z","timestamp":1762459217990},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319117362"},{"type":"electronic","value":"9783319117379"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11737-9_6","type":"book-chapter","created":{"date-parts":[[2014,10,14]],"date-time":"2014-10-14T20:52:14Z","timestamp":1413319934000},"page":"75-90","source":"Crossref","is-referenced-by-count":6,"title":["A Language-Independent Proof System for Mutual Program Equivalence"],"prefix":"10.1007","author":[{"given":"\u015etefan","family":"Ciob\u00e2c\u0103","sequence":"first","affiliation":[]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[]},{"given":"Vlad","family":"Rusu","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/11513988_20","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2005","unstructured":"Arons, T., Elster, E., Fix, L., Mador-Haim, S., Mishaeli, M., Shalev, J., Singerman, E., Tiemeyer, A., Vardi, M.Y., Zuck, L.D.: Formal verification of backward compatibility of microcode. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 185\u2013198. Springer, Heidelberg (2005)"},{"key":"6_CR2","unstructured":"\u00c7iob\u00e2c\u0103, S., Lucanu, D., Rusu, V., Ro\u015fu, G.: A language independent proof system for mutual program equivalence. Technical Report 14-01, Al. I. Cuza Univ."},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-27940-9_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Chaki","year":"2012","unstructured":"Chaki, S., Gurfinkel, A., Strichman, O.: Regression verification for multi-threaded programs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 119\u2013135. Springer, Heidelberg (2012)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/3-540-45619-8_20","volume-title":"Logic Programming","author":"S. Craciunescu","year":"2002","unstructured":"Craciunescu, S.: Proving the equivalence of CLP programs. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol.\u00a02401, pp. 287\u2013301. Springer, Heidelberg (2002)"},{"key":"6_CR5","unstructured":"Godlin, B., Strichman, O.: Regression verification: proving the equivalence of similar programs. Software Testing, Verification and Reliability (To appear)"},{"issue":"6","key":"6_CR6","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/s00236-008-0075-2","volume":"45","author":"B. Godlin","year":"2008","unstructured":"Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Informatica\u00a045(6), 403\u2013439 (2008)","journal-title":"Acta Informatica"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/BFb0014312","volume-title":"Algebraic Methodology and Software Technology","author":"A.E. Haxthausen","year":"1996","unstructured":"Haxthausen, A.E., Nickl, F.: Pushouts of order-sorted algebraic specifications. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 132\u2013147. Springer, Heidelberg (1996)"},{"issue":"10","key":"6_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: PLDI, pp. 327\u2013337. ACM (2009)","DOI":"10.1145\/1543135.1542513"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"712","DOI":"10.1007\/978-3-642-31424-7_54","volume-title":"Computer Aided Verification","author":"S. Lahiri","year":"2012","unstructured":"Lahiri, S., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: Symdiff: A language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 712\u2013717. Springer, Heidelberg (2012)"},{"issue":"7","key":"6_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Lucanu, D., Rusu, V.: Program equivalence by circular reasoning. Technical Report RR-8116, INRIA (2012)","DOI":"10.1007\/978-3-642-38613-8_25"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-38613-8_25","volume-title":"Integrated Formal Methods","author":"D. Lucanu","year":"2013","unstructured":"Lucanu, D., Rusu, V.: Program equivalence by circular reasoning. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol.\u00a07940, pp. 362\u2013377. Springer, Heidelberg (2013)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Necula, G.: Translation validation for an optimizing compiler. In: PLDI, pp. 83\u201394. ACM (2000)","DOI":"10.1145\/358438.349314"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-45699-6_8","volume-title":"Applied Semantics","author":"A. Pitts","year":"2002","unstructured":"Pitts, A.: Operational semantics and program equivalence. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol.\u00a02395, pp. 378\u2013412. Springer, Heidelberg (2002)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Checking reachability using matching logic. In: OOPSLA, pp. 555\u2013574. ACM (2012)","DOI":"10.1145\/2398857.2384656"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-17796-5_9","volume-title":"Algebraic Methodology and Software Technology","author":"G. Ro\u015fu","year":"2011","unstructured":"Ro\u015fu, G., Ellison, C., Schulte, W.: Matching logic: An alternative to hoare\/Floyd logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol.\u00a06486, pp. 142\u2013162. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11737-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T23:22:26Z","timestamp":1558308146000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11737-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319117362","9783319117379"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11737-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}