Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)

Dominik Klumpp; Frank Sch\"ussele; Helmut Seidl; Julian Erhard; Manuel Bentele; Matthias Heizmann; Michael Schwarz; Sarah Tilscher; Simmo Saan; Vesal Vojdani

REVIEW 2 major objections 4 minor 113 references

Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)

T0 review · 2 major / 4 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper establishes that correctness witnesses for concurrent programs can be defined so that their validity is the same under both interleaving semantics and thread-modular semantics, by attaching ghost-variable updates and invariants…

desk verdict Genuinely useful witness format and a 29-bug payoff, but the headline equivalence theorem rests on a direction the paper leaves unproved. read the letter →

arxiv 2411.16612 v1 pith:4G2N7JRN submitted 2024-11-25 cs.PL

Julian Erhard , Manuel Bentele , Matthias Heizmann , Dominik Klumpp , Simmo Saan , Frank Schüssele , Michael Schwarz , Helmut Seidl

show 2 more authors

Sarah Tilscher Vesal Vojdani

This is my paper · ORCID

classification cs.PL

keywords concurrentprogramscorrectnesswitnessesghostvariablesthread-modularsemanticsinterleavingabstractinterpretationmodelcheckingsoftwareverification

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper proposes a format for correctness witnesses of concurrent programs—evidence that a program satisfies an assertion—that works equally well for analyzers that reason by interleaving all thread actions and analyzers that reason thread-by-thread with a local trace semantics. The key idea is to let a witness add ghost variables: auxiliary variables that do not affect program behavior, updated atomically with real statements, plus location invariants over both real and ghost variables. Instrumenting the program with these ghosts turns witness validity into ordinary safety of the instrumented program, and the paper argues that safety under the two semantics coincides for such programs. If the central result holds, a correctness proof produced by a thread-modular analyzer can be checked by an interleaving model checker, and vice versa, without the validator needing to know which semantics produced the witness. In the evaluation, an independent model checker confirmed 75% of the witnesses generated this way, and the exchange exposed 29 pre-existing bugs in the two tools.

What carries the argument

The load-bearing object is the ghost witness $(D,X,U,I)$: ghost global declarations $D$, ghost local variables $X$, a partial function $U$ attaching ghost updates to program edges, and location invariants $I$. It operates through the witness-instrumented program $P^W$, in which each original action is executed atomically together with its ghost update and invariant checks are inserted as atomic assertions. To move between semantics, the split transformation rewrites every atomic block as a critical section guarded by the per-global mutexes of the variables it accesses. The chain of equivalences—Theorem 4 ($P$ safe iff $\mathrm{split}\,P$ safe) and Theorem 1 (safe under interleaving iff safe under local traces for guarded programs)—is what lifts the two semantics to agreement on witness validity in Theorem 5.

What would settle it

Take a ghost-instrumented program whose atomic-block semantics is safe, encode its atomic blocks as critical sections with per-global mutexes, and search the encoded program for an assertion violation; a single such case would directly contradict the unproved direction of Theorem C.2 and, through it, Theorem 5.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is Theorem 5: a witness $W$ for a program $P$ is valid with respect to the interleaving semantics if and only if it is valid with respect to the local trace semantics. Validity is not defined by a bespoke witness checker; it is defined by building the witness-instrumented program $P^W$, which adds ghost declarations and updates plus location invariants, and asking whether $P^W$ is safe. Ghost updates are folded with original statements into atomic blocks, and the split transformation encodes those atomic blocks as critical sections protected by per-global mutexes. The equivalence chains two earlier results: the mutex encoding preserves safety of atomic-block programs (Theorem 4), and for programs in the guarded language, interleaving and local-trace semantics agree on safety (Theorem 1). The paper further shows how thread-modular invariants—mutex invariants and protected invariants—are naturally expressed in the format by ghost booleans that track whether each mutex is locked and whether the program has become multithreaded.

Load-bearing premise

The unproved direction of Theorem C.2 is the load-bearing assumption: an assertion violation in the critical-section-encoded program must always correspond to a violation in the original atomic-block program.

Editorial extensions

If this is right

Witness validity becomes a property of the witness-instrumented program rather than of any particular analyzer, so an independent validator can confirm a concurrent correctness proof without adopting the generator's semantics.
Thread-modular invariants that track lock ownership, including relational mutex invariants, can be packed into the witness format, lowering the adoption barrier for existing verifiers.
Validity under both semantics means that a witness rejected by one kind of validator is rejected by the other, so disagreements between tools can be traced to a bad witness or a buggy validator rather than to a semantic mismatch.
The safety-preservation results guarantee both trust directions: a valid witness forces the original program to be safe, and an unsafe original program can never have a valid correctness witness.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

An implicit consequence is that the same ghost mechanism could be reused for violation witnesses: ghost history variables could record enough of an interleaving for a consumer to reconstruct why an assertion fails, giving concurrent violation witnesses a comparable exchange format.
The missing proof for Theorem C.2 is the place to look first: a counterexample would not necessarily destroy the practical format, but it would force validators to treat atomicity as a first-class semantic notion instead of relying on the mutex encoding.
Because the format attaches invariant evaluation to C sequence points, it sidesteps data-race granularity; extending ghost witnesses to weak-memory models would require redefining when an invariant is allowed to observe a partially written shared value.
The approach also suggests a division of labor in tool chains: a lightweight thread-modular analyzer can emit ghost witnesses that a more expensive interleaving model checker then confirms, effectively using witnesses to focus the model checker on the reasoning it needs to re-verify.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

You should know two things about this paper. First, the engineering is real: a YAML-based ghost-witness format for concurrent programs, implemented in Goblint and Ultimate GemCutter, with an artifact and 29 pre-existing bugs found across the two tools. That is a solid, useful contribution. Second, the central theoretical claim—Theorem 5, that witness validity coincides between interleaving and local-trace semantics—is not actually established. The proof reduces to Theorem 4, whose direction “split P safe implies P safe” is Theorem C.2, and the proof of that theorem in Appendix C.1 is literally the words “Without proof.” This is load-bearing, not cosmetic. If that direction fails, an interleaving-valid witness could produce an unsafe split program, and a thread-modular validator would reject a witness that is valid under interleaving semantics. The paper is candid about the omission, but the coincidence theorem is the headline and it is currently a conjecture, not a theorem.

