{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:13:43Z","timestamp":1760044423203,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662544334"},{"type":"electronic","value":"9783662544341"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-662-54434-1_35","type":"book-chapter","created":{"date-parts":[[2017,3,18]],"date-time":"2017-03-18T04:20:06Z","timestamp":1489810806000},"page":"937-963","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Modular Verification of Procedure Equivalence in the Presence of Memory Allocation"],"prefix":"10.1007","author":[{"given":"Tim","family":"Wood","sequence":"first","affiliation":[]},{"given":"Sophia","family":"Drossopolou","sequence":"additional","affiliation":[]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[]},{"given":"Susan","family":"Eisenbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,19]]},"reference":[{"key":"35_CR1","unstructured":"Banerjee, A., Schmidt, D.A., Nikouei, M.: Relational logic with framing and hypotheses. In: FSTTCS (2016)"},{"key":"35_CR2","unstructured":"de Barker, J.W.: Axiomatics of simple assignment statements. In: MR 94 (1968)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). doi:10.1007\/11804192_17"},{"key":"35_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-642-35722-0_3","volume-title":"Logical Foundations of Computer Science","author":"G Barthe","year":"2013","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: asymmetric product programs for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 29\u201343. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-35722-0_3"},{"issue":"5","key":"35_CR5","doi-asserted-by":"publisher","first-page":"847","DOI":"10.1016\/j.jlamp.2016.05.004","volume":"85","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Product programs and relational program logics. J. Logical Algebraic Methods Program. 85(5), 847\u2013859 (2016)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-642-21437-0_17","volume-title":"FM 2011: Formal Methods","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200\u2013214. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-21437-0_17"},{"key":"35_CR7","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Workshop on Computer Security Foundations. IEEE Computer Society (2004)"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"Bavota, G., et al.: When does a refactoring induce bugs? An empirical study. In: 2012 IEEE 12th International Working Conference on Source Code Analysis and Manipulation (SCAM). IEEE (2012)","DOI":"10.1109\/SCAM.2012.20"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/11874683_12","volume-title":"Computer Science Logic","author":"N Benton","year":"2006","unstructured":"Benton, N.: Abstracting allocation. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 182\u2013196. Springer, Heidelberg (2006). doi:10.1007\/11874683_12"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (2004)","DOI":"10.1145\/964001.964003"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"Benton, N., et al.: Relational semantics for effect-based program transformations with dynamic allocation. In: Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. ACM (2007)","DOI":"10.1145\/1273920.1273932"},{"key":"35_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-22863-6_6","volume-title":"Interactive Theorem Proving","author":"L Beringer","year":"2011","unstructured":"Beringer, L.: Relational decomposition. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 39\u201354. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22863-6_6"},{"key":"35_CR13","doi-asserted-by":"crossref","unstructured":"Bozga, M., Iosif, R., Laknech, Y.: Storeless semantics and alias logic. In: Proceedings of the 2003 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2003, San Diego, California, USA. ACM (2003)","DOI":"10.1145\/777388.777395"},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D., Yorav, K.: Behavioral consistency of C and verilog programs using bounded model checking. In: 2003 Proceedings of the Design Automation Conference. IEEE (2003)","DOI":"10.21236\/ADA461052"},{"key":"35_CR15","volume-title":"Structured Programming","author":"OJ Dahl","year":"1972","unstructured":"Dahl, O.J., Dijkstra, E.W., Hoare, C.A.R.: Structured Programming. Academic Press Ltd., Cambridge (1972)"},{"key":"35_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"35_CR17","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"issue":"2","key":"35_CR18","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s10703-015-0234-3","volume":"47","author":"D Elenbogen","year":"2015","unstructured":"Elenbogen, D., Katz, S., Strichman, O.: Proving mutual termination. Form. Methods Syst. Des. 47(2), 204\u2013229 (2015)","journal-title":"Form. Methods Syst. Des."},{"key":"35_CR19","doi-asserted-by":"crossref","unstructured":"Felsing, D., et al.: Automating regression verification. In: Proceedings of the 29th ACM\/IEEE International Conference on Automated Software Engineering, ASE 2014. ACM (2014)","DOI":"10.1145\/2642937.2642987"},{"issue":"6","key":"35_CR20","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 45(6), 403\u2013439 (2008)","journal-title":"Acta Informatica"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: Proceedings of the 46th Annual Design Automation Conference. ACM (2009)","DOI":"10.1145\/1629911.1630034"},{"key":"35_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-642-38574-2_20","volume-title":"Automated Deduction \u2013 CADE-24","author":"C Hawblitzel","year":"2013","unstructured":"Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Reb\u00ealo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 282\u2013299. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38574-2_20"},{"issue":"10","key":"35_CR23","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"35_CR24","unstructured":"Igarishi, S.: An axiomatic approach to equivalence problems of algorithms with applications. Ph.D. thesis (1964)"},{"key":"35_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0167-6423(99)00024-6","volume":"37","author":"R Joshi","year":"2000","unstructured":"Joshi, R., Leino, K.R.M.: A semantic approach to secure information flow. Sci. Comput. Program. 37, 1\u20133 (2000)","journal-title":"Sci. Comput. Program."},{"key":"35_CR26","unstructured":"Kawaguchi, M., Lahiri, S.K., Reb\u00ealo, H.: Conditional equivalence. Technical report MSR-TR-2010-119. Microsoft, October 2010"},{"key":"35_CR27","doi-asserted-by":"crossref","unstructured":"Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (2006)","DOI":"10.1145\/1111037.1111050"},{"key":"35_CR28","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM (2009)","DOI":"10.1145\/1542476.1542513"},{"key":"35_CR29","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":"SK Lahiri","year":"2012","unstructured":"Lahiri, S.K., 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. 7358, pp. 712\u2013717. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31424-7_54"},{"key":"35_CR30","doi-asserted-by":"crossref","unstructured":"Lahiri, S., et al.: Differential assertion checking. In: Foundations of Software Engineering. ACM (2013)","DOI":"10.1145\/2491411.2491452"},{"key":"35_CR31","doi-asserted-by":"crossref","unstructured":"Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs\u2019. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014. ACM (2014)","DOI":"10.1145\/2594291.2594334"},{"key":"35_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-17511-4_20"},{"key":"35_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-78739-6_24","volume-title":"Programming Languages and Systems","author":"KRM Leino","year":"2008","unstructured":"Leino, K.R.M., M\u00fcller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 307\u2013321. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-78739-6_24"},{"issue":"1","key":"35_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","volume":"4","author":"R Milner","year":"1977","unstructured":"Milner, R.: Fully abstract models of typed $$\\lambda $$-calculi. Theor. Comput. Sci. 4(1), 1\u201322 (1977)","journal-title":"Theor. Comput. Sci."},{"key":"35_CR35","unstructured":"Park, J., et al.: An empirical study of supplementary bug fixes. In: 2012 9th IEEE Working Conference on Mining Software Repositories (MSR) (2012)"},{"key":"35_CR36","doi-asserted-by":"crossref","unstructured":"Partush, N., Yahav, E.: Abstract semantic differencing via speculative correlation. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications. ACM (2014)","DOI":"10.1145\/2660193.2660245"},{"key":"35_CR37","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":"AM Pitts","year":"2002","unstructured":"Pitts, A.M.: Operational semantics and program equivalence. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 378\u2013412. Springer, Heidelberg (2002). doi:10.1007\/3-540-45699-6_8"},{"key":"35_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-642-22110-1_59","volume-title":"Computer Aided Verification","author":"M Stepp","year":"2011","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 737\u2013742. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-22110-1_59"},{"key":"35_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1007\/978-3-319-48989-6_39","volume-title":"FM 2016: Formal Methods","author":"O Strichman","year":"2016","unstructured":"Strichman, O., Veitsman, M.: Regression verification for unbalanced recursive functions. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 645\u2013658. Springer, Heidelberg (2016). doi:10.1007\/978-3-319-48989-6_39"},{"issue":"1","key":"35_CR40","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1023\/A:1010022312623","volume":"13","author":"RD Tennent","year":"2000","unstructured":"Tennent, R.D., Ghica, D.R.: Abstract models of storage. High.-Order Symbolic Comput. 13(1), 119\u2013129 (2000)","journal-title":"High.-Order Symbolic Comput."},{"key":"35_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). doi:10.1007\/11547662_24"},{"key":"35_CR42","doi-asserted-by":"crossref","unstructured":"Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM (2011)","DOI":"10.1145\/1993498.1993533"},{"issue":"2","key":"35_CR43","first-page":"181","volume":"38","author":"N Tzevelekos","year":"2012","unstructured":"Tzevelekos, N.: Program equivalence in a simple language with state. Comput. Lang. Syst. Struct. 38(2), 181\u2013198 (2012)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"35_CR44","unstructured":"Wood, T.: Equivalence verification for memory allocating procedures. Ph.D. thesis, Imperial College London, Under Submission"},{"key":"35_CR45","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H Yang","year":"2007","unstructured":"Yang, H.: Relational separation logic. Theor. Comput. Sci. 375, 1\u20133 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"35_CR46","unstructured":"Yanov, Y.: Logical operator schemes. In: Kybernetilca I (1958)"},{"key":"35_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-68237-0_5","volume-title":"FM 2008: Formal Methods","author":"A Zaks","year":"2008","unstructured":"Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35\u201351. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-68237-0_5"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54434-1_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,26]],"date-time":"2021-10-26T15:56:57Z","timestamp":1635263817000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-54434-1_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783662544334","9783662544341"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54434-1_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"19 March 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Uppsala","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Sweden","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 April 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2017a","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.etaps.org\/index.php\/2017\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}