{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T01:35:10Z","timestamp":1768268110739,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308192","type":"print"},{"value":"9783031308208","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Mopsa is a multilanguage static analysis platform relying on abstract interpretation. It is able to analyze C, Python, and programs mixing these two languages; we focus on the C analysis here. It provides a novel way to combine abstract domains, in order to offer extensibility and cooperation between them, which is especially beneficial when relational numerical domains are used. The analyses are currently flow-sensitive and fully context-sensitive. We focus only on proving programs to be correct, as our analyses are designed to be sound and terminating but not complete. We present our first participation to SV-Comp, where Mopsa earned a bronze medal in the <jats:italic>SoftwareSystems<\/jats:italic> category.\n<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_37","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"565-570","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (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":[[2023,4,20]]},"reference":[{"key":"37_CR1","doi-asserted-by":"crossref","unstructured":"Bau, G., Min\u00e9, A., Botbol, V., Bouaziz, M.: Abstract interpretation of michelson smart-contracts. In: ACM SOAP, pp. 36\u201343 (2022)","DOI":"10.1145\/3520313.3534660"},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Proc. TACAS\u00a0(2), LNCS\u00a0, Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"37_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Verifiers and validators of the 12th Intl. Competition on Software Verification (SV-COMP 2023) (2023), https:\/\/doi.org\/10.5281\/zenodo.7627829","DOI":"10.5281\/zenodo.7627829"},{"key":"37_CR4","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":"37_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Combination of abstractions in the Astr\u00e9e static analyzer. In: ASIAN, pp. 272\u2013300 (2006)","DOI":"10.1007\/978-3-540-77505-8_23"},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C - A software analysis perspective. In: SEFM, pp. 233\u2013247 (2012)","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"37_CR7","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":"37_CR8","doi-asserted-by":"crossref","unstructured":"Jensen, S.H., M\u00f8ller, A., Thiemann, P.: Type analysis for JavaScript. In: SAS, pp. 238\u2013255 (2009)","DOI":"10.1007\/978-3-642-03237-0_17"},{"key":"37_CR9","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":"37_CR10","doi-asserted-by":"crossref","unstructured":"Journault, M., Min\u00e9, A., Ouadjaout, A.: Modular static analysis of string manipulations in C programs. In: SAS, pp. 243\u2013262 (2018)","DOI":"10.1007\/978-3-319-99725-4_16"},{"key":"37_CR11","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":"37_CR12","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":"37_CR13","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Static type analysis by abstract interpretation of python programs. In: ECOOP, pp. 1\u201329 (2020)"},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: A multilanguage static analysis of python programs with native C extensions. In: SAS, pp. 323\u2013345 (2021)","DOI":"10.1007\/978-3-030-88806-0_16"},{"key":"37_CR15","doi-asserted-by":"publisher","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Artefact) (Dec 2022), https:\/\/doi.org\/10.5281\/zenodo.7467136","DOI":"10.5281\/zenodo.7467136"},{"key":"37_CR16","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":"37_CR17","unstructured":"Ouadjaout, A., Monat, R., Min\u00e9, A., Journault, M.: Mopsa (2022), https:\/\/gitlab.com\/mopsa\/mopsa-analyzer"},{"key":"37_CR18","unstructured":"Saan, S.: Witness generation for data-flow analysis. https:\/\/comserv.cs.ut.ee\/home\/files\/saan_computerscience_2020.pdf (2020)"},{"key":"37_CR19","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":"37_CR20","doi-asserted-by":"crossref","unstructured":"Saan, S., Schwarz, M., Erhard, J., Pietsch, M., Seidl, H., Tilscher, S., Vojdani, V.: Goblint: Autotuning thread-modular abstract interpretation (competition contribution). In: Proc. TACAS\u00a0(2), LNCS\u00a0, Springer (2023)","DOI":"10.1007\/978-3-031-30820-8_34"},{"key":"37_CR21","unstructured":"The OCaml Developers: Ocaml (2020), https:\/\/github.com\/ocaml\/ocaml"}],"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-30820-8_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:07:25Z","timestamp":1690974445000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","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":"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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}