What the paper does well: the format itself is a natural extension of the sequential witness format, the ghost-variable encoding is explained clearly, and the evaluation is honest about threats to validity. Finding 29 bugs, including soundness-critical ones, is a meaningful empirical result and a good argument for adoption even without the full theory. The abstract's 75% confirmation rate does not match Table 1 exactly—the overall confirmed rate is closer to 70%, with 83% on correct programs and 61% on incorrect ones—but that is a minor precision issue in the abstract, not a fatal flaw.

The soft spot is the unproved theorem. The rest of the formal development, including the ghost-instrumentation preservation lemmas, is sketched or proved in the appendix and looks plausible. The missing direction is the only part I would call a genuine gap, and the authors clearly know it exists.

Who is this for? Tool developers in concurrency verification, especially those working on SV-COMP witnesses. They will get practical value from the format and the bug list. The theoretical claim should not be cited as a proven theorem until the proof appears.

My recommendation: send it to peer review, but with the explicit expectation that the authors either provide a full proof of Theorem C.2 or re-scope Theorem 5 as a conjecture with empirical support. The engineering and the bug findings deserve publication; the theorem needs to be fixed or downgraded.

Referee Report

2 major / 4 minor

Summary. The paper proposes a witness format for correctness witnesses of concurrent programs, using ghost variables and ghost updates to encode a tool's reasoning into an instrumented program. The central theoretical claim is Theorem 5, which states that the validity of a ghost witness with respect to the interleaving semantics coincides with its validity with respect to the local trace (thread-modular) semantics. The paper also defines a YAML-based concrete format, shows how thread-modular invariants from Goblint can be expressed as ghost witnesses, and reports an evaluation in which witnesses generated by Goblint are validated by the model checker Ultimate GemCutter.

Significance. If established, the equivalence in Theorem 5 would be a valuable contribution: it would allow the exchange of correctness witnesses between verifiers based on different concurrency semantics, with validation soundly performed by either kind of tool. The paper's concrete YAML format, the artifact, and the detailed bug reports from both Goblint and Ultimate GemCutter are significant practical contributions, and the paper is transparent about limitations and threats to validity. However, the central theoretical claim is not actually proved in the submitted manuscript, and the empirical summary contains a numerical inconsistency, so the contribution is currently not fully supported.

major comments (2)

[Section 4, Appendix C.1] Theorem 5 depends on both directions of Theorem 4. The direction P safe implies split P safe — equivalently, the contrapositive that any violation of split P yields a violation of P — is stated as Theorem C.2 in Appendix C.1 with the proof literally marked 'Without proof.' Corollary 3, which asserts the same implication, is also given without a derivation, and the paragraph following Corollary 3 states the converse of the corollary. Since Theorem 5 is the paper's central 'coincides' claim, this is a load-bearing gap: the manuscript does not establish that an interleaving-valid witness is also valid under the local trace semantics, even assuming all other results. A complete proof of Theorem C.2 (or a fully worked proof of the missing direction of Theorem 4) is required before the main claim can be accepted.
[Abstract, Table 1] The abstract states that the model checker can confirm 75% of the generated witnesses, but this percentage is not derivable from Table 1. The table yields 653/787 ≈ 83% confirmed for witnesses of correct programs, 710/1165 ≈ 61% for witnesses of incorrect programs, and 1363/1952 ≈ 70% overall. Please reconcile the abstract's number with the reported data, or explicitly state the denominator and the subset of witnesses used for the 75% figure.

minor comments (4)

[Section 2.3] The formal definition of local trace semantics is deferred to Schwarz et al. [71]; for a self-contained extended version, it would be helpful to include the key definitions and consistency requirements directly, since Theorem 1 and Theorem 5 both rely on this semantics.
[Section 4] The claim that the critical-section encoding may introduce deadlocks that 'do not unduly restrict the set of reachable states' is made without argument. Since this is exactly the point that the unproved Theorem C.2 must justify, the statement should either be proved or explicitly identified as part of the missing proof.
[Section 7.2] In Table 1, the 'rejected' rows are all zero, while the text separately reports 12 crashes due to ghost updates at unsupported locations and 58 cases of unsupported C features. It would be clearer to account for these cases explicitly in the table or in a footnote, so that the reader can see how they relate to the 'out of resources' counts.
[Section 6] The C-level witness semantics is justified via sequence points and the assumption of data-race freedom, but the connection between these C-specific notions and the abstract Lang/Split semantics is only informal. A precise statement of the intended correspondence would strengthen the paper's claim that the abstract equivalence transfers to the implemented format.

Circularity Check

0 steps flagged · score 0.0 of 10

No load-bearing circularity: the witness-validity equivalence is a derivation from stated semantics, not a restatement of its inputs.

full rationale

The paper's central claim, Theorem 5, is an equivalence between two independently defined validity notions: interleaving validity (Definition 5: W is valid iff P^W is safe under interleaving semantics) and local-trace validity (Definition 7: W is valid iff split P^W is safe under local-trace semantics). The proof connects these by Theorem 4 (the atomic-block-to-critical-section encoding split preserves safety) and Theorem 1 (for LangMG programs, interleaving safety and local-trace safety agree), with Theorem 1 argued from Lemma 1 in Appendix A.2 rather than merely cited. The experimental section then checks externally generated Goblint witnesses with a different tool, GemCutter; no parameter is fitted and no 'prediction' is defined in terms of the confirmation data, so the 75% confirmation rate is not circular evidence. The only flagged issue is a proof gap rather than circularity: Appendix C.1's Theorem C.2, which supplies the 'split P unsafe implies P unsafe' direction needed for one side of Theorem 4, is stated with the proof text 'Without proof', and Corollary 3 is likewise unproved. This makes Theorem 5's derivation incomplete as a proof obligation, but it does not reduce the theorem to its own inputs or to a self-citation chain. Self-citations to Goblint and to prior local-trace semantics by overlapping authors provide definitions and implementation context, while the equivalence argument itself is presented in the paper; hence no load-bearing circularity is exhibited.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The paper introduces no new physical or logical entities; ghost variables are a pre-existing concept. The load-bearing assumptions are the unproved atomic-block encoding direction (Theorem C.2), the prior local-trace semantics, and the data-race-free sequential-consistency scoping of the C fragment.

