Fault Localization on Verification Witnesses (poster Paper)
ICSE-Companion '24 Proceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering Companion Proceedings(2024)
摘要
Verifiers export violation witnesses, which help independent valida-tors to confirm a reported specification violation. It is assumed that violation witnesses are helpful if they are very precise: ideally, they should describe a single program path for the validator to check. But we claim that this leads verifiers to produce large, detailed wit-nesses that include a lot of unnecessary information that actually hinders validation. We reduce violation witnesses with automated fault localization to only that information which fault localization suspects as fault. We performed a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023) to explore the effect of our reduction. Our experiments show that the witnesses reduced using our approach shrink considerably and can be confirmed better.
更多查看译文
关键词
Software Verification,Program Analysis,Result Validation,Fault Localization,Violation Witnesses,Error Paths
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要