Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Marco Milanese,
  • Raphaël Monat,
  • Abdelraouf Ouadjaout,
  • Antoine Miné

摘要

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.