{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:29:19Z","timestamp":1767137359531,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031197550","type":"print"},{"value":"9783031197567","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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-19756-7_15","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T03:02:54Z","timestamp":1666148574000},"page":"259-280","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Notion of\u00a0Equivalence for\u00a0Refactorings with\u00a0Abstract Execution"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3428-2929","authenticated-orcid":false,"given":"Ole J\u00f8rgen","family":"Abusdal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0996-2543","authenticated-orcid":false,"given":"Eduard","family":"Kamburjan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8763-5548","authenticated-orcid":false,"given":"Violet","family":"Ka I. Pun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1031-6936","authenticated-orcid":false,"given":"Volker","family":"Stolz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"15_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"15_CR2","doi-asserted-by":"publisher","unstructured":"Baldoni, R., Coppa, E., D\u2019Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1\u201350:39 (2018). https:\/\/doi.org\/10.1145\/3182657","DOI":"10.1145\/3182657"},{"key":"15_CR3","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). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), Pacific Grove, CA, USA, 28\u201330 June 2004, pp. 100\u2013114. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/CSFW.2004.17","DOI":"10.1109\/CSFW.2004.17"},{"key":"15_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kov\u00e1cs, L., Maffei, M.: Verifying relational properties using trace logic. In: Barrett, C.W., Yang, J. (eds.) 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, 22\u201325 October 2019, pp. 170\u2013178. IEEE (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894277","DOI":"10.23919\/FMCAD.2019.8894277"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification - specification is the new bottleneck. In: SSV. EPTCS, vol. 102, pp. 18\u201332 (2012)","DOI":"10.4204\/EPTCS.102.4"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-14125-1_2","volume-title":"Logic-Based Program Synthesis and Transformation","author":"B Beckert","year":"2014","unstructured":"Beckert, B., Bruns, D., Klebanov, V., Scheben, C., Schmitt, P.H., Ulbrich, M.: Information flow in object-oriented software. In: Gupta, G., Pe\u00f1a, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 19\u201337. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-14125-1_2"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-319-98047-8_3","volume-title":"Principled Software Development","author":"B Beckert","year":"2018","unstructured":"Beckert, B., Ulbrich, M.: Trends in relational program verification. In: Principled Software Development, pp. 41\u201358. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98047-8_3"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-24312-2_21","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R Bubel","year":"2015","unstructured":"Bubel, R., Din, C.C., H\u00e4hnle, R., Nakata, K.: A dynamic logic with traces and coinduction. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 307\u2013322. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_21"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"\u00c1 Darvas","year":"2005","unstructured":"Darvas, \u00c1., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193\u2013209. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32004-3_20"},{"issue":"5\u20136","key":"15_CR11","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1016\/j.jlamp.2014.03.003","volume":"83","author":"CC Din","year":"2014","unstructured":"Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. J. Log. Algebraic Methods Program. 83(5\u20136), 360\u2013383 (2014). https:\/\/doi.org\/10.1016\/j.jlamp.2014.03.003","journal-title":"J. Log. Algebraic Methods Program."},{"issue":"1","key":"15_CR12","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.jlamp.2014.09.001","volume":"84","author":"J Dovland","year":"2015","unstructured":"Dovland, J., Johnsen, E.B., Owe, O., Yu, I.C.: A proof system for adaptable class hierarchies. J. Log. Algebraic Methods Program. 84(1), 37\u201353 (2015). https:\/\/doi.org\/10.1016\/j.jlamp.2014.09.001","journal-title":"J. Log. Algebraic Methods Program."},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-47166-2_36","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"AM Eilertsen","year":"2016","unstructured":"Eilertsen, A.M., Bagge, A.H., Stolz, V.: Safer refactorings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 517\u2013531. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_36"},{"key":"15_CR14","unstructured":"Fowler, M.: Refactoring - Improving the Design of Existing Code. Addison Wesley object technology series. Addison-Wesley (1999)"},{"key":"15_CR15","unstructured":"Fowler, M.: Refactoring: Improving the Design of Existing Code, 2nd edn. Addison-Wesley Signature Series (Fowler), Addison-Wesley (2018)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Garrido, A., Meseguer, J.: Formal specification and verification of java refactorings. In: 2006 Sixth IEEE International Workshop on Source Code Analysis and Manipulation, pp. 165\u2013174. IEEE (2006)","DOI":"10.1109\/SCAM.2006.16"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Huisman, M., Ahrendt, W., Bruns, D., Hentschel, M.: Formal specification with jml. Technical Report 10, Karlsruher Institut f\u00fcr Technologie (KIT) (2014). https:\/\/doi.org\/10.5445\/IR\/1000041881","DOI":"10.5445\/IR\/1000041881"},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-030-29026-9_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"E Kamburjan","year":"2019","unstructured":"Kamburjan, E.: Behavioral program logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 391\u2013408. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_22"},{"key":"15_CR20","unstructured":"Kamburjan, E., Wasser, N.: Deductive verification of programs with underspecified semantics by model extraction. CoRR abs\/2110.01964 (2021)"},{"issue":"3","key":"15_CR21","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-017-9433-5","volume":"60","author":"M Kiefer","year":"2018","unstructured":"Kiefer, M., Klebanov, V., Ulbrich, M.: Relational program reasoning using compiler IR - combining static verification and dynamic analysis. J. Autom. Reason. 60(3), 337\u2013363 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9433-5","journal-title":"J. Autom. Reason."},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-31424-7_5","volume-title":"Computer Aided Verification","author":"CJ Myers","year":"2012","unstructured":"Myers, C.J.: Formal verification of genetic circuits. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 5\u20135. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_5"},{"key":"15_CR23","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Information Processing, Proceedings of the 2nd IFIP Congress 1962, Munich, Germany, 27 August\u20131 September 1962, pp. 21\u201328. North-Holland (1962)"},{"key":"15_CR24","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Pretschner, A., Peled, D., Hutzelmann, T. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 50, pp. 104\u2013125. IOS Press (2017). https:\/\/doi.org\/10.3233\/978-1-61499-810-5-104","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"15_CR25","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-88479-8_23","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"L Quan","year":"2008","unstructured":"Quan, L., Zongyan, Q., Liu, Z.: Formal use of design patterns and refactoring. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 323\u2013338. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88479-8_23"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"0 Sch\u00e4fer, M., de Moor, O.: Specifying and implementing refactorings. In: Object-Oriented Programming, Systems, Languages, and Applications (2010)","DOI":"10.1145\/1869459.1869485"},{"issue":"4","key":"15_CR27","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1109\/MS.2010.63","volume":"27","author":"G Soares","year":"2010","unstructured":"Soares, G., Gheyi, R., Serey, D., Massoni, T.: Making program refactoring safer. IEEE Softw. 27(4), 52\u201357 (2010)","journal-title":"IEEE Softw."},{"key":"15_CR28","unstructured":"Steinh\u00f6fel, D.: Abstract Execution: Automatically Proving Infinitely Many Programs. Ph.D. thesis, TU Darmstadt, Dept. of Computer Science (2020). https:\/\/tuprints.ulb.tu-darmstadt.de\/id\/eprint\/8540"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-030-64437-6_16","volume-title":"Programming Languages and Systems","author":"D Steinh\u00f6fel","year":"2020","unstructured":"Steinh\u00f6fel, D.: REFINITY to model and prove program transformation rules. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 311\u2013319. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_16"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-30942-8_20","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"D Steinh\u00f6fel","year":"2019","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Abstract execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 319\u2013336. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_20"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-030-61470-6_9","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles","author":"V Stolz","year":"2020","unstructured":"Stolz, V., Pun, V.K.I., Gheyi, R.: Refactoring and active object languages. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12477, pp. 138\u2013158. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61470-6_9"},{"key":"15_CR32","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011). https:\/\/d-nb.info\/1010034960"},{"key":"15_CR33","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/bs.adcom.2018.10.002","volume":"113","author":"G Yang","year":"2019","unstructured":"Yang, G., Filieri, A., Borges, M., Clun, D., Wen, J.: Chapter five - advances in symbolic execution. Adv. Comput. 113, 225\u2013287 (2019). https:\/\/doi.org\/10.1016\/bs.adcom.2018.10.002","journal-title":"Adv. Comput."}],"updated-by":[{"DOI":"10.1007\/978-3-031-19756-7_24","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2022,10,17]],"date-time":"2022-10-17T00:00:00Z","timestamp":1665964800000}}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19756-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,4]],"date-time":"2023-04-04T20:07:57Z","timestamp":1680638877000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19756-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031197550","9783031197567"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19756-7_15","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":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"17 October 2022","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A correction has been published.","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","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":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}