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 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.
Fault Localization on Verification Witnesses
Lect.Notes Computer
International Symposium on Model Checking Software ; 2024 ; Luxembourg City, Luxembourg April 10, 2024 - April 11, 2024
2024-10-13
20 pages
Article/Chapter (Book)
Electronic Resource
English
British Library Conference Proceedings | 1994
|Finding witnesses using fewer random bits
TIBKAT | 1987
|PRINCIPAL ARTICLES - Training for expert witnesses
Online Contents | 1999
British Computer Society Advice for aspiring expert witnesses
British Library Online Contents | 2004