assumptions (5)

ad hoc to paper Theorem C.2: Safety of the critical-section encoding split P implies safety of the atomic-block program P in the direction used to show interleaving-validity implies local-trace-validity. Stated without proof.
The paper states 'Proof. Without proof.' in Appendix C.1. This theorem is needed for Theorem 5, the central equivalence claim.
ad hoc to paper Atomic blocks in LangAtomic can be encoded as critical sections by inserting lock/unlock operations on per-global mutexes MG following a total order, without changing the set of reachable assertion violations.
Introduced in Section 4 of the paper; the construction (split) is defined and Theorem 4 asserts safety equivalence, but one direction is unproved (Theorem C.2).
domain assumption The local trace semantics of Schwarz et al. [71,72] is taken as the canonical thread-modular semantics, including the causality order, lock order, and reads-from rules.
Section 2.3 summarizes the semantics from prior work; the paper relies on this as the thread-modular view.
domain assumption C programs under analysis are free of data races and assumed to execute under sequential consistency; weak memory models and non-atomic shared accesses are excluded.
Section 6 states 'we only consider well-behaved C programs without such data races' and 'always assume sequential consistency.'
domain assumption Ghost updates are side-effect-free with respect to non-ghost variables and are executed atomically with the original statement or at designated sequence points.
Section 3 and Section 6 define ghost updates and atomicity; the preservation theorems rely on this non-interference.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)." pith.science (2026). https://pith.science/paper/4G2N7JRN

@misc{pith2026241116612,
  author       = {Pith},
  title        = {Pith review of: Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4G2N7JRN}},
  note         = {Machine review of arXiv:2411.16612}
}

read the original abstract

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.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

113 extracted references · 46 canonical work pages

[1]

In: Baader, F., Voronkov, A

Albert, E., Puebla, G., Hermenegildo, M.V.: Abstractio n-carrying code. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, A rtiﬁ- cial Intelligence, and Reasoning, 11th International Conf erence, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings , Lecture Notes in Computer Science, vol. 3452, pp. 380–397, Springer (2004), https://doi...

work page doi:10.1007/978-3-540-32275-7_25 2004
[2]

Texts in Computer Science, Springer (200 9), ISBN 978- 1-84882-744-8, https://doi.org/10.1007/978-1-84882-745-5

Apt, K.R., de Boer, F.S., Olderog, E.: Veriﬁcation of Seq uential and Con- current Programs. Texts in Computer Science, Springer (200 9), ISBN 978- 1-84882-744-8, https://doi.org/10.1007/978-1-84882-745-5

doi:10.1007/978-1-84882-745-5
[3]

In: Model Checking Sof tware, Lec- ture Notes in Computer Science, vol

Ayaziová, P., Beyer, D., Lingsch-Rosenfeld, M., Spiess l, M., Strejček, J.: Software veriﬁcation witnesses 2.0. In: Model Checking Sof tware, Lec- ture Notes in Computer Science, vol. 14624, pp. 184–203, Spr inger (2024), https://doi.org/10.1007/978-3-031-66149-5_11

doi:10.1007/978-3-031-66149-5_11 2024
[4]

In: Chakraborty, S., Navas, J.A

Becker, B.F.H., Marché, C.: Ghost code in action: Automa ted veriﬁcation of a symbolic interpreter. In: Chakraborty, S., Navas, J.A. (eds.) Veriﬁed Software. Theories, Tools, and Experiments - 11th Internat ional Confer- ence, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Re vised Selected Papers, Lecture Notes in Computer Science, vol. 12 031, pp...

work page doi:10.1007/978-3-030-41600-3_8 2019
[5]

In: Tools and Algorithms for the Construction and Analysis of Systems, pp

Beyer, D.: Competition on software veriﬁcation and witn ess validation: SV-COMP 2023. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 495–522, Springer Nature Switzerl and (2023), https://doi.org/10.1007/978-3-031-30820-8_29

doi:10.1007/978-3-031-30820-8_29 2023
[6]

In: Finkbeiner, B., Kovács, L

Beyer, D.: State of the art in software veriﬁcation and wi tness validation: SV-COMP 2024. In: Finkbeiner, B., Kovács, L. (eds.) Tools an d Algorithms for the Construction and Analysis of Systems - 30th Internat ional Confer- ence, TACAS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Pro- ceedings, Part III, Lecture Notes in Computer Science, vol. 1...

doi:10.1007/978-3-031-57256-2_15 2024
[7]

https://sv-comp.sosy-lab.org/2024/rules.php (2024), accessed: 2024- 09-29

Beyer, D.: SV-COMP 2024 - 13th competition on software ve riﬁcation. https://sv-comp.sosy-lab.org/2024/rules.php (2024), accessed: 2024- 09-29

2024
[8]

In: Zimm ermann, T., Cleland-Huang, J., Su, Z

Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correct ness witnesses: exchanging veriﬁcation results between veriﬁers. In: Zimm ermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engine ering, FSE 2016, Seattle, W A, USA, November 13-18, 2016, pp. 326–337, A CM (2016), htt...

arXiv 2016

Show all 113 references

[9]

In: Nitto, E.D., Harman, M., Heymans, P

Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlba uer, A.: Wit- ness validation and stepwise testiﬁcation across software veriﬁers. In: Nitto, E.D., Harman, M., Heymans, P. (eds.) Proceedings of the 2015 10th Joint Correctness Witnesses for Concurrent Programs 23 Meetin...

2015
[10]

In: Margaria, T., Steﬀen, B

Beyer, D., Friedberger, K.: Violation witnesses and re sult validation for multi-threaded programs - implementation and evaluati on with CPAchecker. In: Margaria, T., Steﬀen, B. (eds.) Leveraging Applications of Formal Methods, Veriﬁcation and Validation: Veriﬁcatio n Principl...

2020
[11]

In: Fisman, D., Rosu, G

Beyer, D., Kanav, S.: CoVeriTeam: On-Demand Compositi on of Cooper- ative Veriﬁcation Systems. In: Fisman, D., Rosu, G. (eds.) T ools and Al- gorithms for the Construction and Analysis of Systems, pp. 5 61–579, Lec- ture Notes in Computer Science, Springer International Pub li...

