TY - GEN
T1 - Correctness Witnesses for Concurrent Programs
T2 - 26th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2025
AU - Erhard, Julian
AU - Bentele, Manuel
AU - Heizmann, Matthias
AU - Klumpp, Dominik
AU - Saan, Simmo
AU - Schüssele, Frank
AU - Schwarz, Michael
AU - Seidl, Helmut
AU - Tilscher, Sarah
AU - Vojdani, Vesal
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2025.
PY - 2025
Y1 - 2025
N2 - Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling independent validation of the reasoning by other tools. For the correctness of concurrent programs, no agreed-upon witness format exists—in no small part due to the divide between the semantics considered by analyzers, ranging from interleaving to thread-modular approaches, making it challenging to exchange information. We propose a format that leverages the well-known notion of ghosts to embed the claims a tool makes about a program into a modified program with ghosts, such that the validity of a witness can be decided by analyzing this program. Thus, the validity of witnesses with respect to the interleaving and the thread-modular semantics coincides. Further, thread-modular invariants computed by an abstract interpreter can naturally be expressed in the new format using ghost statements. We evaluate the approach by generating such ghost witnesses for a subset of concurrent programs from the SV-COMP benchmark suite, and pass them to a model checker. It can confirm 75% of these witnesses—indicating that ghost witnesses can bridge the semantic divide between interleaving and thread-modular approaches.
AB - Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling independent validation of the reasoning by other tools. For the correctness of concurrent programs, no agreed-upon witness format exists—in no small part due to the divide between the semantics considered by analyzers, ranging from interleaving to thread-modular approaches, making it challenging to exchange information. We propose a format that leverages the well-known notion of ghosts to embed the claims a tool makes about a program into a modified program with ghosts, such that the validity of a witness can be decided by analyzing this program. Thus, the validity of witnesses with respect to the interleaving and the thread-modular semantics coincides. Further, thread-modular invariants computed by an abstract interpreter can naturally be expressed in the new format using ghost statements. We evaluate the approach by generating such ghost witnesses for a subset of concurrent programs from the SV-COMP benchmark suite, and pass them to a model checker. It can confirm 75% of these witnesses—indicating that ghost witnesses can bridge the semantic divide between interleaving and thread-modular approaches.
KW - Abstract Interpretation
KW - Concurrency
KW - Correctness Witnesses
KW - Ghost Variables
KW - Model Checking
KW - Software Verification
UR - http://www.scopus.com/inward/record.url?scp=85218451674&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-82700-6_4
DO - 10.1007/978-3-031-82700-6_4
M3 - Conference contribution
AN - SCOPUS:85218451674
SN - 9783031826993
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 74
EP - 100
BT - Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Proceedings
A2 - Shankaranarayanan, Krishna
A2 - Sankaranarayanan, Sriram
A2 - Trivedi, Ashutosh
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 20 January 2025 through 21 January 2025
ER -