Result: Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)

Title:
Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)
Authors:
Monat, Raphaël, Ouadjaout, Abdelraouf, Miné, Antoine
Contributors:
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires (SYCOMORES), Centre Inria de l'Université de Lille, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Algorithmes, Programmes et Résolution (APR), LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Source:
Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023). :565-570
Publisher Information:
CCSD; Springer, Cham, 2023.
Publication Year:
2023
Collection:
collection:CNRS
collection:INRIA
collection:INRIA-LILLE
collection:INRIA_TEST
collection:TESTALAIN1
collection:LIP6
collection:CRISTAL
collection:INRIA2
collection:UNIV-LILLE
collection:SORBONNE-UNIVERSITE
collection:SORBONNE-UNIV
collection:SU-SCIENCES
collection:SU-TI
collection:ALLIANCE-SU
collection:CRISTAL-SYCOMORES
collection:SUPRA_MATHS_INFO
Subject Terms:
Competition on software verification, SV-Comp, abstract interpretation, static analysis, [INFO.INFO-PL]Computer Science [cs], Programming Languages [cs.PL]
Subject Geographic:
Paris, France
Original Identifier:
HAL: hal-04077678
Document Type:
Conference conferenceObject<br />Conference papers
Language:
English
ISBN:
978-3-031-30820-8
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-031-30820-8_37
DOI:
10.1007/978-3-031-30820-8_37
Access URL:
https://inria.hal.science/hal-04077678
https://inria.hal.science/hal-04077678v1/document
https://inria.hal.science/hal-04077678v1/file/978-3-031-30820-8_37.pdf
Rights:
info:eu-repo/semantics/OpenAccess
URL: http://creativecommons.org/licenses/by/
Accession Number:
edshal.hal.04077678v1
Database:
HAL

Further Information

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 SoftwareSystems category.