Software Verification Witnesses Thoroughness.

Saved in:
Bibliographic Details
Title: Software Verification Witnesses Thoroughness.
Authors: Mordan, V. O.1 (AUTHOR) mordan@ispras.ru, Mutilin, V. S.1,2 (AUTHOR) mutilin@ispras.ru
Source: Programming & Computer Software. Feb2026, Vol. 52 Issue 1, p39-49. 11p.
Subjects: Software verification, Computer software correctness, Software measurement, Software visualization, Defect tracking (Computer software development)
Abstract: 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. [ABSTRACT FROM AUTHOR]
Copyright of Programming & Computer Software is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract: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. [ABSTRACT FROM AUTHOR]
ISSN:03617688
DOI:10.1134/S0361768826700052