2022 doi
[12]

International Journal on Software Tools for Tec hnology Transfer 21(1), 1–29 (nov 2017), https://doi.org/10.1007/s10009-017-0469-y

Beyer, D., Löwe, S., Wendler, P.: Reliable benchmarkin g: requirements and solutions. International Journal on Software Tools for Tec hnology Transfer 21(1), 1–29 (nov 2017), https://doi.org/10.1007/s10009-017-0469-y

2017 doi
[13]

In: Sergey , I

Bila, E.V., Dongol, B., Lahav, O., Raad, A., Wickerson, J.: View-based Owicki-Gries reasoning for persistent x86-TSO. In: Sergey , I. (ed.) Program- ming Languages and Systems - 31st European Symposium on Prog ram- ming, ESOP 2022, Munich, Germany, April 2-7, 2022, Proceedi ng...

2022 doi
[14]

Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1-3), 227–270 (2007), https://doi.org/10.1016/J.TCS.2006.12.034

2007 doi
[15]

In: Jacobs, B., Silva, A., Staton, S

Brookes, S.: On grainless footprint semantics for shar ed-memory pro- grams. In: Jacobs, B., Silva, A., Staton, S. (eds.) Proceedi ngs of the 30th Conference on the Mathematical Foundations of Programming Seman- tics, MFPS 2014, Ithaca, NY, USA, June 12-15, 2014, Electron ic N...

2014 doi
[16]

In: Kaufmann, M., Paulson, L.C

Cachera, D., Pichardie, D.: A certiﬁed denotational ab stract interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11 -14, 2010. Pro- ceedings, Lecture Notes in Computer Science, vol. 617...

2010 doi
[17]

In: Fernández, M

Casso, I., Morales, J.F., López-García, P., Hermenegi ldo, M.V.: Testing your (static analysis) truths. In: Fernández, M. (ed.) Logi c-Based Pro- gram Synthesis and Transformation - 30th International Sym posium, LOP- STR 2020, Bologna, Italy, September 7-9, 2020, Proceedings ...

2020 doi
[18]

In: Aho, A.V., Zilles, S.N., Rosen, B.K

Clarke, E.M.: Synthesis of resource invariants for con current programs. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference R ecord of the Sixth Annual ACM Symposium on Principles of Programming Lan guages, San Antonio, Texas, USA, January 1979, pp. 211–221, ACM Pres s...

1979
[19]

In: Chandra, S., Blincoe, K., Tonella, P

Correnson, A., Steinhöfel, D.: Engineering a formally veriﬁed automated bug ﬁnder. In: Chandra, S., Blincoe, K., Tonella, P. (eds.) P roceedings of the 31st ACM Joint European Software Engineering Conferenc e and Sym- posium on the Foundations of Software Engineering, ESEC/FS ...

2023
[20]

In: Hirschfeld, R., Pape, T

Dalvandi, S., Doherty, S., Dongol, B., Wehrheim, H.: Ow icki-Gries rea- soning for C11 RAR. In: Hirschfeld, R., Pape, T. (eds.) 34th E uropean Conference on Object-Oriented Programming, ECOOP 2020, No vember 15-17, 2020, Berlin, Germany (Virtual Conference), LIPIcs , vol. 166,...

2020 doi
[21]

Dalvandi, S., Dongol, B., Doherty, S., Wehrheim, H.: In tegrating Owicki- Gries for C11-style memory models into Isabelle/HOL. J. Aut om. Reason. 66(1), 141–171 (2022), https://doi.org/10.1007/S10817-021-09610-2

2022 doi
[22]

In: Bauer, F.L., Broy, M

Dijkstra, E.W.: Finding the correctness proof of a conc urrent program. In: Bauer, F.L., Broy, M. (eds.) Program Construction, Interna tional Sum- mer School, July 26 - August 6, 1978, Marktoberdorf, Germany , Lec- ture Notes in Computer Science, vol. 69, pp. 24–34, Springer (...

1978 doi
[23]

Correctness Witnesses for Co ncur- rent Programs: Bridging the Semantic Divide with Ghosts

Erhard, J., Bentele, M., Heizmann, M., Klumpp, D., Saan , S., Schüs- sele, F., Schwarz, M., Seidl, H., Tilscher, S., Vojdani, V.: Arti- fact for the VMCAI’2025 paper “Correctness Witnesses for Co ncur- rent Programs: Bridging the Semantic Divide with Ghosts” (O ct 2024), https...

2025 doi
[24]

https://ultimate-pa.github.io/concurrency-witnesses /correctness-witness-schema.yml (2024), accessed: 2024-09-29

Erhard, J., Bentele, M., Heizmann, M., Klumpp, D., Saan, S., Schüssele, F., Schwarz, M., Seidl, H., Tilscher, S., Vojdani, V.: Correctness witness schema. https://ultimate-pa.github.io/concurrency-witnesses /correctness-witness-schema.yml (2024), accessed: 2024-09-29

2024
[25]

ultimate-pa.github.io/concurrency-witnesses/index.h tml (2024), accessed: 2024-09-29

Erhard, J., Bentele, M., Heizmann, M., Klumpp, D., Saan , S., Schüssele, F., Schwarz, M., Seidl, H., Tilscher, S., Vo- jdani, V.: Format for correctness witnesses, version 2.1. ultimate-pa.github.io/concurrency-witnesses/index.h tml (2024), accessed: 2024-09-29

2024
[26]

Evans, C., Ben-Kiki, O., döt Net, I., Müller, T., Antoni ou, P., Aro, E., Smith, T.: YAML Ain’t Markup Language (YAML™) Version 1. 2. https://yaml.org/spec/1.2.2/ (2021)

2021
[27]

In: Jagan- nathan, S., Sewell, P

Farzan, A., Kincaid, Z., Podelski, A.: Proofs that coun t. In: Jagan- nathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SI GACT Symposium on Principles of Programming Languages, POPL ’14 , San Correctness Witnesses for Concurrent Programs 25 Diego, CA, USA, January 20-...

2014
[28]

In: Jhala, R., Dillig, I

Farzan, A., Klumpp, D., Podelski, A.: Sound sequential ization for concur- rent program veriﬁcation. In: Jhala, R., Dillig, I. (eds.) P LDI ’22: 43rd ACM SIGPLAN International Conference on Programming Langu age De- sign and Implementation, San Diego, CA, USA, June 13 - 17, 20...

2022
[29]

Farzan, A., Klumpp, D., Podelski, A.: Commutativity si mpliﬁes proofs of parameterized programs. Proc. ACM Program. Lang. 8(POPL), 2485–2513 (2024), https://doi.org/10.1145/3632925

2024 doi
[30]

Formal Methods Syst

Filliâtre, J., Gondelman, L., Paskevich, A.: The spiri t of ghost code. Formal Methods Syst. Des. 48(3), 152–174 (2016), https://doi.org/10.1007/S10703-016-0243-X

2016 doi
[32]

In: Dragoi, C., Mukher jee, S., Namjoshi, K.S

Franceschino, L., Pichardie, D., Talpin, J.: Veriﬁed f unctional pro- gramming of an abstract interpreter. In: Dragoi, C., Mukher jee, S., Namjoshi, K.S. (eds.) Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceeding s, Lectu...

2021 doi
[33]

Gries, D.: An exercise in proving parallel programs cor rect. Commun. ACM 20(12), 921–930 (1977), https://doi.org/10.1145/359897.359903

1977
[34]

In: Gar- avel, H., Hatcliﬀ, J

Gurﬁnkel, A., Chechik, M.: Proof-like counter-exampl es. In: Gar- avel, H., Hatcliﬀ, J. (eds.) Tools and Algorithms for the Con - struction and Analysis of Systems, 9th International Confe rence, TACAS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, Lecture Notes in Compu...

2003 doi
[35]

In: Schli ngloﬀ, B.H., Chai, M

Haltermann, J., Wehrheim, H.: Information Exchange Be tween Over- and Underapproximating Software Analyses. In: Schli ngloﬀ, B.H., Chai, M. (eds.) Software Engineering and Formal Meth- ods, pp. 37–54, Lecture Notes in Computer Science, Springer In- ternational Publishing, Cham...

2022 doi
[36]

In: Palsberg, J., Su, Z

Heizmann, M., Hoenicke, J., Podelski, A.: Reﬁnement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) Static Analysis, 16th Intern ational Sympo- sium, SAS 2009, Los Angeles, CA, USA, August 9-11, 2009. Proc eedings, Lecture Notes in Computer Science, vol. 5673, pp. 69–85,...

