{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T23:30:15Z","timestamp":1759879815146,"version":"3.40.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906596"},{"type":"electronic","value":"9783031906602"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present advances we brought to Mopsa for SV-Comp 2025. Most notably, Mopsa now supports bounded trace partitioning, constant widening with thresholds, and can check that all memory has been correctly deallocated. Further, Mopsa now integrates a sound support of bitfields. While Mopsa at SV-Comp previously relied on a fixed, homogeneous set of configurations to verify tasks, it can now automatically leverage semantic information from a previous analysis to trigger heuristic precision improvements in further analyses. With these improvements, Mopsa wins a silver medal in the <jats:italic>SoftwareSystems<\/jats:italic> category and ranks fifth in the <jats:italic>NoOverflows<\/jats:italic> category.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_17","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:04Z","timestamp":1746005884000},"page":"229-235","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Mopsa-C with Trace Partitioning and Autosuggestions (Competition Contribution)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8487-0326","authenticated-orcid":false,"given":"Rapha\u00ebl","family":"Monat","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7248-5914","authenticated-orcid":false,"given":"Abdelraouf","family":"Ouadjaout","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-3179","authenticated-orcid":false,"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"17_CR1","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":"17_CR2","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.W.: Recency-abstraction for heap-allocated storage. In: SAS, Lecture Notes in Computer Science, vol. 4134, pp. 221\u2013239, Springer (2006)","DOI":"10.1007\/11823230_15"},{"key":"17_CR3","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":"17_CR4","doi-asserted-by":"crossref","unstructured":"Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. Foundations and Trends in Programming Languages pp. 71\u2013190 (2015)","DOI":"10.1561\/2500000002"},{"key":"17_CR5","unstructured":"Beyer, D., Strej\u010dek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proc. TACAS, LNCS, Springer (2025)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Henzinger, T.A.: Bubaak: Runtime monitoring of program verifiers - (competition contribution). In: TACAS (2), Lecture Notes in Computer Science, vol. 13994, pp. 535\u2013540, Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_32"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Chalupa, M., Richter, C.: Bubaak-split: Split what you cannot verify (competition contribution). In: TACAS (3), Lecture Notes in Computer Science, vol. 14572, pp. 353\u2013358, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_20"},{"key":"17_CR8","unstructured":"Chalupa, M., Richter, C.: Bubaak: Dynamic cooperative verification (competition contribution). In: Proc. TACAS, LNCS, Springer (2025)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Dietsch, D., Heizmann, M., Klumpp, D., Sch\u00fcssele, F., Podelski, A.: Ultimate taipan and race detection in ultimate - (competition contribution). In: TACAS (2), Lecture Notes in Computer Science, vol. 13994, pp. 582\u2013587, Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_40"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Barth, M., Dietsch, D., Fichtner, L., Hoenicke, J., Klumpp, D., Naouar, M., Schindler, T., Sch\u00fcssele, F., Podelski, A.: Ultimate automizer and the commuhash normal form - (competition contribution). In: TACAS (2), Lecture Notes in Computer Science, vol. 13994, pp. 577\u2013581, Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_39"},{"key":"17_CR12","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":"17_CR13","doi-asserted-by":"crossref","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)","DOI":"10.1007\/978-3-030-41600-3_1"},{"key":"17_CR14","unstructured":"Lin, Y., Chen, Z., Wang, J.: AISE v2.0: Combining loop transformations (competition contribution). In: Proc. TACAS, LNCS, Springer (2025)"},{"key":"17_CR15","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":"17_CR16","doi-asserted-by":"crossref","unstructured":"Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: ESOP, Lecture Notes in Computer Science, vol. 3444, pp. 5\u201320, Springer (2005)","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"17_CR17","unstructured":"McGowan, C., Richards, M., Sui, Y.: SVF-SVC: Software verification using SVF (competition contribution). In: Proc. TACAS, LNCS, Springer (2025)"},{"key":"17_CR18","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":"17_CR19","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":"17_CR20","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: LCTES (2006)","DOI":"10.1145\/1134650.1134659"},{"key":"17_CR21","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":"17_CR22","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":"17_CR23","doi-asserted-by":"crossref","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: TACAS (3), Lecture Notes in Computer Science, vol. 14572, pp. 387\u2013392, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_26"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa-c: Modular domains and relational abstract interpretation for C programs (competition contribution). In: TACAS (2), Lecture Notes in Computer Science, vol. 13994, pp. 565\u2013570, Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_37"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa at sv-comp 2025 (Nov 2024), https:\/\/doi.org\/10.5281\/zenodo.14208644","DOI":"10.5281\/zenodo.14208644"},{"key":"17_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":"17_CR27","doi-asserted-by":"crossref","unstructured":"Ouadjaout, A., Min\u00e9, A.: A library modeling language for the static analysis of C programs. In: SAS, pp. 223\u2013247 (2020)","DOI":"10.1007\/978-3-030-65474-0_11"},{"key":"17_CR28","unstructured":"Ouadjaout, A., Monat, R., Min\u00e9, A., Journault, M.: Mopsa (2022), URL https:\/\/gitlab.com\/mopsa\/mopsa-analyzer"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Peringer, P., Sokov\u00e1, V., Vojnar, T.: Predatorhp revamped (not only) for interval-sized memory regions and memory reallocation (competition contribution). In: TACAS (2), Lecture Notes in Computer Science, vol. 12079, pp. 408\u2013412, Springer (2020)","DOI":"10.1007\/978-3-030-45237-7_30"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Saan, S., Schwarz, M., Apinis, K., Erhard, J., Seidl, H., Vogler, R., Vojdani, V.: Goblint: Thread-modular abstract interpretation using side-effecting constraints - (competition contribution). In: TACAS (2021)","DOI":"10.1007\/978-3-030-72013-1_28"},{"key":"17_CR31","doi-asserted-by":"crossref","unstructured":"Urban, C.: Function: An abstract domain functor for termination - (competition contribution). In: TACAS, Lecture Notes in Computer Science, vol. 9035, pp. 464\u2013466, Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_46"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: SAS, Lecture Notes in Computer Science, vol. 8723, pp. 302\u2013318, Springer (2014)","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"17_CR33","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":"17_CR34","doi-asserted-by":"crossref","unstructured":"Wang, Z., Chen, Z.: AISE: A symbolic verifier by synergizing abstract interpretation and symbolic execution (competition contribution). In: TACAS (3), Lecture Notes in Computer Science, vol. 14572, pp. 347\u2013352, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_19"},{"key":"17_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-031-90660-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:20Z","timestamp":1746005900000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","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":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}