Correctness Witness Validation by Abstract Interpretation

Simmo Saan, Michael Schwarz, Julian Erhard, Helmut Seidl, Sarah Tilscher, Vesal Vojdani

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

2 Scopus citations

Abstract

Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into the abstract program state. Given suitable invariants, the unassume operation can accelerate fixpoint convergence and yield more precise results. We demonstrate the feasibility of this approach by augmenting an abstract interpreter with unassume operators and evaluating the impact of incorporating witnesses on performance and precision. Using manually crafted witnesses, we can confirm verification results for multi-threaded programs with a reduction in effort ranging from 7% to 47% in CPU time. More intriguingly, we discover that using witnesses from model checkers can guide our analyzer to verify program properties that it could not verify on its own.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings
EditorsRayna Dimitrova, Ori Lahav, Sebastian Wolff
PublisherSpringer Science and Business Media Deutschland GmbH
Pages74-97
Number of pages24
ISBN (Print)9783031505232
DOIs
StatePublished - 2024
Event25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024 was co-located with 51st ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2024 - London, United Kingdom
Duration: 15 Jan 202416 Jan 2024

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14499 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024 was co-located with 51st ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2024
Country/TerritoryUnited Kingdom
CityLondon
Period15/01/2416/01/24

Keywords

  • Abstract Interpretation
  • Correctness Witness
  • Program Analysis
  • Software Verification
  • Witness Validation

Fingerprint

Dive into the research topics of 'Correctness Witness Validation by Abstract Interpretation'. Together they form a unique fingerprint.

Cite this