
Fault Localization on Witnesses Article Abstract When verifiers report an alarm, they export a violation witness (exchangeable counterexample)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 witnesseswith information that makes validation unnecessarily difficult.To check our hypothesis, we reduce violation witnesses to that informationthat automated fault-localization approaches deem relevant for triggering the reported alarm in the program.We perform a large experimental evaluation on the witnessesproduced in the International Competition on Software Verification (SV-COMP 2023).It shows that our reduction shrinks the witnesses considerablyand enables the confirmation of verification results that were not confirmable before. VM The username for the VM is `vagrant`.The password for the VM is `vagrant`. System Requirements The artifact requires 4 CPU cores and 8 GB of RAM. To inspect the data, we require at least 150GB of empty disk space to run the VM.To reproduce the results, we require 155GB.To run the full reproduction, we require 300GB. The VM was tested on Ubuntu with Virtual Box Version 7.0.10 r158379 (Qt5.15.3). Reproduction Import the VM to VirtualBox and start it.We provide symbolic links to the reproduction directory on the Desktop.Please follow the instructions in the `ReadMe.md` inside the VM (located at `~/fault-localization-witnesses/ReadMe.md`).The upcoming three subsections serve as a quick-start guide for our artifact. Reproduce the Example To reproduce the example in our paper, navigate to `~/fault-localization-witnesses` and execute `./example.sh`. Reproduce the Plots Execute `./reproduce.sh` from `~/fault-localization-witnesses/` to reproduce our experiments.
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
