---

Abstract

When verifiers report an alarm, they export a violation witness that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.

---

Tool and Reproduction Information

A reproduction package of this work is available on Zenodo (). The implementation of Flow can be found in our Git repository. The implementation of FaultY is part of CPAchecker. A tutorial explaining the usage and the features of FaultY is archived on Zenodo ()

---

Full Results

The experimental results reported in the paper can be found here. Under each research question, you can find the plots and tables that are referenced in the paper. The plots and tables are generated from the raw data that can be found in our reproduction package. We also include all validators and omitted plots here.

• RQ1: Witness Reduction

Choose a reduction strategy: Always Match State Control

• RQ2: Confirmation Rate

Choose a reduction strategy: Always Match State Control
Choose the validator: CPAchecker Metaval SymbioticWitch UAutomizer

• RQ3: Reduction Variants

Choose a reduction strategy: Always Match State Control