Abstract <p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Software Verification Witnesses Thoroughness

  • V. O. Mordan,
  • V. S. Mutilin

摘要

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.