Title :

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

Author(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]

Scientific editor(s) :

B. Finkbeiner
L. Kovács

Conference title :

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

City :

Luxembourg City

Country :

Luxembourg

Start date of the conference :

2024-04-06

Journal title :

Lecture Notes in Computer Science

Publisher :

Springer Nature Switzerland

Publication place :

Cham

Publication date :

2024

English keyword(s) :

Static Analysis
Abstract Interpretation
Competition on Software Verification
SV-Comp

HAL domain(s) :

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

English abstract : [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. ...
Show more >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.Show less >

Language :

Anglais

Peer reviewed article :

Oui

Audience :

Internationale

Popular science :

Non

Collections :

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

Source :

Harvested from HAL