{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T04:13:11Z","timestamp":1748405591424,"version":"3.41.0"},"publisher-location":"Cham","reference-count":72,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031921957","type":"print"},{"value":"9783031921964","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-92196-4_15","type":"book-chapter","created":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:23:18Z","timestamp":1748348598000},"page":"303-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Automatic Structured Inference of\u00a0Module Abstractions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3289-5764","authenticated-orcid":false,"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8172-3184","authenticated-orcid":false,"given":"Marian","family":"Lingsch-Rosenfeld","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,28]]},"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, LNCS, vol. 10001. Springer (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":"Albarghouthi, A., Dillig, I., Gurfinkel, A.: Maximal specification synthesis. In: POPL, pp. 789\u2013801. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837628","DOI":"10.1145\/2837614.2837628"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-guided synthesis. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"issue":"2104","key":"15_CR4","doi-asserted-by":"publisher","first-page":"20160331","DOI":"10.1098\/rsta.2016.0331","volume":"375","author":"AW Appel","year":"2017","unstructured":"Appel, A.W., et al.: Position paper: the science of deep specification. Philos. Trans. R. Soc. A Math. Phys. Eng. Sci. 375(2104), 20160331 (2017). https:\/\/doi.org\/10.1098\/rsta.2016.0331","journal-title":"Philos. Trans. R. Soc. A Math. Phys. Eng. Sci."},{"issue":"2","key":"15_CR5","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0304-3975(01)00368-1","volume":"286","author":"E Astesiano","year":"2002","unstructured":"Astesiano, E., et al.: CASL: the common algebraic specification language. Theoret. Comput. Sci. 286(2), 153\u2013196 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00368-1","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR6","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et\u00a0al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification\u2013specification is the new bottleneck. In: SSV. EPTCS, vol.\u00a0102, pp. 18\u201332. Elsevier (2012). https:\/\/doi.org\/10.4204\/EPTCS.102.4","DOI":"10.4204\/EPTCS.102.4"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq\u2019Art: Interactive theorem proving and program development. In: Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"15_CR9","first-page":"83","volume":"99","author":"M Bidoit","year":"1999","unstructured":"Bidoit, M., Hennicker, R.: Observer complete definitions are behaviourally coherent. OBJ\/CafeOBJ\/Maude Formal Methods 99, 83\u201394 (1999)","journal-title":"OBJ\/CafeOBJ\/Maude Formal Methods"},{"issue":"2","key":"15_CR10","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1093\/COMJNL\/32.2.122","volume":"32","author":"RS Bird","year":"1989","unstructured":"Bird, R.S.: Algebraic identities for program calculation. Comput. J. 32(2), 122\u2013126 (1989). https:\/\/doi.org\/10.1093\/COMJNL\/32.2.122","journal-title":"Comput. J."},{"key":"15_CR11","doi-asserted-by":"publisher","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: IFM, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Bodenm\u00fcller, S., Schellhorn, G., Bitterlich, M., Reif, W.: Flashix: modular verification of a concurrent and crash-safe flash file system. Logic, Computation and Rigorous Methods: Essays Dedicated to Egon B\u00f6rger on the Occasion of His 75th Birthday, pp. 239\u2013265 (2021)","DOI":"10.1007\/978-3-030-76020-5_14"},{"key":"15_CR13","doi-asserted-by":"publisher","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: VMCAI, pp. 70\u201387. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7","DOI":"10.1007\/978-3-642-18275-4_7"},{"issue":"4","key":"15_CR14","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/J.JAL.2005.10.006","volume":"4","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Log. 4(4), 470\u2013504 (2006). https:\/\/doi.org\/10.1016\/J.JAL.2005.10.006","journal-title":"J. Appl. Log."},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., Van Harmelen, F., Ireland, A., Smaill, A.: Rippling: a heuristic for guiding inductive proofs. Artif. Intell. 62(2), 185\u2013253 (1993). https:\/\/doi.org\/10.1016\/0004-3702(93)90079-Q","journal-title":"Artif. Intell."},{"issue":"1","key":"15_CR16","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/321992.321996","volume":"24","author":"RM Burstall","year":"1977","unstructured":"Burstall, R.M., Darlington, J.: A transformation system for developing recursive programs. J. ACM 24(1), 44\u201367 (1977). https:\/\/doi.org\/10.1145\/321992.321996","journal-title":"J. ACM"},{"key":"15_CR17","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A.: Software model checking via IC3. In: CAV, pp. 277\u2013293. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_23","DOI":"10.1007\/978-3-642-31424-7_23"},{"key":"15_CR18","doi-asserted-by":"publisher","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: International Conference on Automated Deduction, pp. 392\u2013406. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27","DOI":"10.1007\/978-3-642-38574-2_27"},{"issue":"2","key":"15_CR19","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M Clavel","year":"2002","unstructured":"Clavel, M., et al.: Maude: specification and programming in rewriting logic. Theor. Comput. Sci. 285(2), 187\u2013243 (2002). https:\/\/doi.org\/10.1016\/S0304-3975(01)00359-0","journal-title":"Theor. Comput. Sci."},{"key":"15_CR20","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"15_CR21","doi-asserted-by":"publisher","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"issue":"1\u20132","key":"15_CR22","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R De Nicola","year":"1984","unstructured":"De Nicola, R., Hennessy, M.C.: Testing equivalences for processes. Theoret. Comput. Sci. 34(1\u20132), 83\u2013133 (1984). https:\/\/doi.org\/10.1016\/0304-3975(84)90113-0","journal-title":"Theoret. Comput. Sci."},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"De\u00a0Roever, W.P., Engelhardt, K., Buth, K.H.: Data Refinement: Model-Oriented Proof Methods and Their Comparison, vol.\u00a047. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"issue":"6","key":"15_CR24","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV\u2013overview and verify this competition. Softw. Tools Technol. Transfer (STTT) 17(6), 677\u2013694 (2015)","journal-title":"Softw. Tools Technol. Transfer (STTT)"},{"key":"15_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2016.04.009","volume":"131","author":"G Ernst","year":"2016","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Reif, W.: Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. (SCP) 131, 3\u201321 (2016)","journal-title":"Sci. Comput. Program. (SCP)"},{"key":"15_CR26","unstructured":"Ernst, G., Fedyukovich, G., S\u00f6gtrop, R.: Quick theory exploration for algebraic data types via program transformations (2023). https:\/\/www.sosy-lab.org\/research\/pub\/2023-Draft.LemmaCalc.pdf"},{"key":"15_CR27","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3\u2014where programs meet provers. In: ESOP, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"15_CR28","doi-asserted-by":"publisher","unstructured":"Garavel, H., Beek, M.H.t., Pol, J.v.d.: The 2020 expert survey on formal methods. In: FMICS, pp. 3\u201369. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"15_CR29","doi-asserted-by":"publisher","unstructured":"Giesl, J.: Context-moving transformations for function verification. In: LOPSTR, pp. 293\u2013312. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/10720327_17","DOI":"10.1007\/10720327_17"},{"issue":"2","key":"15_CR30","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/J.JLAP.2006.11.001","volume":"71","author":"J Giesl","year":"2007","unstructured":"Giesl, J., K\u00fchnemann, A., Voigtl\u00e4nder, J.: Deaccumulation techniques for improving provability. J. Logic Algebraic Program. 71(2), 79\u2013113 (2007). https:\/\/doi.org\/10.1016\/J.JLAP.2006.11.001","journal-title":"J. Logic Algebraic Program."},{"issue":"6","key":"15_CR31","doi-asserted-by":"publisher","first-page":"4473","DOI":"10.1007\/S10664-020-09836-5","volume":"25","author":"M Gleirscher","year":"2020","unstructured":"Gleirscher, M., Marmsoler, D.: Formal methods in dependable systems engineering: a survey of professionals from Europe and North America. Empir. Softw. Eng. 25(6), 4473\u20134546 (2020). https:\/\/doi.org\/10.1007\/S10664-020-09836-5","journal-title":"Empir. Softw. Eng."},{"key":"15_CR32","unstructured":"Goguen, J.: Hidden algebra for software engineering. In: Proceedings Conference on Discrete Mathematics and Theoretical Computer Science, Auckland, New Zealand, pp. 35\u201359. Citeseer (1999)"},{"key":"15_CR33","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. Computing and Software Science: State of the Art and Perspectives pp. 345\u2013373 (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"15_CR34","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012). https:\/\/doi.org\/10.1145\/2187671.2187678","DOI":"10.1145\/2187671.2187678"},{"issue":"3","key":"15_CR35","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BF01178505","volume":"28","author":"R Hennicker","year":"1991","unstructured":"Hennicker, R.: Observational implementation of algebraic specifications. Acta Informatica 28(3), 187\u2013230 (1991). https:\/\/doi.org\/10.1007\/BF01178505","journal-title":"Acta Informatica"},{"key":"15_CR36","doi-asserted-by":"publisher","unstructured":"Hennicker, R., Bidoit, M.: Observational logic. In: AMAST, pp. 263\u2013277. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49253-4_20","DOI":"10.1007\/3-540-49253-4_20"},{"key":"15_CR37","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"P Hoare","year":"1972","unstructured":"Hoare, P.: Proof of correctness of data representations. Acta Informatica 1, 271\u2013281 (1972). https:\/\/doi.org\/10.1007\/BF00289507","journal-title":"Acta Informatica"},{"key":"15_CR38","doi-asserted-by":"publisher","unstructured":"Hutter, D., Sengler, C.: INKA: the next generation. In: CADE. LNCS, vol.\u00a01104, pp. 288\u2013292. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_92","DOI":"10.1007\/3-540-61511-3_92"},{"key":"15_CR39","doi-asserted-by":"publisher","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Case-analysis for rippling and inductive proof. In: Interactive Theorem Proving, pp. 291\u2013306. Springer, HeidelbergD (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_21","DOI":"10.1007\/978-3-642-14052-5_21"},{"issue":"1","key":"15_CR40","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G.: Comprehensive formal verification of an OS microkernel. TOCS 32(1), 1\u201370 (2014). https:\/\/doi.org\/10.1145\/2560537","journal-title":"TOCS"},{"key":"15_CR41","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: CAV, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"15_CR42","doi-asserted-by":"publisher","unstructured":"Kurashige, C., et al.: CCLemma: e-graph guided lemma discovery for inductive equational proofs. Proc. ACM Program. Lang. 8(ICFP), 818\u2013844 (2024). https:\/\/doi.org\/10.1145\/3674653","DOI":"10.1145\/3674653"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"issue":"7","key":"15_CR44","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). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"15_CR45","unstructured":"Liskov, B., Guttag, J., et\u00a0al.: Abstraction and Specification in Program Development, vol.\u00a020. MIT Press Cambridge (1986)"},{"issue":"2","key":"15_CR46","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/INCO.1995.1134","volume":"121","author":"N Lynch","year":"1995","unstructured":"Lynch, N., Vaandrager, F.: Forward and backward simulations. Inf. Comput. 121(2), 214\u2013233 (1995). https:\/\/doi.org\/10.1006\/INCO.1995.1134","journal-title":"Inf. Comput."},{"key":"15_CR47","doi-asserted-by":"publisher","unstructured":"Meijer, E., Fokkinga, M.M., Paterson, R.: Functional programming with bananas, lenses, envelopes and barbed wire. In: FPCA, vol.\u00a091, pp. 124\u2013144 (1991). https:\/\/doi.org\/10.1007\/3540543961_7","DOI":"10.1007\/3540543961_7"},{"key":"15_CR48","doi-asserted-by":"publisher","unstructured":"Miltner, A., Padhi, S., Millstein, T., Walker, D.: Data-driven inference of representation invariants. In: PLDI, pp. 1\u201315 (2020). https:\/\/doi.org\/10.1145\/3385412.3385967","DOI":"10.1145\/3385412.3385967"},{"key":"15_CR49","doi-asserted-by":"publisher","unstructured":"de\u00a0Moor, O., Sittampalam, G.: Generic program transformation. In: Advanced Functional Programming. LNCS, vol.\u00a01608, pp. 116\u2013149. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/10704973_3","DOI":"10.1007\/10704973_3"},{"key":"15_CR50","doi-asserted-by":"publisher","unstructured":"Moura, L.D., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"15_CR51","doi-asserted-by":"publisher","unstructured":"Nandi, C., et al.: Rewrite rule inference using equality saturation. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201328 (2021). https:\/\/doi.org\/10.1145\/3485496","DOI":"10.1145\/3485496"},{"key":"15_CR52","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"15_CR53","doi-asserted-by":"publisher","unstructured":"Orejas, F., Nivela, P.: Constraints for behavioural specifications. In: ADT. LNCS, vol.\u00a0534, pp. 220\u2013245. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-54496-8_12","DOI":"10.1007\/3-540-54496-8_12"},{"key":"15_CR54","doi-asserted-by":"publisher","unstructured":"Park, K., Peng, X., D\u2019Antoni, L.: LOUD: synthesizing strongest and weakest specifications. CoRR abs\/2408.12539 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2408.12539","DOI":"10.48550\/ARXIV.2408.12539"},{"key":"15_CR55","unstructured":"Reichel, H.: Behavioural equivalence-a unifying concept for initial and final specifications. In: Proceedings of Third Hungarian Computer Science Conference. Akademiai Kiado (1981)"},{"key":"15_CR56","doi-asserted-by":"publisher","unstructured":"Reif, W.: Correctness of generic modules. In: Logical Foundations of Computer Science-Tver 1992: Second International Symposium Tver, Russia, July 20\u201324, 1992 Proceedings 2, pp. 406\u2013417. Springer (1992). https:\/\/doi.org\/10.1007\/BFB0023893","DOI":"10.1007\/BFB0023893"},{"key":"15_CR57","doi-asserted-by":"publisher","unstructured":"Reif, W.: The KIV system: Systematic construction of verified software. In: CADE. Lecture Notes in Computer Science, vol.\u00a0607, pp. 753\u2013757. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_218","DOI":"10.1007\/3-540-55602-8_218"},{"key":"15_CR58","doi-asserted-by":"publisher","unstructured":"Reif, W.: The KIV-approach to software verification. KORSO: Methods, Languages, and Tools for the Construction of Correct Software: Final Report, pp. 339\u2013368 (2005). https:\/\/doi.org\/10.1007\/BFB0015471","DOI":"10.1007\/BFB0015471"},{"key":"15_CR59","doi-asserted-by":"publisher","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. Automated Deduction-A Basis for Applications: Volume II: Systems and Implementation Techniques, pp. 13\u201339 (1998). https:\/\/doi.org\/10.1007\/978-94-017-0435-9_1","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"15_CR60","doi-asserted-by":"publisher","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: VSTTE, pp. 8\u201326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2","DOI":"10.1007\/978-3-319-48869-1_2"},{"issue":"2\/3","key":"15_CR61","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1016\/0022-0000(87)90023-7","volume":"34","author":"D Sannella","year":"1987","unstructured":"Sannella, D., Tarlecki, A.: On observational equivalence and algebraic specification. J. Comput. Syst. Sci. 34(2\/3), 150\u2013178 (1987). https:\/\/doi.org\/10.1016\/0022-0000(87)90023-7","journal-title":"J. Comput. Syst. Sci."},{"key":"15_CR62","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Ernst, G., Pf\u00e4hler, J., Haneberg, D., Reif, W.: Development of a verified Flash file system. In: Proceedings of Alloy, ASM, B, TLA, VDM, and Z (ABZ). LNCS, vol.\u00a08477, pp. 9\u201324. Springer (2014), invited Paper","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"15_CR63","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Bitterlich, M., Reif, W.: Software & system verification with KIV. In: The Logic of Software. A Tasting Menu of Formal Methods: Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday, pp. 408\u2013436. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-08166-8_20","DOI":"10.1007\/978-3-031-08166-8_20"},{"key":"15_CR64","doi-asserted-by":"publisher","unstructured":"Schierl, A., Schellhorn, G., Haneberg, D., Reif, W.: Abstract specification of the ubifs file system for flash memory. In: FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2\u20136, 2009. Proceedings 2, pp. 190\u2013206. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_13","DOI":"10.1007\/978-3-642-05089-3_13"},{"key":"15_CR65","doi-asserted-by":"publisher","unstructured":"Singher, E., Itzhaky, S.: Theory exploration powered by deductive synthesis. In: CAV, pp. 125\u2013148. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_6","DOI":"10.1007\/978-3-030-81688-9_6"},{"key":"15_CR66","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000090","volume":"27","author":"N Smallbone","year":"2017","unstructured":"Smallbone, N., Johansson, M., Claessen, K., Algehed, M.: Quick specifications for the busy programmer. J. Funct. Program. 27, e18 (2017). https:\/\/doi.org\/10.1017\/S0956796817000090","journal-title":"J. Funct. Program."},{"key":"15_CR67","unstructured":"Sonnex, W.: Fixed point promotion: taking the induction out of automated induction, Tech. rep. University of Cambridge, Computer Laboratory (2017)"},{"key":"15_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-28756-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"W Sonnex","year":"2012","unstructured":"Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: an automated prover for properties of recursive data structures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 407\u2013421. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_28"},{"issue":"3","key":"15_CR69","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/5956.5957","volume":"8","author":"VF Turchin","year":"1986","unstructured":"Turchin, V.F.: The concept of a supercompiler. TOPLAS 8(3), 292\u2013325 (1986). https:\/\/doi.org\/10.1145\/5956.5957","journal-title":"TOPLAS"},{"key":"15_CR70","doi-asserted-by":"publisher","unstructured":"Wadler, P.: Deforestation: transforming programs to eliminate trees. In: ESOP. pp. 344\u2013358. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-19027-9_23","DOI":"10.1007\/3-540-19027-9_23"},{"key":"15_CR71","doi-asserted-by":"publisher","unstructured":"Wirsing, M.: Algebraic specification. Formal Models and Semantics, pp. 675\u2013788 (1990). https:\/\/doi.org\/10.1016\/B978-0-444-88074-1.50018-4","DOI":"10.1016\/B978-0-444-88074-1.50018-4"},{"issue":"4","key":"15_CR72","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 1\u201336 (2009). https:\/\/doi.org\/10.1145\/1592434.1592436","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Go Where the Bugs Are"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-92196-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:23:21Z","timestamp":1748348601000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-92196-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031921957","9783031921964"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-92196-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"28 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}