Evaluating Key Elements of Error Traces in Static Software Verification (in Russian)

Software verification is a resource-intensive process that combines automatic program analysis with manual analysis of verification results. While recent advances in verification techniques and cloud-based infrastructures have significantly accelerated the automatic phase, manual analysis remains a critical bottleneck, particularly for large-scale software systems, due to the need for specialized developer expertise. Verification results typically include warnings about potential bugs, which must either be fixed or classified as false positives.

In this work, we address this challenge by introducing a formal notion of thoroughness for error traces in the context of software verification. We define thoroughness as a measure of how comprehensively an error trace captures the essential elements required to understand and validate a reported issue. To evaluate this concept in practice, we apply it to verification results produced by tools participating in the Software Verification Competition (SV-COMP). Our analysis shows that the proposed metric is both feasible and informative in real-world verification scenarios.

Furthermore, we argue that thoroughness can serve as a meaningful metric for comparing verification tools by revealing strengths and weaknesses in how potential errors are represented. The metric also supports improvements in automated validation processes. In addition, our evaluation demonstrates how thoroughness can be used to identify which specific elements must be present in an error trace to enable effective visualization. By identifying these key elements, we aim to facilitate more efficient manual analysis and encourage the development of more user-friendly verification tools.