{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:52:17Z","timestamp":1767984737048,"version":"3.49.0"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032107930","type":"print"},{"value":"9783032107947","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,16]],"date-time":"2025-11-16T00:00:00Z","timestamp":1763251200000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-10794-7_21","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:30Z","timestamp":1763189010000},"page":"424-450","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Quick Theory Exploration for\u00a0Algebraic Data Types via\u00a0Program Transformations"],"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-0003-1727-4043","authenticated-orcid":false,"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., et al.: Syntax-Guided Synthesis. In: FMCAD, pp. 1\u201317. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Bird, R.S.: An introduction to the theory of lists. Springer (1987)","DOI":"10.1007\/978-3-642-87374-4_1"},{"issue":"2","key":"21_CR3","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)","journal-title":"Comput. J."},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Braquehais, R., Runciman, C.: FitSpec: refining property sets for functional testing. In: Proceedings of the 9th International Symposium on Haskell, pp. 1\u201312 (2016)","DOI":"10.1145\/2976002.2976003"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Braquehais, R., Runciman, C.: Speculate: discovering conditional equations and inequalities about black-box functions by reasoning from test results. In: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, pp. 40\u201351 (2017)","DOI":"10.1145\/3122955.3122961"},{"issue":"2","key":"21_CR6","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)","journal-title":"Artif. Intell."},{"issue":"1","key":"21_CR7","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 (JACM) 24(1), 44\u201367 (1977)","journal-title":"J. ACM (JACM)"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Chamarthi, H.R., Dillinger, P., Manolios, P., Vroon, D.: The ACL2 sedan theorem proving system. In: TACAS, pp. 291\u2013295. LNCS, Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_27"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"392","DOI":"10.1007\/978-3-642-38574-2_27","volume-title":"Automated Deduction \u2013 CADE-24","author":"K Claessen","year":"2013","unstructured":"Claessen, K., Johansson, M., Ros\u00e9n, D., Smallbone, N.: Automating inductive proofs using theory exploration. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 392\u2013406. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_27"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-030-51074-9_6","volume-title":"Automated Reasoning","author":"E De Angelis","year":"2020","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Removing algebraic data types from constrained horn clauses using difference predicates. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 83\u2013102. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_6"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Formal models and semantics, pp. 243\u2013320. Elsevier (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"21_CR12","doi-asserted-by":"publisher","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005). https:\/\/doi.org\/10.1145\/1066100.1066102","DOI":"10.1145\/1066100.1066102"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Einarsd\u00f3ttir, S.H., Smallbone, N., Johansson, M.: Template-based theory exploration: discovering properties of functional programs by testing. In: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages, pp. 67\u201378 (2020)","DOI":"10.1145\/3462172.3462192"},{"key":"21_CR14","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Ernst, G.: Bridging arrays and ADTs in recursive proofs. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12652, pp. 24\u201342. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_2","DOI":"10.1007\/978-3-030-72013-1_2"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Fedyukovich, G., Kaufman, S., Bod\u00edk, R.: Sampling invariants from frequency distributions. In: FMCAD, pp. 100\u2013107. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102247"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Giesl, J.: Context-moving transformations for function verification. In: LOPSTR, pp. 293\u2013312. Springer (1999)","DOI":"10.1007\/10720327_17"},{"issue":"2","key":"21_CR17","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)","journal-title":"J. Logic Algebraic Program."},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Gill, A., Launchbury, J., Peyton\u00a0Jones, S.L.: A short cut to deforestation. In: Proceedings of the Conference on Functional Programming Languages and Computer Architecture, pp. 223\u2013232 (1993)","DOI":"10.1145\/165180.165214"},{"key":"21_CR19","doi-asserted-by":"publisher","unstructured":"Govind, H., Shoham, S., Gurfinkel, A.: Solving constrained horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6(POPL), 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3498722","DOI":"10.1145\/3498722"},{"key":"21_CR20","unstructured":"Hajd\u00fa, M., Hozzov\u00e1, P., Kov\u00e1cs, L., Voronkov, A.: Induction with recursive definitions in superposition. In: FMCAD, pp. 1\u201310. IEEE (2021)"},{"issue":"1","key":"21_CR21","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.entcs.2005.11.028","volume":"151","author":"GW Hamilton","year":"2006","unstructured":"Hamilton, G.W.: Po\u00edtin: distilling theorems from conjectures. Electron. Notes Theor. Comput. Sci. 151(1), 143\u2013160 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"Hamilton, G.W.: Distillation: extracting the essence of programs. In: Proceedings of the 2007 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, pp. 61\u201370 (2007)","DOI":"10.1145\/1244381.1244391"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Hinze, R., Harper, T., James, D.W.: Theory and practice of fusion. In: Symposium on Implementation and Application of Functional Languages, pp. 19\u201337. Springer (2010)","DOI":"10.1007\/978-3-642-24276-2_2"},{"issue":"9","key":"21_CR24","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/2544174.2500578","volume":"48","author":"R Hinze","year":"2013","unstructured":"Hinze, R., Wu, N., Gibbons, J.: Unifying structured recursion schemes. ACM SIGPLAN Notices 48(9), 209\u2013220 (2013)","journal-title":"ACM SIGPLAN Notices"},{"issue":"6","key":"21_CR25","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/232629.232637","volume":"31","author":"Z Hu","year":"1996","unstructured":"Hu, Z., Iwasaki, H., Takeichi, M.: Deriving structural hylomorphisms from recursive definitions. ACM Sigplan Notices 31(6), 73\u201382 (1996)","journal-title":"ACM Sigplan Notices"},{"key":"21_CR26","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-642-14052-5_21","volume-title":"Interactive Theorem Proving","author":"M Johansson","year":"2010","unstructured":"Johansson, M., Dixon, L., Bundy, A.: Case-analysis for rippling and inductive proof. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, pp. 291\u2013306. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_21"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Kapur, D., Subramaniam, M.: Automatic generation of simple lemmas from recursive definitions using decision procedures\u2013preliminary report. In: Advances in Computing Science\u2013ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation: 8th Asian Computing Science Conference, Mumbai, India, December 10-12, 2003. Proceedings 8, pp. 125\u2013145. Springer (2003)","DOI":"10.1007\/978-3-540-40965-6_9"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Klyuchnikov, I.G., Romanenko, S.A.: Proving the equivalence of higher-order terms by means of supercompilation. In: Ershov Memorial Conference, pp. 193\u2013205. Springer (2009)","DOI":"10.1007\/978-3-642-11486-1_17"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"Kostyukov, Y., Mordvinov, D., Fedyukovich, G.: Beyond the elementary representations of program invariants over algebraic data types. In: PLDI, pp. 451\u2013465 (2021)","DOI":"10.1145\/3453483.3454055"},{"key":"21_CR30","doi-asserted-by":"crossref","unstructured":"K\u00fchnemann, A., Gl\u00fcck, R., Kakehi, K.: Relating accumulative and non-accumulative functional programs. In: RTA, vol.\u00a01, pp. 154\u2013168. Springer (2001)","DOI":"10.1007\/3-540-45127-7_13"},{"key":"21_CR31","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). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"21_CR32","doi-asserted-by":"crossref","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)","DOI":"10.1007\/3540543961_7"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Miltner, A., Padhi, S., Millstein, T., Walker, D.: Data-driven inference of representation invariants. In: PLDI, pp. 1\u201315 (2020)","DOI":"10.1145\/3385412.3385967"},{"key":"21_CR34","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 de Moura","year":"2008","unstructured":"de 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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Nandi, C., et al.: Rewrite rule inference using equality saturation. In: Proceedings of the ACM on Programming Languages vol. 5(OOPSLA), pp. 1\u201328 (2021)","DOI":"10.1145\/3485496"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"1","key":"21_CR37","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/1190215.1190241","volume":"42","author":"A Ohori","year":"2007","unstructured":"Ohori, A., Sasano, I.: Lightweight fusion by fixed point promotion. ACM SIGPLAN Notices 42(1), 143\u2013154 (2007)","journal-title":"ACM SIGPLAN Notices"},{"issue":"4","key":"21_CR38","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10817-016-9368-2","volume":"57","author":"T Pham","year":"2016","unstructured":"Pham, T., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. J. Autom. Reason. 57(4), 281\u2013318 (2016)","journal-title":"J. Autom. Reason."},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-25543-5_5","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C., Tinelli, C.: CVC4SY: smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 74\u201383. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5"},{"key":"21_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"issue":"1","key":"21_CR41","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM (JACM) 12(1), 23\u201341 (1965)","journal-title":"J. ACM (JACM)"},{"key":"21_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-030-81688-9_6","volume-title":"Computer Aided Verification","author":"E Singher","year":"2021","unstructured":"Singher, E., Itzhaky, S.: Theory exploration powered by deductive synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 125\u2013148. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_6"},{"issue":"OOPSLA2","key":"21_CR43","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1145\/3563306","volume":"6","author":"A Sivaraman","year":"2022","unstructured":"Sivaraman, A., Sanchez-Stern, A., Chen, B., Lerner, S., Millstein, T.D.: Data-driven lemma synthesis for interactive proofs. Proc. ACM Program. Lang. 6(OOPSLA2), 505\u2013531 (2022)","journal-title":"Proc. ACM Program. Lang."},{"key":"21_CR44","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)","journal-title":"J. Funct. Program."},{"key":"21_CR45","unstructured":"Sonnex, W.: Fixed point promotion: taking the induction out of automated induction. University of Cambridge, Computer Laboratory, Tech. rep. (2017)"},{"key":"21_CR46","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"},{"key":"21_CR47","doi-asserted-by":"crossref","unstructured":"Srivastava, S., Gulwani, S.: Program verification using templates over predicate abstraction. In: PLDI, pp. 223\u2013234. ACM (2009)","DOI":"10.1145\/1542476.1542501"},{"key":"21_CR48","doi-asserted-by":"crossref","unstructured":"Takano, A., Meijer, E.: Shortcut deforestation in calculational form. In: Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, pp. 306\u2013313 (1995)","DOI":"10.1145\/224164.224221"},{"issue":"3","key":"21_CR49","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. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(3), 292\u2013325 (1986)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"21_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-19027-9_23","volume-title":"ESOP \u201988","author":"P Wadler","year":"1988","unstructured":"Wadler, P.: Deforestation: transforming programs to eliminate trees. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 344\u2013358. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-19027-9_23"},{"key":"21_CR51","doi-asserted-by":"crossref","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: EGG: fast and extensible equality saturation. In: Proceedings of the ACM on Programming Languages, vol. 5(POPL), pp. 1\u201329 (2021)","DOI":"10.1145\/3434304"},{"key":"21_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/978-3-030-30048-7_35","volume-title":"Principles and Practice of Constraint Programming","author":"W Yang","year":"2019","unstructured":"Yang, W., Fedyukovich, G., Gupta, A.: Lemma synthesis for automating induction over algebraic data types. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 600\u2013617. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30048-7_35"},{"key":"21_CR53","unstructured":"Yokoyama, T., Hu, Z., Takeichi, M.: Calculation rules for warming-up in fusion transformation. In: the 2005 Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, pp. 399\u2013412. Citeseer (2005)"},{"key":"21_CR54","doi-asserted-by":"publisher","unstructured":"Zaval\u00eda, L., Chernigovskaia, L., Fedyukovich, G.: Solving constrained horn clauses over algebraic data types. In: Dragoi, C., Emmi, M., Wang, J. (eds.) Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings. Lecture Notes in Computer Science, vol. 13881, pp. 341\u2013365. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_16","DOI":"10.1007\/978-3-031-24950-1_16"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-10794-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:24Z","timestamp":1767967164000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,16]]},"assertion":[{"value":"16 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2025.ens.psl.eu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}