View in EDS

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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 194006115
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Software Verification Witnesses Thoroughness.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Mordan%2C+V%2E+O%2E%22">Mordan, V. O.</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> mordan@ispras.ru</i><br /><searchLink fieldCode="AR" term="%22Mutilin%2C+V%2E+S%2E%22">Mutilin, V. S.</searchLink><relatesTo>1,2</relatesTo> (AUTHOR)<i> mutilin@ispras.ru</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Programming+%26+Computer+Software%22">Programming & Computer Software</searchLink>. Feb2026, Vol. 52 Issue 1, p39-49. 11p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+correctness%22">Computer software correctness</searchLink><br /><searchLink fieldCode="DE" term="%22Software+measurement%22">Software measurement</searchLink><br /><searchLink fieldCode="DE" term="%22Software+visualization%22">Software visualization</searchLink><br /><searchLink fieldCode="DE" term="%22Defect+tracking+%28Computer+software+development%29%22">Defect tracking (Computer software development)</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=194006115
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1134/S0361768826700052
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 11
        StartPage: 39
    Subjects:
      – SubjectFull: Software verification
        Type: general
      – SubjectFull: Computer software correctness
        Type: general
      – SubjectFull: Software measurement
        Type: general
      – SubjectFull: Software visualization
        Type: general
      – SubjectFull: Defect tracking (Computer software development)
        Type: general
    Titles:
      – TitleFull: Software Verification Witnesses Thoroughness.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Mordan, V. O.
      – PersonEntity:
          Name:
            NameFull: Mutilin, V. S.
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 02
              Text: Feb2026
              Type: published
              Y: 2026
          Identifiers:
            – Type: issn-print
              Value: 03617688
          Numbering:
            – Type: volume
              Value: 52
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Programming & Computer Software
              Type: main
ResultId 1