Reproduction Package for ICSE 2024 Submission `Fault Localization on Verification Witnesses'

This package is a reproduction package for our ICSE 2024 submission "Fault Localization on Verification Witnesses". This artifact requires at least 2 CPU cores, 8 GB of RAM, and about 150 GB of disk space. The README on the Desktop contains all further instructions. VM username: vagrant VM password: vagrant The VM was tested on Ubuntu with Virtual Box Version 7.0.10 r158379 (Qt5.15.3). Article Abstract: Formal verification has the potential to prove software safe, but suffers from trust issues. Because most formal-verification techniques make a trade-off between precision and resource consumption, they produce false alarms. These reduce the confidence in the verification result. To mitigate this issue, state-of-the-art verifiers export violation witnesses that help independent validators to confirm a reported property violation. It is assumed that these violation witnesses are helpful if they are very precise: ideally, they should describe a single program path for the validator to check. We claim that this leads verifiers to produce large, detailed witnesses that include a lot of unnecessary information. To check our hypothesis, we reduce violation witnesses through automated fault localization: Given a witness as input, we reduce the witness to only that information that fault localization deems relevant for reaching a property violation in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification 2023 to explore the effect of this reduction. Our experiments show that the reduced witnesses shrink considerably. In addition, the confirmation rate of validators can grow: The run time to confirm our reduced witnesses decreases on average, and witnesses that were not confirmed before can be confirmed after reduction.