{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T18:27:39Z","timestamp":1767983259932,"version":"3.49.0"},"publisher-location":"Cham","reference-count":48,"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_20","type":"book-chapter","created":{"date-parts":[[2025,11,15]],"date-time":"2025-11-15T06:43:12Z","timestamp":1763188992000},"page":"401-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Model-Based Testing of\u00a0an\u00a0Intermediate Verifier Using Executable Operational Semantics"],"prefix":"10.1007","author":[{"given":"Lidia","family":"Losavio","sequence":"first","affiliation":[]},{"given":"Marco","family":"Paganoni","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1040-3201","authenticated-orcid":false,"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,11,16]]},"reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-642-25379-9_22","volume-title":"Certified Programs and Proofs","author":"M Backes","year":"2011","unstructured":"Backes, M., Hri\u0163cu, C., Tarrach, T.: Automatically verifying typing constraints for a data processing language. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 296\u2013313. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_22"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Baek, S.: A formally verified checker for first-order proofs. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). LIPIcs, vol.\u00a0193, pp. 6:1\u20136:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2021.6","DOI":"10.4230\/LIPICS.ITP.2021.6"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Bringolf, M., Winterer, D., Su, Z.: Finding and understanding incompleteness bugs in SMT solvers. In: 37th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, 10\u201314 October 2022, pp. 43:1\u201343:10. ACM (2022). https:\/\/doi.org\/10.1145\/3551349.3560435","DOI":"10.1145\/3551349.3560435"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14186-7_6","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"R Brummayer","year":"2010","unstructured":"Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44\u201357. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_6"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-030-90870-6_15","volume-title":"Formal Methods","author":"A Bugariu","year":"2021","unstructured":"Bugariu, A., Ter-Gabrielyan, A., M\u00fcller, P.: Identifying overly restrictive matching patterns in SMT-based program verifiers. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 273\u2013291. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_15"},{"key":"20_CR7","doi-asserted-by":"publisher","unstructured":"Chen, J., et al.: A survey of compiler testing. ACM Comput. Surv. 53(1), 4:1\u20134:36 (2021). https:\/\/doi.org\/10.1145\/3363562","DOI":"10.1145\/3363562"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-66845-1_19","volume-title":"Integrated Formal Methods","author":"YT Chen","year":"2017","unstructured":"Chen, Y.T., Furia, C.A.: Triggerless happy \u2013 intermediate verification with a first-order prover. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 295\u2013311. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_19"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-030-01090-4_6","volume-title":"Automated Technology for Verification and Analysis","author":"YT Chen","year":"2018","unstructured":"Chen, Y.T., Furia, C.A.: Robustness testing of intermediate verifiers. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 91\u2013108. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_6"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Dardinier, T., Sammler, M., Parthasarathy, G., Summers, A.J., M\u00fcller, P.: Formal foundations for translational separation logic verifiers. Proc. ACM Program. Lang. 9(POPL), 569\u2013599 (2025). https:\/\/doi.org\/10.1145\/3704856","DOI":"10.1145\/3704856"},{"key":"20_CR11","unstructured":"Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT Press (2009). http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=11885"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-662-46669-8_16","volume-title":"Programming Languages and Systems","author":"B Fetscher","year":"2015","unstructured":"Fetscher, B., Claessen, K., Pa\u0142ka, M., Hughes, J., Findler, R.B.: Making random judgments: automatically generating well-typed terms from the definition of a type-system. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 383\u2013405. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_16"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Fiala, J., Itzhaky, S., M\u00fcller, P., Polikarpova, N., Sergey, I.: Leveraging rust types for program synthesis. Proc. ACM Program. Lang. 7(PLDI), 1414\u20131437 (2023). https:\/\/doi.org\/10.1145\/3591278","DOI":"10.1145\/3591278"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Fink, X., Berger, P., Katoen, J.: Configurable benchmarks for C model checkers. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260, pp. 338\u2013354. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_18","DOI":"10.1007\/978-3-031-06773-0_18"},{"key":"20_CR16","doi-asserted-by":"publisher","unstructured":"From, A.H., Jacobsen, F.K.: Verifying a sequent calculus prover for first-order logic with functions in Isabelle\/HOL. J. Autom. Reason. 68(3), 15 (2024). https:\/\/doi.org\/10.1007\/s10817-024-09697-3","DOI":"10.1007\/s10817-024-09697-3"},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don\u2019t sweat the small stuff: formal verification of C code without the pain. In: O\u2019Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom - 09\u201311 June 2014, pp. 429\u2013439. ACM (2014). https:\/\/doi.org\/10.1145\/2594291.2594296","DOI":"10.1145\/2594291.2594296"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-14107-2_7","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"A Guha","year":"2010","unstructured":"Guha, A., Saftoiu, C., Krishnamurthi, S.: The essence of JavaScript. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126\u2013150. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_7"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-27705-4_2","volume-title":"Verified Software: Theories, Tools, Experiments","author":"P Herms","year":"2012","unstructured":"Herms, P., March\u00e9, C., Monate, B.: A certified multi-prover verification condition generator. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 2\u201317. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_2"},{"key":"20_CR20","doi-asserted-by":"publisher","unstructured":"Kapus, T., Cadar, C.: Automatic testing of symbolic execution engines via program generation and differential testing. 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, 30 October\u201303 November 2017, pp. 590\u2013600. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115669","DOI":"10.1109\/ASE.2017.8115669"},{"key":"20_CR21","doi-asserted-by":"publisher","unstructured":"Klein, C., et al.: Run your research: on the effectiveness of lightweight mechanization. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, 22\u201328 January 2012, pp. 285\u2013296. ACM (2012). https:\/\/doi.org\/10.1145\/2103656.2103691","DOI":"10.1145\/2103656.2103691"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010). https:\/\/doi.org\/10.1145\/1743546.1743574","DOI":"10.1145\/1743546.1743574"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20\u201321 January 2014, pp. 179\u2013192. ACM (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"20_CR24","doi-asserted-by":"publisher","unstructured":"Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: O\u2019Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom - 09\u201311 June 2014, pp. 216\u2013226. ACM (2014). https:\/\/doi.org\/10.1145\/2594291.2594334","DOI":"10.1145\/2594291.2594334"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-41528-4_20","volume-title":"Computer Aided Verification","author":"KRM Leino","year":"2016","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 361\u2013381. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_20"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). http:\/\/xavierleroy.org\/publi\/compcert-backend.pdf","DOI":"10.1007\/s10817-009-9155-4"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1\u201331 (2008). http:\/\/xavierleroy.org\/publi\/memory-model-journal.pdf","DOI":"10.1007\/s10817-008-9099-0"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Liew, D., Cadar, C., Donaldson, A.: Symbooglix: a symbolic execution engine for Boogie programs. In: IEEE International Conference on Software Testing, Verification, and Validation (ICST 2016), pp. 45\u201356 (2016)","DOI":"10.1109\/ICST.2016.11"},{"key":"20_CR29","doi-asserted-by":"publisher","unstructured":"Lin, Z., Chen, X., Trinh, M., Wang, J., Rosu, G.: Generating proof certificates for a language-agnostic deductive program verifier. Proc. ACM Program. Lang. 7(OOPSLA1), 56\u201384 (2023). https:\/\/doi.org\/10.1145\/3586029","DOI":"10.1145\/3586029"},{"key":"20_CR30","doi-asserted-by":"publisher","unstructured":"Losavio, L., Paganoni, M., Furia, C.A.: Boogie Consistency Checker: Replication package for iFM2025 (2025). https:\/\/doi.org\/10.6084\/m9.figshare.29338589.v2","DOI":"10.6084\/m9.figshare.29338589.v2"},{"key":"20_CR31","doi-asserted-by":"publisher","unstructured":"Mansur, M.N., Christakis, M., W\u00fcstholz, V., Zhang, F.: Detecting critical bugs in SMT solvers using blackbox mutational fuzzing. In: Devanbu, P., Cohen, M.B., Zimmermann, T. (eds.) ESEC\/FSE 2020: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, 8\u201313 November 2020, pp. 701\u2013712. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409763","DOI":"10.1145\/3368089.3409763"},{"key":"20_CR32","doi-asserted-by":"publisher","unstructured":"Marti, N., Affeldt, R.: A certified verifier for a fragment of separation logic. Inf. Media Technol. 4(2), 304\u2013316 (2009). https:\/\/doi.org\/10.11185\/IMT.4.304","DOI":"10.11185\/IMT.4.304"},{"key":"20_CR33","doi-asserted-by":"publisher","unstructured":"Monniaux, D., Gourdin, L., Boulm\u00e9, S., Lebeltel, O.: Testing a formally verified compiler. In: Prevosto, V., Seceleanu, C. (eds.) TAP 2023. LNCS, vol. 14066, pp. 40\u201348. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38828-6_3","DOI":"10.1007\/978-3-031-38828-6_3"},{"key":"20_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"20_CR35","doi-asserted-by":"publisher","unstructured":"Nipkow, T.: Winskel is (almost) right: towards a mechanized semantics. Formal Aspects Comput. 10(2), 171\u2013186 (1998). https:\/\/doi.org\/10.1007\/s001650050009","DOI":"10.1007\/s001650050009"},{"key":"20_CR36","doi-asserted-by":"publisher","unstructured":"Parthasarathy, G., Dardinier, T., Bonneau, B., M\u00fcller, P., Summers, A.J.: Towards trustworthy automated program verifiers: formally validating translations into an intermediate verification language. Proc. ACM Program. Lang. 8(PLDI), 1510\u20131534 (2024). https:\/\/doi.org\/10.1145\/3656438","DOI":"10.1145\/3656438"},{"key":"20_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/978-3-030-81688-9_33","volume-title":"Computer Aided Verification","author":"G Parthasarathy","year":"2021","unstructured":"Parthasarathy, G., M\u00fcller, P., Summers, A.J.: Formally validating a practical verification condition generator. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 704\u2013727. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_33"},{"key":"20_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-40787-1_15","volume-title":"Runtime Verification","author":"N Polikarpova","year":"2013","unstructured":"Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before: executing an intermediate verification language. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 251\u2013268. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40787-1_15"},{"key":"20_CR39","unstructured":"Skot\u00e5m, S.H.: CreuSAT, Using Rust and Creusot to create the world\u2019s fastest deductively verified SAT solver. Master\u2019s thesis, University of Oslo (2022). https:\/\/www.duo.uio.no\/handle\/10852\/96757"},{"key":"20_CR40","doi-asserted-by":"publisher","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2:1\u20132:58 (2012). https:\/\/doi.org\/10.1145\/2160910.2160911","DOI":"10.1145\/2160910.2160911"},{"key":"20_CR41","doi-asserted-by":"publisher","unstructured":"Soldevila, M., Ziliani, B., Silvestre, B., Fridlender, D., Mascarenhas, F.: Decoding Lua: formal semantics for the developer and the semanticist. In: Ancona, D. (ed.) Proceedings of the 13th ACM SIGPLAN International Symposium on on Dynamic Languages, Vancouver, BC, Canada, 23\u201327 October 2017, pp. 75\u201386. ACM (2017). https:\/\/doi.org\/10.1145\/3133841.3133848","DOI":"10.1145\/3133841.3133848"},{"issue":"5","key":"20_CR42","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10009-014-0336-z","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transfer 16(5), 465\u2013479 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0336-z","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"20_CR43","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A.C.J., Owens, S., Norrish, M.: The verified CakeML compiler backend. J. Funct. Program. 29, e2 (2019). https:\/\/doi.org\/10.1017\/S0956796818000229","DOI":"10.1017\/S0956796818000229"},{"key":"20_CR44","doi-asserted-by":"publisher","unstructured":"Thoben, N., Haltermann, J., Wehrheim, H.: Timeout prediction for software analyses. In: Ferreira, C., Willemse, T.A.C. (eds.) SEFM 2023. LNCS, vol. 14323, pp. 340\u2013358. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47115-5_19","DOI":"10.1007\/978-3-031-47115-5_19"},{"key":"20_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-95891-8_51","volume-title":"SOFSEM 2009: Theory and Practice of Computer Science","author":"F Vogels","year":"2009","unstructured":"Vogels, F., Jacobs, B., Piessens, F.: A machine checked soundness proof for an intermediate verification language. In: Nielsen, M., Ku\u010dera, A., Miltersen, P.B., Palamidessi, C., T\u016fma, P., Valencia, F. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 570\u2013581. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-540-95891-8_51"},{"key":"20_CR46","doi-asserted-by":"publisher","unstructured":"Winterer, D., Su, Z.: Validating SMT solvers for correctness and performance via grammar-based enumeration. Proc. ACM Program. Lang. 8(OOPSLA2), 2378\u20132401 (2024). https:\/\/doi.org\/10.1145\/3689795","DOI":"10.1145\/3689795"},{"key":"20_CR47","doi-asserted-by":"publisher","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: Hall, M.W., Padua, D.A. (eds.) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, 4\u20138 June 2011, pp. 283\u2013294. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"20_CR48","doi-asserted-by":"publisher","unstructured":"Zhang, C., Su, T., Yan, Y., Zhang, F., Pu, G., Su, Z.: Finding and understanding bugs in software model checkers. In: Dumas, M., Pfahl, D., Apel, S., Russo, A. (eds.) Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE 2019, Tallinn, Estonia, 26\u201330 August 2019, pp. 763\u2013773. ACM (2019). https:\/\/doi.org\/10.1145\/3338906.3338932","DOI":"10.1145\/3338906.3338932"}],"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_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T13:59:33Z","timestamp":1767967173000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10794-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,16]]},"ISBN":["9783032107930","9783032107947"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10794-7_20","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"}}]}}