Correctness Witness Validation by Abstract Interpretation

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

doi:10.1007/978-3-031-50524-9_4

Correctness Witness Validation by Abstract Interpretation

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

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

4 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 language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings
Editors	Rayna Dimitrova, Ori Lahav, Sebastian Wolff
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	74-97
Number of pages	24
ISBN (Print)	9783031505232
DOIs	https://doi.org/10.1007/978-3-031-50524-9_4
State	Published - 2024
Event	25th 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 2024 → 16 Jan 2024

Publication series

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

Conference

Conference	25th 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/Territory	United Kingdom
City	London
Period	15/01/24 → 16/01/24

Keywords

Abstract Interpretation
Correctness Witness
Program Analysis
Software Verification
Witness Validation

Access to Document

10.1007/978-3-031-50524-9_4

Cite this

Saan, S., Schwarz, M., Erhard, J., Seidl, H., Tilscher, S., & Vojdani, V. (2024). Correctness Witness Validation by Abstract Interpretation. In R. Dimitrova, O. Lahav, & S. Wolff (Eds.), Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings (pp. 74-97). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14499 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-50524-9_4

Saan, Simmo ; Schwarz, Michael ; Erhard, Julian et al. / Correctness Witness Validation by Abstract Interpretation. Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings. editor / Rayna Dimitrova ; Ori Lahav ; Sebastian Wolff. Springer Science and Business Media Deutschland GmbH, 2024. pp. 74-97 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{247acb77ea9346d5873df200bcf5c4e4,

title = "Correctness Witness Validation by Abstract Interpretation",

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.",

keywords = "Abstract Interpretation, Correctness Witness, Program Analysis, Software Verification, Witness Validation",

author = "Simmo Saan and Michael Schwarz and Julian Erhard and Helmut Seidl and Sarah Tilscher and Vesal Vojdani",

note = "Publisher Copyright: {\textcopyright} 2024, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 25th 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 ; Conference date: 15-01-2024 Through 16-01-2024",

year = "2024",

doi = "10.1007/978-3-031-50524-9_4",

language = "English",

isbn = "9783031505232",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "74--97",

editor = "Rayna Dimitrova and Ori Lahav and Sebastian Wolff",

booktitle = "Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings",

}

Saan, S, Schwarz, M, Erhard, J, Seidl, H, Tilscher, S & Vojdani, V 2024, Correctness Witness Validation by Abstract Interpretation. in R Dimitrova, O Lahav & S Wolff (eds), Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14499 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 74-97, 25th 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, 15/01/24. https://doi.org/10.1007/978-3-031-50524-9_4

Correctness Witness Validation by Abstract Interpretation. / Saan, Simmo; Schwarz, Michael; Erhard, Julian et al.
Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings. ed. / Rayna Dimitrova; Ori Lahav; Sebastian Wolff. Springer Science and Business Media Deutschland GmbH, 2024. p. 74-97 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14499 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Correctness Witness Validation by Abstract Interpretation

AU - Saan, Simmo

AU - Schwarz, Michael

AU - Erhard, Julian

AU - Seidl, Helmut

AU - Tilscher, Sarah

AU - Vojdani, Vesal

PY - 2024

Y1 - 2024

N2 - 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.

AB - 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.

KW - Abstract Interpretation

KW - Correctness Witness

KW - Program Analysis

KW - Software Verification

KW - Witness Validation

UR - http://www.scopus.com/inward/record.url?scp=85181976499&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-50524-9_4

DO - 10.1007/978-3-031-50524-9_4

M3 - Conference contribution

AN - SCOPUS:85181976499

SN - 9783031505232

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 74

EP - 97

BT - Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings

A2 - Dimitrova, Rayna

A2 - Lahav, Ori

A2 - Wolff, Sebastian

PB - Springer Science and Business Media Deutschland GmbH

T2 - 25th 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

Y2 - 15 January 2024 through 16 January 2024

ER -

Saan S, Schwarz M, Erhard J, Seidl H, Tilscher S, Vojdani V. Correctness Witness Validation by Abstract Interpretation. In Dimitrova R, Lahav O, Wolff S, editors, Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Proceedings. Springer Science and Business Media Deutschland GmbH. 2024. p. 74-97. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-50524-9_4