Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)
Raphaël Monat, Marco Milanese, Francesco Parolini, Jérôme Boillot, Abdelraouf Ouadjaout, Antoine Miné
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’s SoftwareSystems category by a large margin, scoring 2.5 times more points than the silver medalist, Bubaak-SpLit.
Topics & Concepts
ValidatorCorrectnessComputer scienceWitnessSimple (philosophy)Programming languageMargin (machine learning)Integer (computer science)Competition (biology)Theoretical computer scienceMachine learningWorld Wide WebPhilosophyEpistemologyEcologyBiologySoftware Testing and Debugging TechniquesSecurity and Verification in ComputingFormal Methods in Verification