Mopsa-C: Improved Verification for C ...
Document type :
Communication dans un congrès avec actes
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]
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
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
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 >
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 :
Source :
Files
- document
- Open access
- Access the document
- 978-3-031-57256-2_26.pdf
- Open access
- Access the document
- document
- Open access
- Access the document
- 978-3-031-57256-2_26.pdf
- Open access
- Access the document