Marco Milanese 0001

dblp:285/8907-1 · DBLP profile ↗
← Back
5ranked-venue papers
4as first author
5since 2021 · last 2026
0000-0002-6215-7359ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 5 · 4 first-author · 5 since 2021
YearPublicationVenuePosition
2026 Mopsa-C: Towards Incorrectness and Termination Verdicts (Competition Contribution)
Marco Milanese 0001, Raphaël Monat, Abdelraouf Ouadjaout, Antoine Miné
TACAS (2)1
2024 Under-Approximating Memory Abstractions
Marco Milanese 0001, Antoine Miné
SAS1
2024 Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)
abstract
Abstract 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’sSoftwareSystemscategory by a large margin, scoring 2.5 times more points than the silver medalist, Bubaak-SpLit.
Raphaël Monat, Marco Milanese 0001, Francesco Parolini, Jérôme Boillot, Abdelraouf Ouadjaout, Antoine Miné
TACAS (3)2
2024 Generation of Violation Witnesses by Under-Approximating Abstract Interpretation
Marco Milanese 0001, Antoine Miné
VMCAI (1)1
2022 Local Completeness Logic on Kleene Algebra with Tests
Marco Milanese 0001, Francesco Ranzato
SAS1