{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T17:17:10Z","timestamp":1778692630079,"version":"3.51.4"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T00:00:00Z","timestamp":1773964800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T00:00:00Z","timestamp":1773964800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004270","name":"Royal Institute of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004270","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2026,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about this equivalent program instead. In this article, we propose\n                    <jats:italic>program instrumentation<\/jats:italic>\n                    as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the\n                    <jats:sc>MonoCera<\/jats:sc>\n                    tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.\n                  <\/jats:p>","DOI":"10.1007\/s10703-026-00493-w","type":"journal-article","created":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:12:28Z","timestamp":1774023148000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A program instrumentation framework for automatic verification"],"prefix":"10.1007","volume":"68","author":[{"given":"Jesper","family":"Amilon","sequence":"first","affiliation":[]},{"given":"Zafer","family":"Esen","sequence":"additional","affiliation":[]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Lidstr\u00f6m","sequence":"additional","affiliation":[]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[]},{"given":"Marten","family":"Voorberg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,3,20]]},"reference":[{"key":"493_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of model checking","author":"EM Clarke","year":"2018","unstructured":"Clarke EM, Henzinger TA, Veith H et al. (eds) (2018) Handbook of model checking. Springer. https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"key":"493_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of practical logic and automated reasoning","author":"J Harrison","year":"2009","unstructured":"Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press"},{"key":"493_CR3","doi-asserted-by":"publisher","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22\u201325 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, pp 55\u201374. https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"493_CR4","unstructured":"Baudin P, Filli\u00e2tre JC, March\u00e9 C et al. (2024) ACSL: ANSI\/ISO C specification language. Tech. Rep., CEA-List, https:\/\/frama-c.com\/download\/acsl.pdf, Inria"},{"key":"493_CR5","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral specifications of businesses and systems, the kluwer international series in engineering and computer science","author":"GT Leavens","year":"1999","unstructured":"Leavens GT, Baker AL, Ruby C (1999) JML: a notation for detailed design. In: Kilov H, Rumpe B, Simmonds I (eds) Behavioral specifications of businesses and systems, the Kluwer international series in engineering and computer science, vol 523. Springer, pp 175\u2013188. https:\/\/doi.org\/10.1007\/978-1-4615-5229-1_12"},{"key":"493_CR6","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner NS, McMillan KL, Rybalchenko A (2013) On solving universally quantified Horn clauses. In: Logozzo F, F\u00e4hndrich M (eds) Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings, Lecture Notes in Computer Science, vol 7935. Springer, pp 105\u2013125. https:\/\/doi.org\/10.1007\/978-3-642-38856-9_8","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"493_CR7","doi-asserted-by":"publisher","unstructured":"Monniaux D, Gonnord L (2016) Cell morphing: from array programs to array-free horn clauses. In: Rival X (ed) Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, Lecture Notes in Computer Science, vol 9837. Springer, pp 361\u2013382. https:\/\/doi.org\/10.1007\/978-3-662-53413-7_18","DOI":"10.1007\/978-3-662-53413-7_18"},{"key":"493_CR8","doi-asserted-by":"publisher","unstructured":"Donaldson AF, Kroening D, R\u00fcmmer P (2010) Automatic analysis of scratch-pad memory code for heterogeneous multicore processors. In: Esparza J, Majumdar R (eds) Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol 6015. Springer, pp 280\u2013295. https:\/\/doi.org\/10.1007\/978-3-642-12002-2_24","DOI":"10.1007\/978-3-642-12002-2_24"},{"issue":"3","key":"493_CR9","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/s10703-016-0243-x","volume":"48","author":"J Filli\u00e2tre","year":"2016","unstructured":"Filli\u00e2tre J, Gondelman L, Paskevich A (2016) The spirit of ghost code. Formal Methods Syst Des 48(3):152\u2013174. https:\/\/doi.org\/10.1007\/s10703-016-0243-x","journal-title":"Formal Methods Syst Des"},{"key":"493_CR10","doi-asserted-by":"publisher","unstructured":"Priya S, Zhou X, Su Y et al. (2021) Verifying verified code. In: Hou Z, Ganesh V (eds) Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings, Lecture Notes in Computer Science, vol 12971. Springer, pp 187\u2013202. https:\/\/doi.org\/10.1007\/978-3-030-88885-5_13","DOI":"10.1007\/978-3-030-88885-5_13"},{"key":"493_CR11","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-031-37709-9_14","volume-title":"Computer aided verification","author":"J Amilon","year":"2023","unstructured":"Amilon J, Esen Z, Gurov D et al. (2023) Automatic program instrumentation for automatic verification. In: Enea C, Lal A (eds) Computer aided verification. Springer Nature, Switzerland, Cham, pp 281\u2013304. https:\/\/doi.org\/10.1007\/978-3-031-37709-9_14"},{"key":"493_CR12","doi-asserted-by":"publisher","unstructured":"Beyer D (2022) Progress on software verification: SV-COMP 2022. In: Fisman D, Rosu G (eds) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, Lecture Notes in Computer Science, vol 13244. Springer, pp 375\u2013402. https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20","DOI":"10.1007\/978-3-030-99527-0_20"},{"key":"493_CR13","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner N, Gurfinkel A, McMillan KL et al. (2015) Horn clause solvers for program verification. In: Beklemishev LD, Blass A, Dershowitz N et al. (eds) Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Lecture Notes in Computer Science, vol 9300. Springer, pp 24\u201351. https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"493_CR14","unstructured":"Barrett C, Fontaine P, Tinelli C (2017) The SMT-LIB standard: version 2.6. Tech. Rep., Department of Computer Science, The University of Iowa. Available at https:\/\/www.SMT-LIB.org"},{"key":"493_CR15","doi-asserted-by":"publisher","unstructured":"Flanagan C, Saxe JB (2001) Avoiding exponential explosion: generating compact verification conditions. In: Hankin C, Schmidt D (eds) Proceedings of: Symposium on Principles of Programming Languages (POPL\u201901), ACM, pp 193\u2013205. https:\/\/doi.org\/10.1145\/360204.360220","DOI":"10.1145\/360204.360220"},{"key":"493_CR16","doi-asserted-by":"publisher","unstructured":"Cuoq P, Kirchner F, Kosmatov N et al. (2012) Frama-C - A software analysis perspective. In: Eleftherakis G, Hinchey M, Holcombe M (eds) Software Engineering and Formal Methods - 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, Lecture Notes in Computer Science, vol 7504. Springer, pp 233\u2013247. https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"493_CR17","doi-asserted-by":"publisher","unstructured":"Hojjat H, R\u00fcmmer P (2018) The ELDARICA horn solver. In FMCAD 2018, pp 1\u20137. https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"493_CR18","doi-asserted-by":"crossref","unstructured":"Kahsai T, Kersten R, R\u00fcmmer P et al. (2017) Quantified heap invariants for object-oriented programs. In: Eiter T, Sands D (eds) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, EPiC Series in Computing, vol 46. EasyChair, pp 368\u2013384. https:\/\/easychair.org\/publications\/paper\/Pmh","DOI":"10.29007\/zrct"},{"key":"493_CR19","doi-asserted-by":"publisher","unstructured":"Ernst G (2023) Korn - software verification with horn clauses (competition contribution). In: Sankaranarayanan S, Sharygina N (eds) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, Lecture Notes in Computer Science, vol 13994. Springer, pp 559\u2013564. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_36","DOI":"10.1007\/978-3-031-30820-8_36"},{"key":"493_CR20","doi-asserted-by":"publisher","unstructured":"Matsushita Y, Tsukada T, Kobayashi N (2021) RustHorn: CHC-based verification for rust programs. ACM Trans Program Lang Syst 43(4):15:1\u201315:54. https:\/\/doi.org\/10.1145\/3462205","DOI":"10.1145\/3462205"},{"key":"493_CR21","doi-asserted-by":"publisher","unstructured":"Gurfinkel A, Kahsai T, Komuravelli A et al. (2015) The SeaHorn verification framework. In: Kroening D, Pasareanu CS (eds) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Lecture Notes in Computer Science, vol 9206. Springer, pp 343\u2013361. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"493_CR22","doi-asserted-by":"publisher","unstructured":"Esen Z, R\u00fcmmer P (2022) Tricera: verifying C programs using the theory of heaps. In: Griggio A, Rungta N (eds) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, IEEE, pp 380\u2013391. https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_45","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_45"},{"key":"493_CR23","doi-asserted-by":"publisher","unstructured":"Amilon J, Esen Z, Gurov D et al. (2023) Artifact for the CAV 2023 paper \u201cAutomatic program instrumentation for automatic verification\u201d. https:\/\/doi.org\/10.5281\/zenodo.7875416","DOI":"10.5281\/zenodo.7875416"},{"key":"493_CR24","doi-asserted-by":"publisher","unstructured":"Beyer D, Keremoglu ME (2011) Cpachecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, Lecture Notes in Computer Science, vol 6806. Springer, pp 184\u2013190. https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"493_CR25","doi-asserted-by":"publisher","unstructured":"Afzal M, Chakraborty S, Chauhan A et al. (2020) Veriabs: verification by abstraction and test generation (competition contribution). In: Biere A, Parker D (eds) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, Lecture Notes in Computer Science, vol 12079. Springer, pp 383\u2013387. https:\/\/doi.org\/10.1007\/978-3-030-45237-7_25","DOI":"10.1007\/978-3-030-45237-7_25"},{"key":"493_CR26","doi-asserted-by":"publisher","unstructured":"Beyer D, Dangl M, Wendler P (2015) Boosting k-induction with continuously-refined invariants. In: Kroening D, Pasareanu CS (eds) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Lecture Notes in Computer Science, vol 9206. Springer, pp 622\u2013640. https:\/\/doi.org\/10.1007\/978-3-319-21690-4_42","DOI":"10.1007\/978-3-319-21690-4_42"},{"key":"493_CR27","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5831003","volume-title":"SV-Benchmarks: benchmark set for software verification and testing (SV-COMP 2022 and test-comp 2022)","author":"D Beyer","year":"2022","unstructured":"Beyer D (2022) SV-Benchmarks: benchmark set for software verification and testing (SV-COMP 2022 and test-comp 2022). https:\/\/doi.org\/10.5281\/zenodo.5831003"},{"key":"493_CR28","unstructured":"Amilon J, Esen Z, Gurov D et al. (2024) A program instrumentation framework for automatic verification. https:\/\/arxiv.org\/abs\/2412.06431, 2412.06431"},{"key":"493_CR29","doi-asserted-by":"publisher","unstructured":"Alberti F, Bruttomesso R, Ghilardi S et al. (2012) Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner NS, Voronkov A (eds) Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, M\u00e9rida, Venezuela, March 11-15, 2012. Proceedings, Lecture Notes in Computer Science, vol 7180. Springer, pp 46\u201361. https:\/\/doi.org\/10.1007\/978-3-642-28717-6_7","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"493_CR30","doi-asserted-by":"publisher","unstructured":"Gurfinkel A, Shoham S, Vizel Y (2018) Quantifiers on demand. In: Lahiri SK, Wang C (eds) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, Lecture Notes in Computer Science, vol 11138. Springer, pp 248\u2013266. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15","DOI":"10.1007\/978-3-030-01090-4_15"},{"key":"493_CR31","doi-asserted-by":"publisher","unstructured":"Fedyukovich G, Prabhu S, Madhukar K et al. (2019) Quantified invariants via syntax-guided synthesis. In: Dillig I, Tasiran S (eds) Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I, Lecture Notes in Computer Science, vol 11561. Springer, pp 259\u2013277. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"493_CR32","doi-asserted-by":"publisher","unstructured":"Garg P, L\u00f6ding C, Madhusudan P et al. (2013) Learning universally quantified invariants of linear data structures. In: Sharygina N, Veith H (eds) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, Lecture Notes in Computer Science, vol 8044. Springer, pp 813\u2013829. https:\/\/doi.org\/10.1007\/978-3-642-39799-8_57","DOI":"10.1007\/978-3-642-39799-8_57"},{"key":"493_CR33","doi-asserted-by":"publisher","unstructured":"Henzinger TA, Hottelier T, Kov\u00e1cs L et al. (2010) Aligators for arrays (tool paper). In: Ferm\u00fcller CG, Voronkov A (eds) Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, Lecture Notes in Computer Science, vol 6397. Springer, pp 348\u2013356. https:\/\/doi.org\/10.1007\/978-3-642-16242-8_25","DOI":"10.1007\/978-3-642-16242-8_25"},{"key":"493_CR34","doi-asserted-by":"publisher","unstructured":"Georgiou P, Gleiss B, Kov\u00e1cs L (2020) Trace logic for inductive loop reasoning. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, IEEE, pp 255\u2013263. https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_33","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_33"},{"key":"493_CR35","doi-asserted-by":"publisher","unstructured":"Leino KRM, Monahan R (2009) Reasoning about comprehensions with first-order SMT solvers. In: Shin SY, Ossowski S (eds) Proceedings of the 2009 ACM Symposium on Applied Computing (SAC), Honolulu, Hawaii, USA, March 9-12, 2009, ACM, pp 615\u2013622. https:\/\/doi.org\/10.1145\/1529282.1529411","DOI":"10.1145\/1529282.1529411"},{"key":"493_CR36","doi-asserted-by":"publisher","unstructured":"Ahrendt W, Beckert B, Bubel R et al. (2016) Deductive software verification - the KeY book - from theory to practice. In Lecture Notes in Computer Science, vol 10001. Springer. https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"493_CR37","doi-asserted-by":"publisher","unstructured":"Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EM, Voronkov A (eds) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science, vol 6355. Springer, pp 348\u2013370. https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"issue":"4","key":"493_CR38","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1017\/S1471068422000175","volume":"22","author":"E De Angelis","year":"2022","unstructured":"De Angelis E, Proietti M, Fioravanti F et al. (2022) Verifying catamorphism-based contracts using constrained horn clauses. Theory Pract Log Program 22(4):555\u2013572. https:\/\/doi.org\/10.1017\/S1471068422000175","journal-title":"Theory Pract Log Program"},{"issue":"POPL","key":"493_CR39","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3498722","volume":"6","author":"K Hgv","year":"2022","unstructured":"Hgv K, Shoham S, Gurfinkel A (2022) Solving constrained horn clauses modulo algebraic data types and recursive functions. Proc ACM Program Lang 6(POPL):1\u201329. https:\/\/doi.org\/10.1145\/3498722","journal-title":"Proc ACM Program Lang"},{"key":"493_CR40","doi-asserted-by":"publisher","unstructured":"Daca P, Henzinger TA, Kupriyanov A (2016) Array folds logic. In: Chaudhuri S, Farzan A (eds) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Lecture Notes in Computer Science, vol 9780. Springer, pp 230\u2013248. https:\/\/doi.org\/10.1007\/978-3-319-41540-6_13","DOI":"10.1007\/978-3-319-41540-6_13"},{"key":"493_CR41","doi-asserted-by":"publisher","unstructured":"Segoufin L (2006) Automata and logics for words and trees over an infinite alphabet. In: \u00c9sik Z (ed) Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, Lecture Notes in Computer Science, vol 4207. Springer, pp 41\u201357. https:\/\/doi.org\/10.1007\/11874683_3","DOI":"10.1007\/11874683_3"},{"issue":"3","key":"493_CR42","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F Neven","year":"2004","unstructured":"Neven F, Schwentick T, Vianu V (2004) Finite state machines for strings over infinite alphabets. ACM Trans Comput Log 5(3):403\u2013435. https:\/\/doi.org\/10.1145\/1013560.1013562","journal-title":"ACM Trans Comput Log"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00493-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-026-00493-w","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-026-00493-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T16:39:45Z","timestamp":1778690385000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-026-00493-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,20]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4]]}},"alternative-id":["493"],"URL":"https:\/\/doi.org\/10.1007\/s10703-026-00493-w","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,20]]},"assertion":[{"value":"15 March 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 February 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 March 2026","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 no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"7"}}