Titre :

Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)

Auteur(s) :

Monat, Raphaël [Auteur]
Analyse symbolique et conception orientée composants pour des systèmes embarqués temps-réel modulaires [SYCOMORES]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Milanese, Marco [Auteur]
Algorithmes, Programmes et Résolution [APR]
Parolini, Francesco [Auteur]
Algorithmes, Programmes et Résolution [APR]
Boillot, Jérôme [Auteur]
Analyse Statique par Interprétation Abstraite [ANTIQUE]
Ouadjaout, Abdelraouf [Auteur]
Miné, Antoine [Auteur]
Algorithmes, Programmes et Résolution [APR]

Éditeur(s) ou directeur(s) scientifique(s) :

B. Finkbeiner
L. Kovács

Titre de la manifestation scientifique :

Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2024

Ville :

Luxembourg City

Pays :

Luxembourg

Date de début de la manifestation scientifique :

2024-04-06

Titre de la revue :

Lecture Notes in Computer Science

Éditeur :

Springer Nature Switzerland

Lieu de publication :

Cham

Date de publication :

2024

Mot(s)-clé(s) en anglais :

Static Analysis
Abstract Interpretation
Competition on Software Verification
SV-Comp

Discipline(s) HAL :

Informatique [cs]/Langage de programmation [cs.PL]

Résumé en anglais : [en]

We present advances we brought to Mopsa for SV-Comp 2024. We significantly improved the precision of our verifier in the presence of dynamic memory allocation, library calls such as , -based loops, and integer abstractions. ...
Lire la suite >We present advances we brought to Mopsa for SV-Comp 2024. We significantly improved the precision of our verifier in the presence of dynamic memory allocation, library calls such as , -based loops, and integer abstractions. We introduced a witness validator for correctness witnesses. Thanks to these improvements, Mopsa won SV-Comp’s SoftwareSystems category by a large margin, scoring 2.5 times more points than the silver medalist, Bubaak-SpLit.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL