Software verification is a resource-intensive process that combines automated program analysis with manual evaluation of results. While modern methodologies and cloud technologies have expedited the automated phase, manual analysis remains a critical bottleneck, particularly for large-scale software systems, due to the need for specialized developer expertise. Verification results often include warnings about potential bugs, which must be either fixed or classified as false alarms, and correctness proofs intended to demonstrate the absence of defects. This paper addresses these challenges by formally introducing the concept of witness thoroughness in software verification. We evaluate this concept using results from tools that participated in the Competition on Software Verification, demonstrating its practical applicability to real-world verification benchmarks. Furthermore, we show how witness thoroughness can serve as a meaningful metric for comparing verification tools and provide recommendations to improve validation rates. Finally, we identify which error trace elements are essential for effective visualization of witnesses.
Мордань et al. (Sun,) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: