{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:33:57Z","timestamp":1740123237341,"version":"3.37.3"},"reference-count":92,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T00:00:00Z","timestamp":1711411200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T00:00:00Z","timestamp":1711411200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005714","name":"Technische Universit\u00e4t Darmstadt","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005714","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose <jats:italic>Abstract Execution<\/jats:italic>, a static verification framework based on symbolic execution and dynamic frames for proving properties of <jats:italic>schematic<\/jats:italic> programs. Since a schematic program may potentially represent infinitely many concrete programs, Abstract Execution can analyze infinitely many programs at once. Trading off expressiveness and automation, the framework allows proving many interesting (universal, behavioral) properties <jats:italic>fully automatically<\/jats:italic>. Its main application are correctness proofs of <jats:italic>program transformations<\/jats:italic> represented as pairs of schematic programs. We implemented Abstract Execution in a deductive verification framework and designed a graphical workbench supporting the modeling process. Abstract Execution has been applied to correct code refactoring, analysis of the cost impact of transformation rules, and parallelization of sequential code. Using our framework, we found and reported several bugs in the refactoring engines of the <jats:sc>Java<\/jats:sc>\u00a0IDEs IntelliJ IDEA and Eclipse, which were acknowledged and fixed.<\/jats:p>","DOI":"10.1007\/s10817-023-09692-0","type":"journal-article","created":{"date-parts":[[2024,3,26]],"date-time":"2024-03-26T11:02:27Z","timestamp":1711450947000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Schematic Program Proofs with Abstract Execution"],"prefix":"10.1007","volume":"68","author":[{"given":"Dominic","family":"Steinh\u00f6fel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,26]]},"reference":[{"key":"9692_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B\u00a0Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"9692_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: Modeling in Event-B \u2013 System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"key":"9692_CR3","doi-asserted-by":"publisher","unstructured":"Abusdal, O.J., Kamburjan, E., Pun, V.K.I., Stolz, V.: A Notion of Equivalence for Refactorings with Abstract Execution. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering - 11th International Symposium, ISoLA 2022, Proceedings, Part II, LNCS, vol. 13702, pp. 259\u2013280. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-19756-7_15","DOI":"10.1007\/978-3-031-19756-7_15"},{"key":"9692_CR4","unstructured":"Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley series in computer science \/ World student series edition. Addison-Wesley (1986). https:\/\/www.worldcat.org\/oclc\/12285707"},{"key":"9692_CR5","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification \u2013 The KeY Book, LNCS, vol. 10001. Springer (2016).https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"9692_CR6","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Roth, A., Sasse, R.: Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics. In: G.\u00a0Sutcliffe, A.\u00a0Voronkov (eds.) Proc. 12th LPAR, LNCS, vol. 3835, pp. 412\u2013426. Springer (2005). https:\/\/doi.org\/10.1007\/11591191_29","DOI":"10.1007\/11591191_29"},{"key":"9692_CR7","doi-asserted-by":"publisher","unstructured":"Albert, E., H\u00e4hnle, R., Merayo, A., Steinh\u00f6fel, D.: Certified Abstract Cost Analysis. In: E.\u00a0Guerra, M.\u00a0Stoelinga (eds.) Proc. 24th Intern. Conf. on Fundamental Approaches to Software Engineering (FASE), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), LNCS, vol. 12649, pp. 24\u201345. Springer (2021).https:\/\/doi.org\/10.1007\/978-3-030-71500-7_2","DOI":"10.1007\/978-3-030-71500-7_2"},{"key":"9692_CR8","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-50:39 (2018).https:\/\/doi.org\/10.1145\/3182657","DOI":"10.1145\/3182657"},{"key":"9692_CR9","doi-asserted-by":"crossref","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal System Development with KIV. In: T.\u00a0Maibaum (ed.) Fundamental Approaches to Software Engineering, LNCS, pp. 363\u2013366. Springer (2000)","DOI":"10.1007\/3-540-46428-X_25"},{"key":"9692_CR10","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational Verification Using Product Programs. In: M.J. Butler, W.\u00a0Schulte (eds.) 17th Intl. Symp. on Formal Methods (FM), LNCS, vol. 6664, pp. 200\u2013214. Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"9692_CR11","doi-asserted-by":"publisher","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification \u2013 specification is the new bottleneck. In: F.\u00a0Cassez, R.\u00a0Huuck, G.\u00a0Klein, B.\u00a0Schlich (eds.) Proc. 7th Conf. on Systems Software Verification (SSV), EPTCS, vol. 102, pp. 18\u201332 (2012). https:\/\/doi.org\/10.4204\/EPTCS.102.4","DOI":"10.4204\/EPTCS.102.4"},{"key":"9692_CR12","doi-asserted-by":"publisher","unstructured":"Beckert, B., Ulbrich, M.: Trends in Relational Program Verification. In: Principled Software Development - Essays Dedicated to Arnd Poetzsch-Heffter on the Occasion of his 60th Birthday, pp. 41\u201358 (2018). https:\/\/doi.org\/10.1007\/978-3-319-98047-8_3","DOI":"10.1007\/978-3-319-98047-8_3"},{"key":"9692_CR13","doi-asserted-by":"crossref","unstructured":"Bubel, R., H\u00e4hnle, R., Heydari\u00a0Tabar, A.: A Program Logic For Dependence Analysis. In: W.\u00a0Ahrendt, S.L.T. Tarifa (eds.) Proc. 15th Intern. Conf on Integrated Formal Methods (IFM), LNCS. Springer (2019). To appear","DOI":"10.1007\/978-3-030-34968-4_5"},{"key":"9692_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/j.entcs.2007.11.015","volume":"199","author":"R Bubel","year":"2008","unstructured":"Bubel, R., Roth, A., R\u00fcmmer, P.: Ensuring the Correctness of Lightweight Tactics for JavaCard Dynamic Logic. Electr. Notes Theor. Comput. Sci. 199, 107\u2013128 (2008). https:\/\/doi.org\/10.1016\/j.entcs.2007.11.015","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9692_CR15","unstructured":"Burstall, R.M.: Program proving as hand simulation with a little induction. In: Information Processing \u201974, pp. 308\u2013312. Elsevier\/North-Holland (1974)"},{"key":"9692_CR16","unstructured":"Chen, T.Y., Cheung, S.C., Yiu, S.: Metamorphic Testing: A New Approach for Generating Next Test Cases. CoRR abs\/2002.12543 (2020). arxiv:2002.12543"},{"key":"9692_CR17","doi-asserted-by":"crossref","unstructured":"Daniel, B., Dig, D., Garcia, K., Marinov, D.: Automated Testing of Refactoring Engines. In: 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 185\u2013194 (2007)","DOI":"10.1145\/1287624.1287651"},{"key":"9692_CR18","doi-asserted-by":"crossref","unstructured":"Dannenberg, R., Ernst, G.: Formal Program Verification Using Symbolic Execution. IEEE Transactions on Software Engineering SE\u20138(1), 43\u201352 (1982)","DOI":"10.1109\/TSE.1982.234773"},{"key":"9692_CR19","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"9692_CR20","doi-asserted-by":"publisher","unstructured":"Eilertsen, A.M., Bagge, A.H., Stolz, V.: Safer Refactorings. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I, LNCS, vol. 9952, pp. 517\u2013531 (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_36","DOI":"10.1007\/978-3-319-47166-2_36"},{"key":"9692_CR21","volume-title":"Refactoring: Improving the Design of Existing Code","author":"M Fowler","year":"1999","unstructured":"Fowler, M.: Refactoring: Improving the Design of Existing Code. Addison-Wesley, Object Technology Series (1999)"},{"key":"9692_CR22","unstructured":"Fowler, M.: Refactoring: Improving the Design of Existing Code. Addison-Wesley Signature Series. Addison-Wesley Professional (2018). 2nd edition"},{"key":"9692_CR23","doi-asserted-by":"publisher","unstructured":"Futamura, Y.: Partial computation of programs. In: E.\u00a0Goto, K.\u00a0Furukawa, R.\u00a0Nakajima, I.\u00a0Nakata, A.\u00a0Yonezawa (eds.) RIMS Symposium on Software Science and Engineering, Kyoto, Japan, LNCS, vol. 147, pp. 1\u201335. Springer (1982).https:\/\/doi.org\/10.1007\/3-540-11980-9_13","DOI":"10.1007\/3-540-11980-9_13"},{"key":"9692_CR24","doi-asserted-by":"publisher","unstructured":"Garrido, A., Meseguer, J.: Formal Specification and Verification of Java Refactorings. In: Proc. 6th SCAM, pp. 165\u2013174. IEEE Computer Society, Washington, DC, USA (2006).https:\/\/doi.org\/10.1109\/SCAM.2006.16","DOI":"10.1109\/SCAM.2006.16"},{"key":"9692_CR25","unstructured":"Godefroid, P.: Test Generation using Symbolic Execution. In: LIPIcs-Leibniz International Proceedings in Informatics, vol.\u00a018, pp. 24\u201333. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2012). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2012\/3845\/"},{"key":"9692_CR26","doi-asserted-by":"publisher","unstructured":"Godlin, B., Strichman, O.: Regression Verification: Proving the Equivalence of Similar Programs. Softw. Test., Verif. Reliab. 23(3), 241\u2013258 (2013). https:\/\/doi.org\/10.1002\/stvr.1472","DOI":"10.1002\/stvr.1472"},{"key":"9692_CR27","doi-asserted-by":"publisher","unstructured":"Gopinath, R., Kampmann, A., Havrikov, N., Soremekun, E.O., Zeller, A.: Abstracting failure-inducing inputs. In: S.\u00a0Khurshid, C.S. Pasareanu (eds.) ISSTA \u201920: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, USA, July 18-22, 2020, pp. 237\u2013248. ACM (2020). https:\/\/doi.org\/10.1145\/3395363.3397349","DOI":"10.1145\/3395363.3397349"},{"key":"9692_CR28","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java (TM) Language Specification, 3rd edn. Addison-Wesley Professional (2005)"},{"key":"9692_CR29","doi-asserted-by":"crossref","unstructured":"Gries, D.: The Science of Programming. Texts and Monographs in Computer Science. Springer (1981)","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"9692_CR30","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. In: B.\u00a0Steffen, G.J. Woeginger (eds.) Computing and Software Science - State of the Art and Perspectives, LNCS, vol. 10000, pp. 345\u2013373. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"9692_CR31","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Schaefer, I.: A liskov principle for delta-oriented programming. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, LNCS, vol. 7609, pp. 32\u201346. Springer, Berlin, Heidelberg (2012).https:\/\/doi.org\/10.1007\/978-3-642-34026-0_4","DOI":"10.1007\/978-3-642-34026-0_4"},{"key":"9692_CR32","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: M.P. Bonacina (ed.) Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, LNCS, vol. 7898, pp. 300\u2013314. Springer (2013).https:\/\/doi.org\/10.1007\/978-3-642-38574-2_21","DOI":"10.1007\/978-3-642-38574-2_21"},{"key":"9692_CR33","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Tabar, A.H., Mazaheri, A., Norouzi, M., Steinh\u00f6fel, D., Wolf, F.: Safer Parallelization. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Proc. 9th Intern. Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles (Part II), LNCS, vol. 12477, pp. 117\u2013137. Springer (2020).https:\/\/doi.org\/10.1007\/978-3-030-61470-6_8","DOI":"10.1007\/978-3-030-61470-6_8"},{"issue":"10","key":"9692_CR34","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. Communications of the ACM 12(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"9692_CR35","doi-asserted-by":"publisher","unstructured":"Huda, Z.U., Jannesari, A., Wolf, F.: Using Template Matching to Infer Parallel Design Patterns. TACO 11(4), 64:1-64:21 (2015).https:\/\/doi.org\/10.1145\/2688905","DOI":"10.1145\/2688905"},{"key":"9692_CR36","unstructured":"Jackson, D.: Software Abstractions - Logic, Language, and Analysis. MIT Press (2006). http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=10928"},{"key":"9692_CR37","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: M.G. Bobaru, K.\u00a0Havelund, G.J. Holzmann, R.\u00a0Joshi (eds.) Proc. 3rd Intern. Symp. NASA Formal Methods (NFM), LNCS, vol. 6617, pp. 41\u201355. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"issue":"1","key":"9692_CR38","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0304-3975(91)90301-H","volume":"90","author":"ND Jones","year":"1991","unstructured":"Jones, N.D.: Static semantics, types, and binding time analysis. Theor. Comput. Sci. 90(1), 95\u2013118 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90301-H","journal-title":"Theor. Comput. Sci."},{"key":"9692_CR39","doi-asserted-by":"publisher","unstructured":"Kampmann, A., Havrikov, N., Soremekun, E.O., Zeller, A.: When Does My Program Do This? Learning Circumstances of Software Behavior. In: P.\u00a0Devanbu, M.B. Cohen, T.\u00a0Zimmermann (eds.) ESEC\/FSE \u201920: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020, pp. 1228\u20131239. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409687","DOI":"10.1145\/3368089.3409687"},{"issue":"3","key":"9692_CR40","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The Dynamic Frames Theory. Formal Asp. Comput. 23(3), 267\u2013288 (2011). https:\/\/doi.org\/10.1007\/s00165-010-0152-5","journal-title":"Formal Asp. Comput."},{"issue":"7","key":"9692_CR41","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385\u2013394 (1976)","journal-title":"Communications of the ACM"},{"issue":"4","key":"9692_CR42","first-page":"619","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A Machine-Checked Model for a Java-like Language, Virtual Machine, and Compiler. ACM Trans. PLS 28(4), 619\u2013695 (2006)","journal-title":"ACM Trans. PLS"},{"key":"9692_CR43","doi-asserted-by":"publisher","unstructured":"Kn\u00fcppel, A., Kr\u00fcger, S., Th\u00fcm, T., Bubel, R., Krieter, S., Bodden, E., Schaefer, I.: Using Abstract Contracts for Verifying Evolving Features and Their Interactions, LNCS, vol. 12345, pp. 122\u2013148. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_5","DOI":"10.1007\/978-3-030-64354-6_5"},{"key":"9692_CR44","doi-asserted-by":"publisher","unstructured":"Kn\u00fcppel, A., Runge, T., Schaefer, I.: Scaling correctness-by-construction. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles: 9th Intl. Symp. on Leveraging Applications of Formal Methods, ISoLA, Rhodes, Greece, Part I, LNCS, vol. 12476, pp. 187\u2013207. Springer, Cham (2020).https:\/\/doi.org\/10.1007\/978-3-030-61362-4_10","DOI":"10.1007\/978-3-030-61362-4_10"},{"key":"9692_CR45","doi-asserted-by":"publisher","unstructured":"Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Berlin Heidelberg (2012).https:\/\/doi.org\/10.1007\/978-3-642-27919-5","DOI":"10.1007\/978-3-642-27919-5"},{"key":"9692_CR46","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving Optimizations Correct Using Parameterized Program Equivalence. In: Proc. PLDI 2009, pp. 327\u2013337 (2009)","DOI":"10.1145\/1543135.1542513"},{"key":"9692_CR47","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML Reference Manual (2013). http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/\/OldReleases\/jmlrefman.pdf. Draft revision 2344"},{"issue":"7","key":"9692_CR48","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. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"6","key":"9692_CR49","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994). https:\/\/doi.org\/10.1145\/197320.197383","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"9692_CR50","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/3166064","volume":"61","author":"NP Lopes","year":"2018","unstructured":"Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Practical Verification of Peephole Optimizations with Alive. Commun. ACM 61(2), 84\u201391 (2018)","journal-title":"Commun. ACM"},{"issue":"2","key":"9692_CR51","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/s100090100045","volume":"3","author":"BL Massingill","year":"2001","unstructured":"Massingill, B.L., Mattson, T.G., Sanders, B.A.: Parallel Programming with a Pattern Language. Int. J. Softw. Tools Technol. Transf. 3(2), 217\u2013234 (2001). https:\/\/doi.org\/10.1007\/s100090100045","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9692_CR52","unstructured":"Mazaheri, A., Norouzi, M., Olokin, K., Wolf, F.: Enhancing parallel pattern identification through code-restructuring. Tech. rep., Technical University of Darmstadt, Department of Computer Science, Laboratory for Parallel Programming (2020)"},{"key":"9692_CR53","doi-asserted-by":"crossref","unstructured":"McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: P.\u00a0Braffort, D.\u00a0Hirschberg (eds.) Computer Programming and Formal Systems, pp. 33\u201369. North Holland (1963)","DOI":"10.1016\/S0049-237X(08)72018-4"},{"key":"9692_CR54","doi-asserted-by":"crossref","unstructured":"Mechtaev, S., Griggio, A., Cimatti, A., Roychoudhury, A.: Symbolic Execution with Existential Second-Order Constraints. In: Proc. 2018 Joint Meeting on European Software Engineering Conf. and Symp. on the Foundations of Software Engineering, pp. 389\u2013399 (2018)","DOI":"10.1145\/3236024.3236049"},{"key":"9692_CR55","doi-asserted-by":"publisher","unstructured":"Meseguer, J., Winkler, T.C.: Parallel Programmming in Maude. In: J.\u00a0Ban\u00e2tre, D.L. M\u00e9tayer (eds.) Research Directions in High-Level Parallel Programming Languages, LNCS, vol. 574, pp. 253\u2013293. Springer (1991). https:\/\/doi.org\/10.1007\/3-540-55160-3_49","DOI":"10.1007\/3-540-55160-3_49"},{"key":"9692_CR56","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: A.\u00a0Platzer, G.\u00a0Sutcliffe (eds.) CADE, 28th Intl. Conf. on Automated Deduction, LNCS, vol. 12699, pp. 625\u2013635. Springer (2021).https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37","DOI":"10.1007\/978-3-030-79876-5_37"},{"issue":"4","key":"9692_CR57","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1109\/MS.2006.105","volume":"23","author":"GC Murphy","year":"2006","unstructured":"Murphy, G.C., Kersten, M., Findlater, L.: How Are Java Software Developers Using the Eclipse IDE? IEEE Software 23(4), 76\u201383 (2006). https:\/\/doi.org\/10.1109\/MS.2006.105","journal-title":"IEEE Software"},{"key":"9692_CR58","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S., Zuck, L.D.: Witnessing Program Transformations. In: F.\u00a0Logozzo, M.\u00a0F\u00e4hndrich (eds.) 20th International Symposium on Static Analysis (SAS), LNCS, vol. 7935, pp. 304\u2013323. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_17","DOI":"10.1007\/978-3-642-38856-9_17"},{"key":"9692_CR59","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002). doihttps:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9692_CR60","doi-asserted-by":"publisher","unstructured":"Norouzi, M., Wolf, F., Jannesari, A.: Automatic construct selection and variable classification in OpenMP. In: Proc. of the International Conference on Supercomputing (ICS), Phoenix, AZ, USA, pp. 330\u2013341. ACM (2019). https:\/\/doi.org\/10.1145\/3330345.3330375","DOI":"10.1145\/3330345.3330375"},{"issue":"2","key":"9692_CR61","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: A Complete Uniform Substitution Calculus for Differential Dynamic Logic. J. Autom. Reason. 59(2), 219\u2013265 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J. Autom. Reason."},{"key":"9692_CR62","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-28901-1","author":"K Pohl","year":"2005","unstructured":"Pohl, K., B\u00f6ckle, G., van der Linden, F.: Software Product Line Engineering - Foundations, Principles, and Techniques. Springer (2005). https:\/\/doi.org\/10.1007\/3-540-28901-1","journal-title":"Springer"},{"key":"9692_CR63","doi-asserted-by":"publisher","unstructured":"Qu, W., Gaboardi, M., Garg, D.: Relational Cost Analysis for Functional-Imperative Programs. Proc. ACM Program. Lang. 3(ICFP), 92:1-92:29 (2019). https:\/\/doi.org\/10.1145\/3341696","DOI":"10.1145\/3341696"},{"key":"9692_CR64","doi-asserted-by":"publisher","unstructured":"Radicek, I., Barthe, G., Gaboardi, M., Garg, D., Zuleger, F.: Monadic Refinements for Relational Cost Analysis. Proc. ACM Program. Lang. 2(POPL), 36:1-36:32 (2018). https:\/\/doi.org\/10.1145\/3158124","DOI":"10.1145\/3158124"},{"key":"9692_CR65","doi-asserted-by":"publisher","unstructured":"R\u00fcmmer, P., Ulbrich, M.: Proof Search with Taclets. In: W.\u00a0Ahrendt, B.\u00a0Beckert, R.\u00a0Bubel, R.\u00a0H\u00e4hnle, P.H. Schmitt, M.\u00a0Ulbrich (eds.) Deductive Software Verification - The KeY Book - From Theory to Practice, LNCS, vol. 10001, pp. 107\u2013147. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_4","DOI":"10.1007\/978-3-319-49812-6_4"},{"key":"9692_CR66","doi-asserted-by":"crossref","unstructured":"Scaletta, M., H\u00e4hnle, R., Steinh\u00f6fel, D., Bubel, R.: Delta-based verification of software product families. In: C.\u00a0De\u00a0Roever (ed.) Proc. 20th Intl. Conf. on Generative Programming (GPCE). ACM Press, New York, NY, USA (2021)","DOI":"10.1145\/3486609.3487200"},{"key":"9692_CR67","doi-asserted-by":"publisher","unstructured":"Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: J.\u00a0Bosch, J.\u00a0Lee (eds.) Software Product Lines: Going Beyond, LNCS, vol. 6287, pp. 77\u201391. Springer, Berlin, Heidelberg (2010).https:\/\/doi.org\/10.1007\/978-3-642-15579-6_6","DOI":"10.1007\/978-3-642-15579-6_6"},{"issue":"6","key":"9692_CR68","doi-asserted-by":"publisher","first-page":"1233","DOI":"10.1109\/TSE.2012.13","volume":"38","author":"M Sch\u00e4fer","year":"2012","unstructured":"Sch\u00e4fer, M., Thies, A., Steimann, F., Tip, F.: A Comprehensive Approach to Naming and Accessibility in Refactoring Java Programs. IEEE Trans. Software Eng. 38(6), 1233\u20131257 (2012). https:\/\/doi.org\/10.1109\/TSE.2012.13","journal-title":"IEEE Trans. Software Eng."},{"key":"9692_CR69","doi-asserted-by":"crossref","unstructured":"Schmitt, P.H., Ulbrich, M., Wei\u00df, B.: Dynamic Frames in Java Dynamic Logic. In: B.\u00a0Beckert, C.\u00a0March\u00e9 (eds.) Intl. Conf. on Formal Verification of Object-Oriented Software (FoVeOOS), LNCS, vol. 6528, pp. 138\u2013152. Springer (2011)","DOI":"10.1007\/978-3-642-18070-5_10"},{"issue":"4","key":"9692_CR70","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1145\/778559.778561","volume":"25","author":"UP Schultz","year":"2003","unstructured":"Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for Java. ACM Trans. Program. Lang. Syst. 25(4), 452\u2013499 (2003). https:\/\/doi.org\/10.1145\/778559.778561","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9692_CR71","doi-asserted-by":"publisher","unstructured":"da\u00a0Silva, T.D., Sampaio, A., Mota, A.: Verifying Transformations of Java Programs Using Alloy. In: M.\u00a0Corn\u00e9lio, B.\u00a0Roscoe (eds.) 18th Brazilian Symposium on Formal Methods: Foundations and Applications (SBMF), LNCS, vol. 9526, pp. 110\u2013126. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-29473-5_7","DOI":"10.1007\/978-3-319-29473-5_7"},{"key":"9692_CR72","doi-asserted-by":"publisher","unstructured":"Soares, G., Catao, B., Varjao, C., Aguiar, S., Gheyi, R., Massoni, T.: Analyzing Refactorings on Software Repositories. In: 25th Brazilian Symposium on Software Engineering (SBES), pp. 164\u2013173. IEEE Computer Society (2011).https:\/\/doi.org\/10.1109\/SBES.2011.21","DOI":"10.1109\/SBES.2011.21"},{"issue":"2","key":"9692_CR73","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1109\/TSE.2012.19","volume":"39","author":"G Soares","year":"2013","unstructured":"Soares, G., Gheyi, R., Massoni, T.: Automated Behavioral Testing of Refactoring Engines. IEEE Trans. Software Eng. 39(2), 147\u2013162 (2013). https:\/\/doi.org\/10.1109\/TSE.2012.19","journal-title":"IEEE Trans. Software Eng."},{"issue":"4","key":"9692_CR74","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 Software 27(4), 52\u201357 (2010). https:\/\/doi.org\/10.1109\/MS.2010.63","journal-title":"IEEE Software"},{"key":"9692_CR75","doi-asserted-by":"publisher","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: From Program Verification to Program Synthesis. In: Proc. 37th POPL, pp. 313\u2013326 (2010). https:\/\/doi.org\/10.1145\/1706299.1706337","DOI":"10.1145\/1706299.1706337"},{"key":"9692_CR76","doi-asserted-by":"publisher","unstructured":"Steinh\u00f6fel, D.: Abstract Execution: Automatically Proving Infinitely Many Programs. Ph.D. thesis, Technical University of Darmstadt, Department of Computer Science, Darmstadt, Germany (2020). https:\/\/doi.org\/10.25534\/tuprints-00008540.http:\/\/tuprints.ulb.tu-darmstadt.de\/8540\/","DOI":"10.25534\/tuprints-00008540."},{"key":"9692_CR77","doi-asserted-by":"publisher","unstructured":"Steinh\u00f6fel, D.: REFINITY to Model and Prove Program Transformation Rules. In: B.C. d.\u00a0S.\u00a0Oliveira (ed.) Proc. 18th Asian Symposium on Programming Languages and Systems (APLAS), LNCS, vol. 12470, pp. 311\u2013319. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_16","DOI":"10.1007\/978-3-030-64437-6_16"},{"key":"9692_CR78","doi-asserted-by":"crossref","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Modular, Correct Compilation with Automatic Soundness Proofs. In: T.\u00a0Margaria, B.\u00a0Steffen (eds.) Proc. 8th ISOLA, LNCS (2018)","DOI":"10.1007\/978-3-030-03418-4_25"},{"key":"9692_CR79","doi-asserted-by":"publisher","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Abstract Execution. In: Proc. Third World Congress on Formal Methods - The Next 30 Years, (FM), pp. 319\u2013336 (2019).https:\/\/doi.org\/10.1007\/978-3-030-30942-8_20","DOI":"10.1007\/978-3-030-30942-8_20"},{"key":"9692_CR80","doi-asserted-by":"publisher","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: The Trace Modality. In: L.S. Barbosa, A.\u00a0Baltag (eds.) Dynamic Logic. New Trends and Applications - Second International Workshop (DaLi), LNCS, vol. 12005, pp. 124\u2013140. Springer (2019).https:\/\/doi.org\/10.1007\/978-3-030-38808-9_8","DOI":"10.1007\/978-3-030-38808-9_8"},{"key":"9692_CR81","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A., Owens, S., Norrish, M.: A New Verified Compiler Backend for CakeML. In: Proc. 21st ICFP, pp. 60\u201373. ACM (2016).https:\/\/doi.org\/10.1145\/2951913.2951924","DOI":"10.1145\/2951913.2951924"},{"key":"9692_CR82","doi-asserted-by":"publisher","unstructured":"The Coq Development Team: The Coq Proof Assistant, version 8.10.0 (2019). https:\/\/doi.org\/10.5281\/zenodo.3476303","DOI":"10.5281\/zenodo.3476303"},{"key":"9692_CR83","doi-asserted-by":"publisher","unstructured":"Th\u00fcm, T., Apel, S., K\u00e4stner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6:1-6:45 (2014). https:\/\/doi.org\/10.1145\/2580950","DOI":"10.1145\/2580950"},{"key":"9692_CR84","doi-asserted-by":"publisher","unstructured":"Th\u00fcm, T., Kn\u00fcppel, A., Kr\u00fcger, S., Bolle, S., Schaefer, I.: Feature-oriented contract composition. In: Proc. 23rd Intl. Systems and Software Product Line Conference - Volume A, p.\u00a025. ACM, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3336294.3342374","DOI":"10.1145\/3336294.3342374"},{"issue":"3","key":"9692_CR85","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/2480361.2371404","volume":"48","author":"T Th\u00fcm","year":"2012","unstructured":"Th\u00fcm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. SIGPLAN Not. 48(3), 11\u201320 (2012). https:\/\/doi.org\/10.1145\/2480361.2371404","journal-title":"SIGPLAN Not."},{"key":"9692_CR86","doi-asserted-by":"publisher","unstructured":"Th\u00fcm, T., Schaefer, I., Kuhlemann, M., Apel, S.: Proof composition for deductive verification of software product lines. In: Fourth IEEE Intl. Conf. on Software Testing, Verification and Validation, ICST, Berlin, Germany, pp. 270\u2013277. IEEE Computer Society, Los Alamitos, CA (2011). https:\/\/doi.org\/10.1109\/ICSTW.2011.48","DOI":"10.1109\/ICSTW.2011.48"},{"key":"9692_CR87","unstructured":"Vermeer, B.: IntelliJ IDEA dominates the IDE market with 62% adoption among JVM developers (2020). https:\/\/snyk.io\/blog\/intellij-idea-dominates-the-ide-market. Last accessed: 2021\/06\/16"},{"key":"9692_CR88","unstructured":"Wei\u00df, B.: Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. Ph.D. thesis, Karlsruhe Institute of Technology, Karlsruhe (2011)"},{"key":"9692_CR89","unstructured":"Winterland, D.: Abstract execution for correctness-by-construction. Master\u2019s thesis, Technische Universit\u00e4t Braunschweig, Institute of Software Engineering and Automotive Informatics (2020). https:\/\/www.tu-braunschweig.de\/isf\/team\/runge"},{"issue":"4","key":"9692_CR90","first-page":"221","volume":"14","author":"N Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. CACM 14(4), 221\u2013227 (1971)","journal-title":"Program development by stepwise refinement. CACM"},{"key":"9692_CR91","doi-asserted-by":"publisher","unstructured":"Yang, G., Filieri, A., Borges, M., Clun, D., Wen, J.: Advances in Symbolic Execution. In: A.M. Memon (ed.) Advances in Computers, Advances in Computers, vol. 113, pp. 225 \u2013 287. Elsevier (2019). https:\/\/doi.org\/10.1016\/bs.adcom.2018.10.002. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0065245818300627","DOI":"10.1016\/bs.adcom.2018.10.002"},{"key":"9692_CR92","doi-asserted-by":"publisher","unstructured":"Zeller, A.: Yesterday, My Program Worked. Today, It Does Not. Why? In: O.\u00a0Nierstrasz, M.\u00a0Lemoine (eds.) Software Engineering - ESEC\/FSE\u201999, 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering, Toulouse, France, September 1999, Proceedings, Lecture Notes in Computer Science, vol. 1687, pp. 253\u2013267. Springer (1999). https:\/\/doi.org\/10.1007\/3-540-48166-4_16","DOI":"10.1007\/3-540-48166-4_16"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09692-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09692-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09692-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,4]],"date-time":"2024-10-04T10:23:56Z","timestamp":1728037436000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09692-0"}},"subtitle":["Theory and Applications"],"short-title":[],"issued":{"date-parts":[[2024,3,26]]},"references-count":92,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["9692"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09692-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2024,3,26]]},"assertion":[{"value":"11 January 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 December 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 March 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"7"}}