{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:39:29Z","timestamp":1767983969294,"version":"3.49.0"},"publisher-location":"Cham","reference-count":46,"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_11","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:16Z","timestamp":1763188996000},"page":"205-225","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["CHC-Based Reachability Analysis via\u00a0Cycle Summarization"],"prefix":"10.1007","author":[{"given":"Konstantin","family":"Britikov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"11_CR1","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":"11_CR2","doi-asserted-by":"publisher","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf. 10(5), 401\u2013424 (2008). https:\/\/doi.org\/10.1007\/s10009-008-0064-3","DOI":"10.1007\/s10009-008-0064-3"},{"key":"11_CR3","unstructured":"Beyer, D., Keremoglu, M.E., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: Bloem, R., Sharygina, N. (eds.) Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pp. 189\u2013197. IEEE (2010), https:\/\/ieeexplore.ieee.org\/document\/5770949\/"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Lee, N., Wendler, P.: Interpolation and sat-based model checking revisited: Adoption to software verification. CoRR abs\/2208.05046 (2022). https:\/\/doi.org\/10.48550\/arXiv.2208.05046","DOI":"10.48550\/arXiv.2208.05046"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.S., Gurfinkel, A., McMillan, K.L., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (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.\u00a09300, pp. 24\u201351. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"11_CR6","doi-asserted-by":"publisher","unstructured":"Blicha, M., Britikov, K., Sharygina, N.: The golem horn solver. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13965, pp. 209\u2013223. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_10","DOI":"10.1007\/978-3-031-37703-7_10"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Split transition power abstraction for unbounded safety. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, pp. 349\u2013358. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_42","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_42"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Blicha, M., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Transition power abstractions for deep counterexample detection. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022. Lecture Notes in Computer Science, vol. 13243, pp. 524\u2013542. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_29","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Blicha, M., Kofron, J., Tatarko, W.: Summarization of branching loops. In: Hong, J., Bures, M., Park, J.W., Cern\u00fd, T. (eds.) SAC \u201922: The 37th ACM\/SIGAPP Symposium on Applied Computing, Virtual Event, April 25 - 29, 2022, pp. 1808\u20131816. ACM (2022). https:\/\/doi.org\/10.1145\/3477314.3507042","DOI":"10.1145\/3477314.3507042"},{"key":"11_CR10","doi-asserted-by":"publisher","unstructured":"Bozga, M., Iosif, R., Konecn\u00fd, F.: Fast acceleration of ultimately periodic relations. In: Touili, T., Cook, B., Jackson, P.B. (eds.) Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19. Lecture Notes in Computer Science, vol.\u00a06174, pp. 227\u2013242. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_23","DOI":"10.1007\/978-3-642-14295-6_23"},{"key":"11_CR11","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z.: Property-directed incremental invariant generation. Formal Aspects Comput. 20(4-5), 379\u2013405 (2008). https:\/\/doi.org\/10.1007\/S00165-008-0080-9","DOI":"10.1007\/S00165-008-0080-9"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Britikov, K., Blicha, M., Sharygina, N., Fedyukovich, G.: Reachability analysis for multiloop programs using transition power abstraction. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14933, pp. 558\u2013576. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_29","DOI":"10.1007\/978-3-031-71162-6_29"},{"key":"11_CR13","unstructured":"Bueno, D.: Horn2VMT: Translating horn reachability into transition systems. Tech. rep., Sandia National Lab. (SNL-NM), Albuquerque, NM (United States) (2020)"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001). https:\/\/doi.org\/10.1023\/A:1011276507260","DOI":"10.1023\/A:1011276507260"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) Computer Aided Verification, 12th International Conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, Proceedings. Lecture Notes in Computer Science, vol.\u00a01855, pp. 154\u2013169. Springer (2000). https:\/\/doi.org\/10.1007\/10722167_15","DOI":"10.1007\/10722167_15"},{"issue":"3","key":"11_CR16","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(3), 269\u2013285 (1957)","journal-title":"J. Symbolic Logic"},{"key":"11_CR17","doi-asserted-by":"publisher","unstructured":"De Angelis, E., K., H.G.V.: CHC-COMP 2023: competition report. In: Kutsia, T., Ventura, D., Monniaux, D., Morales, J.F. (eds.) Proceedings 18th International Workshop on Logical and Semantic Frameworks, with Applications and 10th Workshop on Horn Clauses for Verification and Synthesis, LSFA\/HCVS 2023, and 10th Workshop on Horn Clauses for Verification and SynthesisRome, Italy & Paris, France, 1-2 July, 2023 & 23rd April 2023. EPTCS, vol.\u00a0402, pp. 83\u2013104 (2023). https:\/\/doi.org\/10.4204\/EPTCS.402.10","DOI":"10.4204\/EPTCS.402.10"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Donaldson, A.F., Kroening, D., R\u00fcmmer, P.: Automatic analysis of DMA races using model checking and k-induction. Formal Methods Syst. Des. 39(1), 83\u2013113 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0124-2","DOI":"10.1007\/s10703-011-0124-2"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Ernst, G.: 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, pp. 559\u2013564. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_36","DOI":"10.1007\/978-3-031-30820-8_36"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Kaufman, S.J., Bod\u00edk, R.: Learning inductive invariants by sampling from frequency distributions. Formal Methods Syst. Des. 56(1), 154\u2013177 (2020). https:\/\/doi.org\/10.1007\/s10703-020-00349-x","DOI":"10.1007\/s10703-020-00349-x"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: 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, pp. 259\u2013277. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Frohn, F.: A calculus for modular loop acceleration. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020. Lecture Notes in Computer Science, vol. 12078, pp. 58\u201376. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_4","DOI":"10.1007\/978-3-030-45190-5_4"},{"key":"11_CR23","unstructured":"Frohn, F., Giesl, J.: Proving non-termination via loop acceleration. CoRR abs\/1905.11187 (2019). http:\/\/arxiv.org\/abs\/1905.11187"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 712\u2013722. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_41","DOI":"10.1007\/978-3-031-10769-6_41"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Accelerated bounded model checking. CoRR abs\/2401.09973 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.09973","DOI":"10.48550\/ARXIV.2401.09973"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Frohn, F., Giesl, J.: Integrating loop acceleration into bounded model checking. In: Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M. (eds.) Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14933, pp. 73\u201391. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71162-6_4","DOI":"10.1007\/978-3-031-71162-6_4"},{"key":"11_CR27","doi-asserted-by":"publisher","unstructured":"Godefroid, P., Luchaup, D.: Automatic partial loop summarization in dynamic test generation. In: Dwyer, M.B., Tip, F. (eds.) Proceedings of the 20th International Symposium on Software Testing and Analysis, ISSTA 2011, Toronto, ON, Canada, pp. 23\u201333. ACM (2011). https:\/\/doi.org\/10.1145\/2001420.2001424","DOI":"10.1145\/2001420.2001424"},{"key":"11_CR28","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Pasareanu, C.S. (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.\u00a09206, pp. 343\u2013361. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"11_CR29","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, pp.\u00a01\u20137. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Hyv\u00e4rinen, A.E.J., Marescotti, M., Alt, L., Sharygina, N.: OpenSMT2: an SMT solver for multi-core and cloud computing. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09710, pp. 547\u2013553. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_35","DOI":"10.1007\/978-3-319-40970-2_35"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Kafle, B., Gallagher, J.P., Morales, J.F.: Rahft: a tool for verifying horn clauses using abstract interpretation and finite tree automata. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada. Lecture Notes in Computer Science, vol.\u00a09779, pp. 261\u2013268. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_14","DOI":"10.1007\/978-3-319-41528-4_14"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Kahsai, T., R\u00fcmmer, P., Sanchez, H., Sch\u00e4f, M.: Jayhorn: a framework for verifying java programs. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol.\u00a09779, pp. 352\u2013358. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_19","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Kamath, A., et al.: Finding inductive loop invariants using large language models. CoRR abs\/2311.07948 (2023). https:\/\/doi.org\/10.48550\/arXiv.2311.07948","DOI":"10.48550\/arXiv.2311.07948"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/S10703-016-0249-4","DOI":"10.1007\/S10703-016-0249-4"},{"key":"11_CR35","doi-asserted-by":"publisher","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S.D., Choi, J., Kim, M., Lee, I., Viswanathan, M. (eds.) Automated Technology for Verification and Analysis, 6th International Symposium, ATVA 2008, Seoul, Korea. Lecture Notes in Computer Science, vol.\u00a05311, pp. 111\u2013125. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-88387-6_10","DOI":"10.1007\/978-3-540-88387-6_10"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Lin, S., Sun, J., Xiao, H., Liu, Y., San\u00e1n, D., Hansen, H.: FiB: squeezing loop invariants by interpolation between forward\/backward predicate transformers. In: Rosu, G., Penta, M.D., Nguyen, T.N. (eds.) Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, pp. 793\u2013803. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115690","DOI":"10.1109\/ASE.2017.8115690"},{"key":"11_CR37","doi-asserted-by":"publisher","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for rust programs. In: M\u00fcller, P. (ed.) Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12075, pp. 484\u2013514. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_18","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"11_CR38","unstructured":"McMillan, K., Rybalchenko, A.: Computing relational fixed points using interpolation. Technical report, January 2013. MSR-TR-2013-6 (2013)"},{"key":"11_CR39","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and sat-based model checking. In: Jr., W.A.H., Somenzi, F. (eds.) Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02725, pp. 1\u201313. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"11_CR40","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04144, pp. 123\u2013136. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"11_CR41","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"11_CR42","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pp. 32\u201341. IEEE Computer Society (2004). https:\/\/doi.org\/10.1109\/LICS.2004.1319598","DOI":"10.1109\/LICS.2004.1319598"},{"key":"11_CR43","unstructured":"Ryan, G., Wong, J., Yao, J., Gu, R., Jana, S.: CLN2INV: learning loop invariants with continuous logic networks. In: 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia. OpenReview.net (2020). https:\/\/openreview.net\/forum?id=HJlfuTEtvB"},{"key":"11_CR44","doi-asserted-by":"publisher","unstructured":"Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification - 31st International Conference, CAV 2019. Lecture Notes in Computer Science, vol. 11562, pp. 97\u2013115. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_7","DOI":"10.1007\/978-3-030-25543-5_7"},{"key":"11_CR45","doi-asserted-by":"publisher","unstructured":"Strejcek, J., Trt\u00edk, M.: Abstracting path conditions. In: Heimdahl, M.P.E., Su, Z. (eds.) International Symposium on Software Testing and Analysis, ISSTA 2012, Minneapolis, MN, USA, pp. 155\u2013165. ACM (2012). https:\/\/doi.org\/10.1145\/2338965.2336772","DOI":"10.1145\/2338965.2336772"},{"key":"11_CR46","doi-asserted-by":"publisher","unstructured":"Xie, X., Chen, B., Zou, L., Liu, Y., Le, W., Li, X.: Automatic loop summarization via path dependency analysis. IEEE Trans. Software Eng. 45(6), 537\u2013557 (2019). https:\/\/doi.org\/10.1109\/TSE.2017.2788018","DOI":"10.1109\/TSE.2017.2788018"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:58:50Z","timestamp":1767967130000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_11","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"}}]}}