2009 doi
[37]

In: Castagna, G

Hoenicke, J., Majumdar, R., Podelski, A.: Thread modul arity at many lev- els: a pearl in compositional veriﬁcation. In: Castagna, G. , Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Prin ciples of 26 J. Erhard et al. Programming Languages, POPL 2017, Par...

2017
[38]

International Organization for Standardization and I nternational Electrotechnical Commission: ISO/IEC 9899:1999 — Program ming Languages — C. Tech. rep., ISO/IEC JTC 1/SC 22 (1999), URL http://www.open-std.org/jtc1/sc22/wg14/www/docs/n11 24.pdf, ISO/IEC 9899:1999 (C99) draft

1999
[39]

In: Rajamani, S.K., Walker, D

Jourdan, J., Laporte, V., Blazy, S., Leroy, X., Pichard ie, D.: A formally- veriﬁed C static analyzer. In: Rajamani, S.K., Walker, D. (e ds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principl es of Programming Languages, POPL 2015, Mumbai, India, January ...

2015
[40]

In: Proceedings of the 39th International Conf erence on Automated Software Engineering (ASE’24), ACM (2024), UR L https://doi.org/10.1145/3691620.3695034

Kaindlstorfer, D., Isychev, A., Wüstholz, V., Christa kis, M.: In- terrogation testing of program analyzers for soundness and preci- sion issues. In: Proceedings of the 39th International Conf erence on Automated Software Engineering (ASE’24), ACM (2024), UR L https://doi.org/...

2024
[41]

Keller, R.M.: Formal veriﬁcation of parallel programs . Commun. ACM 19(7), 371–384 (1976), https://doi.org/10.1145/360248.360251

1976
[42]

In: Zhang, D., Møller, A

Klinger, C., Christakis, M., Wüstholz, V.: Diﬀerentia lly testing soundness and precision of program analyzers. In: Zhang, D., Møller, A . (eds.) Pro- ceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, Beijing, China, July 15...

2019
[43]

In: Fisman, D., Rosu, G

Klumpp, D., Dietsch, D., Heizmann, M., Schüssele, F., E bbinghaus, M., Farzan, A., Podelski, A.: Ultimate GemCutter and the axes of generaliza- tion (competition contribution). In: Fisman, D., Rosu, G. ( eds.) Tools and Algorithms for the Construction and Analysis of Systems -...

2022 doi
[44]

I n: Yang, H

Krebbers, R., Jung, R., Bizjak, A., Jourdan, J., Dreyer , D., Birkedal, L.: The essence of higher-order concurrent separation logic. I n: Yang, H. (ed.) Programming Languages and Systems - 26th European Symposiu m on Programming, ESOP 2017, Uppsala, Sweden, April 22-29, 2017 ,...

2017 doi
[45]

In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann , B

Lahav, O., Vafeiadis, V.: Owicki-Gries reasoning for w eak memory models. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann , B. (eds.) Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Par t ...

2015 doi
[46]

IEEE Trans

Lamport, L.: Proving the correctness of multiprocess p ro- grams. IEEE Trans. Software Eng. 3(2), 125–143 (1977), https://doi.org/10.1109/TSE.1977.229904 Correctness Witnesses for Concurrent Programs 27

1977
[47]

Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978), https://doi.org/10.1145/359545.359563

1978
[48]

IEEE Trans

Lamport, L.: How to make a multiprocessor computer that correctly ex- ecutes multiprocess programs. IEEE Trans. Computers 28(9), 690–691 (1979), https://doi.org/10.1109/TC.1979.1675439

1979
[49]

In: Giacobazzi, R., Cousot, R

