Mopsa-C: Towards Incorrectness and Termination Verdicts (Competition Contribution)

We present advances we brought to Mopsa for SV-COMP 2026. Mopsa now supports a backward analysis mode which computes an under-approximation of the weakest liberal precondition for the alarms found during a verification pass, which generates an input harness to reproduce the incorrectness condition. We also added support for termination checking through the introduction of loop counters. With these improvements, Mopsa wins the SoftwareSystems category, and ranks third in the TrueOverall category.