{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:33Z","timestamp":1776305373385,"version":"3.50.1"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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-22749-2_31","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:09:34Z","timestamp":1776258574000},"page":"551-558","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Mopsa-C: Towards Incorrectness and Termination Verdicts (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6215-7359","authenticated-orcid":false,"given":"Marco","family":"Milanese","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8487-0326","authenticated-orcid":false,"given":"Rapha\u00ebl","family":"Monat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7248-5914","authenticated-orcid":false,"given":"Abdelraouf","family":"Ouadjaout","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-3179","authenticated-orcid":false,"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"31_CR1","unstructured":"Ayaziov\u00e1, P., Jon\u00e1\u0161, M., Mihalkovi\u010d, V., Sedl\u00e1\u010dek, J., Strej\u010dek, J.: Symbiotic 11: Predicate abstraction joins the party (competition contribution). In: Proc. TACAS\u00a0(2), LNCS\u00a016506, Springer (2026)"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"Baier, D., Beyer, D., Chien, P., Jankola, M., Kettl, M., Lee, N., Lemberger, T., Rosenfeld, M.L., Spiessl, M., Wachowitz, H., Wendler, P.: Cpachecker 2.3 with strategy selection - (competition contribution). In: TACAS (3), Lecture Notes in Computer Science, vol. 14572, pp. 359\u2013364, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_21"},{"key":"31_CR3","unstructured":"Barth, M., Dietsch, D., Heizmann, M., Jakobs, M.C.: Ultimate Paralizer: Parallel trace abstraction (competition contribution). In: Proc. TACAS\u00a0(2), LNCS\u00a016506, Springer (2026)"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Becchi, A., Zaffanella, E.: Pplite: Zero-overhead encoding of NNC polyhedra. Inf. Comput. 275, 104620 (2020)","DOI":"10.1016\/j.ic.2020.104620"},{"key":"31_CR5","unstructured":"Beyer, D., Strej\u010dek, J.: Evaluating software verifiers for C, Java, and SV-LIB (report on SV-COMP 2026). In: Proc. TACAS\u00a0(2), LNCS\u00a016506, Springer (2026)"},{"key":"31_CR6","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 238\u2013252, ACM Press, Los Angeles, California (1977), https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"31_CR7","unstructured":"Halbwachs, N.: D\u00e9termination automatique de relations lin\u00e9aires v\u00e9rifi\u00e9es par les variables d\u2019un programme. Theses, Institut National Polytechnique de Grenoble - INPG ; Universit\u00e9 Joseph-Fourier - Grenoble I (Mar 1979), URL https:\/\/theses.hal.science\/tel-00288805, universit\u00e9s : Universit\u00e9 scientifique et m\u00e9dicale de Grenoble et Institut national polytechnique de Grenoble"},{"key":"31_CR8","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Bentele, M., Dietsch, D., Jiang, X., Klumpp, D., Sch\u00fcssele, F., Podelski, A.: Ultimate Automizer and the abstraction of bitwise operations (competition contribution). In: Proc. TACAS\u00a0(3), pp. 418\u2013423, LNCS\u00a014572, Springer (2024), https:\/\/doi.org\/10.1007\/978-3-031-57256-2_31","DOI":"10.1007\/978-3-031-57256-2_31"},{"key":"31_CR9","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: CAV, pp. 661\u2013667, Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"31_CR10","doi-asserted-by":"publisher","unstructured":"Journault, M., Min\u00e9, A., Monat, R., Ouadjaout, A.: Combinations of reusable abstract domains for a multilingual static analyzer. In: VSTTE, pp. 1\u201318 (2019), https:\/\/doi.org\/10.1007\/978-3-030-41600-3_1","DOI":"10.1007\/978-3-030-41600-3_1"},{"key":"31_CR11","doi-asserted-by":"publisher","unstructured":"Lin, Y., Chen, Z., Wang, J.: AISE v2.0: Combining loop transformations (competition contribution). In: Proc. TACAS\u00a0(3), pp. 199\u2013204, LNCS\u00a015698, Springer (2025), https:\/\/doi.org\/10.1007\/978-3-031-90660-2_12","DOI":"10.1007\/978-3-031-90660-2_12"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Mansur, M.N., Mariano, B., Christakis, M., Navas, J.A., W\u00fcstholz, V.: Automatically tailoring abstract interpretation to custom usage scenarios. In: CAV (2), Lecture Notes in Computer Science, vol. 12760, pp. 777\u2013800, Springer (2021)","DOI":"10.1007\/978-3-030-81688-9_36"},{"key":"31_CR13","doi-asserted-by":"publisher","unstructured":"Menezes, R., Aldughaim, M., Farias, B., Li, X., Manino, E., Shmarov, F., Song, K., Brau\u00dfe, F., Gadelha, M.R., Tihanyi, N., Korovin, K., Cordeiro, L.: ESBMC v7.4: Harnessing the power of intervals (competition contribution). In: Proc. TACAS\u00a0(3), pp. 376\u2013380, LNCS\u00a014572, Springer (2024), https:\/\/doi.org\/10.1007\/978-3-031-57256-2_24","DOI":"10.1007\/978-3-031-57256-2_24"},{"key":"31_CR14","doi-asserted-by":"crossref","unstructured":"Milanese, M., Min\u00e9, A.: Generation of Violation Witnesses by Under-Approximating Abstract Interpretation. In: VMCAI, Springer (2024)","DOI":"10.1007\/978-3-031-50524-9_3"},{"key":"31_CR15","unstructured":"Milanese, M., Min\u00e9, A.: Under-approximating memory abstractions. In: Proc.\u00a0of the 31th International Static Analysis Symposium (SAS\u201924), Lecture Notes in Computer Science (LNCS), vol. 14995, Springer (Oct 2024), http:\/\/www-apr.lip6.fr\/~mine\/publi\/article-milanese-al-sas24.pdf"},{"key":"31_CR16","doi-asserted-by":"publisher","unstructured":"Milanese, M., Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa at sv-comp 2026 (Nov 2025), https:\/\/doi.org\/10.5281\/zenodo.17696794","DOI":"10.5281\/zenodo.17696794"},{"key":"31_CR17","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program. 93, 154\u2013182 (2014), https:\/\/doi.org\/10.1016\/J.SCICO.2013.09.014, URL https:\/\/doi.org\/10.1016\/j.scico.2013.09.014","DOI":"10.1016\/J.SCICO.2013.09.014"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Relational thread-modular static value analysis by abstract interpretation. In: VMCAI, Lecture Notes in Computer Science, vol. 8318, pp. 39\u201358, Springer (2014)","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"31_CR19","unstructured":"Monat, R.: Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries. Ph.D. thesis, Sorbonne Universit\u00e9, France (2021)"},{"key":"31_CR20","doi-asserted-by":"publisher","unstructured":"Monat, R., Milanese, M., Parolini, F., Boillot, J., Ouadjaout, A., Min\u00e9, A.: Mopsa-C: Improved verification for C programs, simple validation of correctness witnesses (competition contribution). In: Proc. TACAS\u00a0(3), pp. 387\u2013392, LNCS\u00a014572, Springer (2024), https:\/\/doi.org\/10.1007\/978-3-031-57256-2_26","DOI":"10.1007\/978-3-031-57256-2_26"},{"key":"31_CR21","doi-asserted-by":"publisher","unstructured":"Monat, R., Min\u00e9, A.: Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10145, pp. 386\u2013404, Springer (2017), https:\/\/doi.org\/10.1007\/978-3-319-52234-0_21, URL https:\/\/doi.org\/10.1007\/978-3-319-52234-0_21","DOI":"10.1007\/978-3-319-52234-0_21"},{"key":"31_CR22","doi-asserted-by":"publisher","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa-C: Modular domains and relational abstract interpretation for C programs (competition contribution). In: Proc. TACAS\u00a0(2), pp. 565\u2013570, LNCS\u00a013994, Springer (2023), https:\/\/doi.org\/10.1007\/978-3-031-30820-8_37","DOI":"10.1007\/978-3-031-30820-8_37"},{"key":"31_CR23","doi-asserted-by":"publisher","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa-C with trace partitioning and autosuggestions (competition contribution). In: Proc. TACAS\u00a0(3), pp. 229\u2013235, LNCS\u00a015698, Springer (2025), https:\/\/doi.org\/10.1007\/978-3-031-90660-2_17","DOI":"10.1007\/978-3-031-90660-2_17"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"Moussaoui\u00a0Remil, N., Urban, C.: Termination Resilience Static Analysis. In: VMCAI 2026 - 27th International Conference on Verification, Model Checking, and Abstract Interpretation, Rennes, France (Jan 2026), URL https:\/\/inria.hal.science\/hal-05398150","DOI":"10.1007\/978-3-032-15700-3_11"},{"key":"31_CR25","doi-asserted-by":"publisher","unstructured":"Mukhopadhyay, D., Metta, R., Karmarkar, H., Madhukar, K.: PROTON\u00a02.1: Synthesizing ranking functions via fine-tuned locally hosted LLM (competition contribution). In: Proc. TACAS\u00a0(3), pp. 242\u2013247, LNCS\u00a015698, Springer (2025), https:\/\/doi.org\/10.1007\/978-3-031-90660-2_19","DOI":"10.1007\/978-3-031-90660-2_19"},{"key":"31_CR26","doi-asserted-by":"crossref","unstructured":"Oh, H., Lee, W., Heo, K., Yang, H., Yi, K.: Selective context-sensitivity guided by impact pre-analysis. In: PLDI, pp. 475\u2013484, ACM (2014)","DOI":"10.1145\/2594291.2594318"},{"key":"31_CR27","doi-asserted-by":"publisher","unstructured":"Ouadjaout, A., Min\u00e9, A.: A library modeling language for the static analysis of C programs. In: SAS, pp. 223\u2013247 (2020), https:\/\/doi.org\/10.1007\/978-3-030-65474-0_11","DOI":"10.1007\/978-3-030-65474-0_11"},{"key":"31_CR28","unstructured":"Ouadjaout, A., Monat, R., Min\u00e9, A., Journault, M.: Mopsa (2022), URL https:\/\/gitlab.com\/mopsa\/mopsa-analyzer"},{"key":"31_CR29","doi-asserted-by":"publisher","unstructured":"Saan, S.: Sv-sanitizers in sv-comp 2026 (Oct 2025), https:\/\/doi.org\/10.5281\/zenodo.17400380, URL https:\/\/doi.org\/10.5281\/zenodo.17400380","DOI":"10.5281\/zenodo.17400380"},{"key":"31_CR30","unstructured":"Saan, S.: Sv-sanitizers: Sv-comp wrapper for sanitizers (Dec 2025), URL https:\/\/github.com\/sim642\/sv-sanitizers"},{"key":"31_CR31","doi-asserted-by":"publisher","unstructured":"Saan, S., Erhard, J., Schwarz, M., Bozhilov, S., Holter, K., Tilscher, S., Vojdani, V., Seidl, H.: Goblint: Abstract interpretation for memory safety and termination - (competition contribution). In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, Lecture Notes in Computer Science, vol. 14572, pp. 381\u2013386, Springer (2024), https:\/\/doi.org\/10.1007\/978-3-031-57256-2_25, URL https:\/\/doi.org\/10.1007\/978-3-031-57256-2_25","DOI":"10.1007\/978-3-031-57256-2_25"},{"key":"31_CR32","doi-asserted-by":"publisher","unstructured":"Suzanne, T., Min\u00e9, A.: Relational thread-modular abstract interpretation under relaxed memory models. In: Ryu, S. (ed.) Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, Lecture Notes in Computer Science, vol. 11275, pp. 109\u2013128, Springer (2018), https:\/\/doi.org\/10.1007\/978-3-030-02768-1_6, URL https:\/\/doi.org\/10.1007\/978-3-030-02768-1_6","DOI":"10.1007\/978-3-030-02768-1_6"},{"key":"31_CR33","doi-asserted-by":"publisher","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: M\u00fcller-Olm, M., Seidl, H. (eds.) Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, Lecture Notes in Computer Science, vol. 8723, pp. 302\u2013318, Springer (2014), https:\/\/doi.org\/10.1007\/978-3-319-10936-7_19, URL https:\/\/doi.org\/10.1007\/978-3-319-10936-7_19","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"31_CR34","doi-asserted-by":"crossref","unstructured":"Vojdani, V., Apinis, K., R\u00f5tov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the goblint approach. In: ASE, pp. 391\u2013402, ACM (2016)","DOI":"10.1145\/2970276.2970337"},{"key":"31_CR35","doi-asserted-by":"crossref","unstructured":"Wang, Z., Yang, L., Chen, M., Bu, Y., Li, Z., Wang, Q., Qin, S., Yi, X., Yin, J.: Parf: Adaptive parameter refining for abstract interpretation. In: ASE, pp. 1082\u20131093 (2024)","DOI":"10.1145\/3691620.3695487"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22749-2_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:09:39Z","timestamp":1776258579000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}