Ley-Wild, R., Nanevski, A.: Subjective auxiliary stat e for coarse-grained concurrency. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan guages, POPL ’13, Rome, Italy - January 23 - 25, 2013, pp. 561–574, ACM (...

2013
[50]

In: Wortman, D.B

Lomet, D.B.: Process structuring, synchronization, a nd recovery using atomic actions. In: Wortman, D.B. (ed.) Proceedings of an AC M Con- ference on Language Design for Reliable Software (LDRS), Ra leigh, North Carolina, USA, March 28-30, 1977, pp. 128–137, ACM (19 77), https...

1977
[51]

Acta Informatica 21, 125–169 (1984), https://doi.org/10.1007/BF00289237

Lubachevsky, B.D.: An approach to automating the veriﬁ cation of com- pact parallel coordination programs I. Acta Informatica 21, 125–169 (1984), https://doi.org/10.1007/BF00289237

1984 doi
[52]

In: Brauer, W., Reis ig, W., Rozen- berg, G

Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reis ig, W., Rozen- berg, G. (eds.) Petri Nets: Central Models and Their Proper- ties, Advances in Petri Nets 1986, Part II, Proceedings of an Ad- vanced Course, Bad Honnef, Germany, 8-19 September 1986, Le cture Notes in Compu...

1986 doi
[53]

In: Morrisett , J.G., Jones, S.L.P

McCloskey, B., Zhou, F., Gay, D., Brewer, E.A.: Autoloc ker: syn- chronization inference for atomic sections. In: Morrisett , J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Sy mpo- sium on Principles of Programming Languages, POPL 2006, Cha rleston, Sout...

2006
[54]

In: de Frutos-Escrig, D., Núñez, M

Meolic, R., Fantechi, A., Gnesi, S.: Witness and counte rexample automata for ACTL. In: de Frutos-Escrig, D., Núñez, M. (eds.) Formal T echniques for Networked and Distributed Systems - FORTE 2004, 24th IFI P WG 6.1 International Conference, Madrid Spain, September 27-30, 2004...

2004 doi
[55]

In: Dimitrova, R

Milanese, M., Miné, A.: Generation of violation witnes ses by under- approximating abstract interpretation. In: Dimitrova, R. , Lahav, O., Wolﬀ, S. (eds.) Veriﬁcation, Model Checking, and Abstract I nter- pretation - 25th International Conference, VMCAI 2024, Lon don, United K...

2024 doi
[56]

Miné, A.: Static analysis of run-time errors in embedde d real- time parallel C programs. Log. Methods Comput. Sci. 8(1) (2012), https://doi.org/10.2168/LMCS-8(1:26)2012

2012 doi
[57]

In: McMillan, K.L., Rival, X

Miné, A.: Relational thread-modular static value anal ysis by abstract inter- pretation. In: McMillan, K.L., Rival, X. (eds.) Veriﬁcatio n, Model Check- ing, and Abstract Interpretation - 15th International Conf erence, VM- CAI 2014, San Diego, CA, USA, January 19-21, 2014, Pr...

2014 doi
[58]

In: Bouajjani, A., Monniaux, D

Monat, R., Miné, A.: Precise thread-modular abstract i nterpreta- tion of concurrent programs using relational interference abstractions. In: Bouajjani, A., Monniaux, D. (eds.) Veriﬁcation, Model C heck- ing, and Abstract Interpretation - 18th International Conf erence, VM- CA...

2017 doi
[59]

In: Ranzato, F

Mukherjee, S., Padon, O., Shoham, S., D’Souza, D., Rine tzky, N.: Thread- local semantics and its eﬃcient sequential abstractions fo r race-free pro- grams. In: Ranzato, F. (ed.) Static Analysis - 24th Internat ional Sympo- sium, SAS 2017, New York, NY, USA, August 30 - Septem...

2017 doi
[60]

In: Shao, Z

Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A .: Communicating state transition systems for ﬁne-grained concurrent resou rces. In: Shao, Z. (ed.) Programming Languages and Systems - 23rd European Sym posium on Programming, ESOP 2014, Grenoble, France, April 5-13, 2014...

2014 doi
[61]

In: Proceedings of the 15th Interna tional Par- allel & Distributed Processing Symposium (IPDPS-01), San F rancisco, CA, USA, April 23-27, 2001, p

Nieto, L.P.: Completeness of the Owicki-Gries system f or parameter- ized parallel programs. In: Proceedings of the 15th Interna tional Par- allel & Distributed Processing Symposium (IPDPS-01), San F rancisco, CA, USA, April 23-27, 2001, p. 150, IEEE Computer Society (20 01), ...

2001
[62]

Nieto, L.P.: Veriﬁcation of parallel programs with the Owicki- Gries and Rely-Guarantee methods in Isabelle, HOL. Ph.D. thesis, Technical University Munich, Germany (2002), URL https://mediatum.ub.tum.de/?id=601717

2002
[63]

In: Finance, J

Nipkow, T., Nieto, L.P.: Owicki/Gries in Isabelle/HOL . In: Finance, J. (ed.) Fundamental Approaches to Software Engineering, Sec ond Interna- tionsl Conference, F ASE’99, Amsterdam, The Netherlands, M arch 22-28, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1577...

1999 doi
[64]

OASIS SARIF Technical Committee: Static analysis resu lts interchange format (SARIF) version 2.1.0. OASIS standard, Organizatio n for the Advancement of Structured Information Standards (OASIS) ( 2020), URL https://docs.oasis-open.org/sarif/sarif/v2.1.0/os/s arif-v2.1.0-os.pdf...

2020
[65]

Owicki, S.S., Gries, D.: Verifying properties of paral lel programs: An axiomatic approach. Commun. ACM 19(5), 279–285 (1976), https://doi.org/10.1145/360051.360224

1976
[66]

Raad, A., Lahav, O., Vafeiadis, V.: Persistent Owicki- Gries reason- ing: a program logic for reasoning about persistent program s on Intel- x86. Proc. ACM Program. Lang. 4(OOPSLA), 151:1–151:28 (2020), https://doi.org/10.1145/3428219

2020 doi
[67]

In: Tools and Algorithms for the Construction an d Anal- ysis of Systems, pp

Saan, S., Schwarz, M., Erhard, J., Pietsch, M., Seidl, H ., Tilscher, S., Vojdani, V.: Goblint: Autotuning thread-modular abstr act inter- pretation. In: Tools and Algorithms for the Construction an d Anal- ysis of Systems, pp. 547–552, Springer Nature Switzerland ( 2023), htt...

2023 doi
[68]

In: Dimitrova, R., Lahav, O., Wolﬀ, S

Saan, S., Schwarz, M., Erhard, J., Seidl, H., Tilscher, S., Vojdani, V.: Correctness witness validation by abstract interpretatio n. In: Dimitrova, R., Lahav, O., Wolﬀ, S. (eds.) Veriﬁcation, Model Checking, and Ab- stract Interpretation - 25th International Conference, VM CAI...

2024 doi
[69]

Schmaltz, S.B.: Towards the pervasive formal veriﬁcat ion of multi-core oper- ating systems and hypervisors implemented in C. Ph.D. thesi s, Universität des Saarlandes (2012), https://doi.org/10.22028/D291-26525

2012 doi
[70]

In: Bidoit, M., Dauchet, M

Schreiber, T.: Auxiliary variables and recursive proc edures. In: Bidoit, M., Dauchet, M. (eds.) TAPSOFT’97: Theory and Practice of Software Develop- ment, 7th International Joint Conference CAAP/F ASE, Lille, France, April 14-18, 1997, Proceedings, Lecture Notes in Computer S...

1997 doi
[71]

, Vojdani, V.: Im- proving thread-modular abstract interpretation

Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J. , Vojdani, V.: Im- proving thread-modular abstract interpretation. In: Drag oi, C., Mukher- jee, S., Namjoshi, K.S. (eds.) Static Analysis - 28th Intern ational Sympo- sium, SAS 2021, Chicago, IL, USA, October 17-19, 202...

2021 doi
[72]

In: Wies, T

Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V .: Clustered rela- tional thread-modular abstract interpretation with local traces. In: Wies, T. (ed.) Programming Languages and Systems - 32nd European S ymposium on Programming, ESOP 2023, Paris, France, April 22-27, 2...

2023 doi
[73]

In: Hong, J., Lanperne, M., Park, J.W., Cerný, T., Shahriar, H

Semenyuk, M., Dongol, B.: Ownership-based Owicki-Gri es reasoning. In: Hong, J., Lanperne, M., Park, J.W., Cerný, T., Shahriar, H. ( eds.) Proceed- ings of the 38th ACM/SIGAPP Symposium on Applied Computing, SAC 2023, Tallinn, Estonia, March 27-31, 2023, pp. 1685–1694, A CM (2...

2023
[74]

In: Grove, D., Blackburn, S.M

Sergey, I., Nanevski, A., Banerjee, A.: Mechanized ver iﬁcation of ﬁne- grained concurrent programs. In: Grove, D., Blackburn, S.M . (eds.) Pro- 30 J. Erhard et al. ceedings of the 36th ACM SIGPLAN Conference on Programming L an- guage Design and Implementation, Portland, OR, ...

2015
[75]

In: Gurﬁnkel, A., Ganesh , V

Stade, Y., Tilscher, S., Seidl, H.: The top-down solver veriﬁed: Build- ing conﬁdence in static analyzers. In: Gurﬁnkel, A., Ganesh , V. (eds.) Computer Aided Veriﬁcation - 36th International Conferenc e, CA V 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I ,...

2024 doi
[76]

In: Biere, A., Parker, D

Svejda, J., Berger, P., Katoen, J.: Interpretation-ba sed violation witness validation for C: NITWIT. In: Biere, A., Parker, D. (eds.) To ols and Algo- rithms for the Construction and Analysis of Systems - 26th In ternational Conference, TACAS 2020, Dublin, Ireland, April 25-3...

2020 doi
[77]

https://ultimate-pa.org/ (2024), accessed: 2024-09-29

Ultimate developers: Ultimate program analysis frame work. https://ultimate-pa.org/ (2024), accessed: 2024-09-29

2024
[78]

In: Dragoi, C., Emmi, M., Wang, J

Vick, C., McMillan, K.L.: Synthesizing history and pro phecy variables for symbolic model checking. In: Dragoi, C., Emmi, M., Wang, J. ( eds.) Veriﬁca- tion, Model Checking, and Abstract Interpretation - 24th In ternational Con- ference, VMCAI 2023, Boston, MA, USA, January 16...

2023 doi
[79]

de Vilhena, P.E., Pottier, F., Jourdan, J.: Spy game: ve rifying a local generic solver in Iris. Proc. ACM Program. Lang. 4(POPL), 33:1–33:28 (2020), https://doi.org/10.1145/3371101

2020 doi
[80]

In : Proceedings of the 31st IEEE/ACM International Conference on Automated So ftware En- gineering, ACM (aug 2016), https://doi.org/10.1145/2970276.2970337

Vojdani, V., Apinis, K., Rõtov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the Goblint approach. In : Proceedings of the 31st IEEE/ACM International Conference on Automated So ftware En- gineering, ACM (aug 2016), https://doi.org/10.1145/297...

2016
[81]

Form al Aspects Comput

Wright, D., Dalvandi, S., Batty, M., Dongol, B.: Mechan ised operational reasoning for C11 programs with relaxed dependencies. Form al Aspects Comput. 35(2), 10:1–10:27 (2023), https://doi.org/10.1145/3580285

2023 doi
[82]

In: Agrawal, M., Cooper, S.B., Li, A

Zhang, Z., Feng, X., Fu, M., Shao, Z., Li, Y.: A structura l approach to prophecy variables. In: Agrawal, M., Cooper, S.B., Li, A. (eds.) The- ory and Applications of Models of Computation - 9th Annual Co nfer- ence, TAMC 2012, Beijing, China, May 16-21, 2012. Proceedin gs, Le...

2012 doi
[83]

For any interleaving i ∈ I , there exists a create-complete global trace gt ∈ GT such that i and gt coincide
[84]

For any create-complete global trace gt ∈ GT , there exists an interleaving i ∈ I such that i and gt coincide. Proof. 1. Fix an interleaving i ∈ I and a thread t ∈ threadsI(i). We obtain the global trace gt as follows: (a) For every thread ti ∈ threadsI (i), including t, we ex...
[85]

Then, we pick a total order on states that extends this partial order, yielding ordered states s0 < s 1 < · · ·< s n, for some n

We extend the partial order of the create-complete global trace gt, by adding an ordering between any end node u of a create step and the initial node of the created thread v, with u < v . Then, we pick a total order on states that extends this partial order, yielding ordered ...
[86]

Unsound invariants from interval set domain widening (is sue #1356, issue #1473, PR #1476)
[87]

Unsound relational analysis due to extern variables (issue #1440, PR #1444)
[88]

Unsound relational analysis due to __VERIFIER_atomic mutex (issue #1440, PR #1441)
[89]

– SV-COMP witness generation:

continue handling in syntactic loop unrolling (PR #1369). – SV-COMP witness generation:
[90]

Logical expression intermediate locations (issue #1356 , CIL PR #166)
[91]

Multiple/composite declaration initializer intermedi ate locations (CIL PR #167, PR #1372)
[92]

for loop initializer location_invariant location ( CIL PR #167)
[93]

for loop loop_invariant location (issue #1355, PR #1372)
[94]

No loop_invariant for goto loop (PR #1372)
[95]

do-while loop loop_invariant location (PR #1372)
[96]

Exclude internal struct names from generated invariants (PR #1375)
[97]

Improve invariants for syntactically unrolled loops (PR #1403)
[98]

Exclude trivial _Bool invariants (issue #1356, PR #1436)
[99]

Exclude trivial congruence invariants (issue #1218)
[100]

Exclude invariants with out-of-scope local variables ( issue #1361, PR #1362)
[101]

Mutex-meet invariants do not account for initial values (issue #1356)
[102]

Not ﬁxed:

Exclude Goblint stubs from witnesses (PR #1334). Not ﬁxed:
[103]

Witness invariant parser does not handle typedef (CIL issue #159)
[104]

Autotuner enables all integer domains (issue #1472)
[105]

Ultimate

Cannot have location_invariant before loop (issue #1391). Ultimate. Fixed:
[106]

Erhard et al

(Validation) Location invariants at labels were not hand led properly (d55e39c) 38 J. Erhard et al
[107]

(C-Translation) Model return value of __VERIFIER_nondet_bool properly (f7d84c9)
[108]

(ACSL) Enhance grammar for variable names (b9e0ﬀ7, ab2e0 ac)
[109]

(ACSL) Support _Bool type (9435525, cb09d65)
[110]

(ACSL) Support for &(ed2a5ba)
[111]

(ACSL) Fix -> translation (6f5224f)
[112]

(CFG) Fix support for nested atomic blocks (a38a16e) Not ﬁxed:
[113]

(C-Translation) Missing support for pthread-attributes
[114]

(ACSL) Missing support for function pointers

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [1]

In: Baader, F., Voronkov, A

Albert, E., Puebla, G., Hermenegildo, M.V.: Abstractio n-carrying code. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, A rtiﬁ- cial Intelligence, and Reasoning, 11th International Conf erence, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings , Lecture Notes in Computer Science, vol. 3452, pp. 380–397, Springer (2004), https://doi...

work page doi:10.1007/978-3-540-32275-7_25 2004

[2] [2]

Texts in Computer Science, Springer (200 9), ISBN 978- 1-84882-744-8, https://doi.org/10.1007/978-1-84882-745-5

Apt, K.R., de Boer, F.S., Olderog, E.: Veriﬁcation of Seq uential and Con- current Programs. Texts in Computer Science, Springer (200 9), ISBN 978- 1-84882-744-8, https://doi.org/10.1007/978-1-84882-745-5

doi:10.1007/978-1-84882-745-5

[3] [3]

In: Model Checking Sof tware, Lec- ture Notes in Computer Science, vol

Ayaziová, P., Beyer, D., Lingsch-Rosenfeld, M., Spiess l, M., Strejček, J.: Software veriﬁcation witnesses 2.0. In: Model Checking Sof tware, Lec- ture Notes in Computer Science, vol. 14624, pp. 184–203, Spr inger (2024), https://doi.org/10.1007/978-3-031-66149-5_11

doi:10.1007/978-3-031-66149-5_11 2024

[4] [4]

In: Chakraborty, S., Navas, J.A

Becker, B.F.H., Marché, C.: Ghost code in action: Automa ted veriﬁcation of a symbolic interpreter. In: Chakraborty, S., Navas, J.A. (eds.) Veriﬁed Software. Theories, Tools, and Experiments - 11th Internat ional Confer- ence, VSTTE 2019, New York City, NY, USA, July 13-14, 2019, Re vised Selected Papers, Lecture Notes in Computer Science, vol. 12 031, pp...

work page doi:10.1007/978-3-030-41600-3_8 2019

[5] [5]

In: Tools and Algorithms for the Construction and Analysis of Systems, pp

Beyer, D.: Competition on software veriﬁcation and witn ess validation: SV-COMP 2023. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 495–522, Springer Nature Switzerl and (2023), https://doi.org/10.1007/978-3-031-30820-8_29

doi:10.1007/978-3-031-30820-8_29 2023

[6] [6]

In: Finkbeiner, B., Kovács, L

Beyer, D.: State of the art in software veriﬁcation and wi tness validation: SV-COMP 2024. In: Finkbeiner, B., Kovács, L. (eds.) Tools an d Algorithms for the Construction and Analysis of Systems - 30th Internat ional Confer- ence, TACAS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Pro- ceedings, Part III, Lecture Notes in Computer Science, vol. 1...

doi:10.1007/978-3-031-57256-2_15 2024

[7] [7]

https://sv-comp.sosy-lab.org/2024/rules.php (2024), accessed: 2024- 09-29

Beyer, D.: SV-COMP 2024 - 13th competition on software ve riﬁcation. https://sv-comp.sosy-lab.org/2024/rules.php (2024), accessed: 2024- 09-29

2024

[8] [8]

In: Zimm ermann, T., Cleland-Huang, J., Su, Z

Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correct ness witnesses: exchanging veriﬁcation results between veriﬁers. In: Zimm ermann, T., Cleland-Huang, J., Su, Z. (eds.) Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engine ering, FSE 2016, Seattle, W A, USA, November 13-18, 2016, pp. 326–337, A CM (2016), htt...

arXiv 2016