Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs

Guy Blelloch; Siddhartha Jayanti; Stephanie Balzer; Ugur Y. Yavuz; Zachary Kent

REVIEW 4 major objections 5 minor 15 references

Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs

T0 review · 4 major / 5 minor · reviewed 2026-08-04 · deepseek-v4-flash

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

Pith's one-line read Mechanized proof in Rocq certifies forward-reasoning linearizability end to end.

desk verdict A genuinely useful mechanization of Jayanti et al.'s meta-configuration tracking metatheory, but the submitted text misstates the central adequacy theorem (missing a well-formedness hypothesis) and ships no Rocq artifact, so it needs correction and artifact release before I'd trust the end-to-end claim. read the letter →

arxiv 2509.06872 v1 pith:7ZZPGUHH submitted 2025-09-08 cs.PL

Zachary Kent , Ugur Y. Yavuz , Siddhartha Jayanti , Stephanie Balzer , Guy Blelloch This is my paper · ORCID

classification cs.PL

keywords linearizabilitymeta-configurationtrackingforwardreasoningmechanicalverificationRocqconcurrentdatastructuresfuture-dependentlinearizationregister

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

Linearizability is the gold standard for concurrent data structure correctness, but machine-checked proofs of it are hard to obtain end to end. This paper formalizes meta-configuration tracking, the first sound and complete forward-reasoning technique for proving linearizability, and mechanizes its metatheory in the Rocq proof assistant. The central result, Theorem 1 (Adequacy), states that an implementation is linearizable if and only if the tracker of the final configuration of every augmented run it admits is inhabited. Both directions of this biconditional are machine-checked, and a concurrent register with a future-dependent linearization structure receives a fully verified end-to-end linearizability proof. If the paper is right, future linearizability proofs using this technique no longer need to trust an unmechanized soundness and completeness argument.

What carries the argument

The central mechanism is meta-configuration tracking, with a 'tracker' as ghost state attached to each concrete configuration. The tracker holds the set of all atomic configurations that could be the final state of some linearization of the run so far. The evolve function updates this set on each executed line: invocations mark a process pending, responses discard atomic configurations whose linearized value does not match the returned value, and intermediate lines leave the set unchanged; a linearize_pending relation then closes the set under arbitrary sequences of pending operations taking effect. The multistep transition relation δ* is the load-bearing bridge that lets the proof maintain

What would settle it

Inspect the Rocq proof term of Theorem adequacy: if its only assumptions are the paper's definitions, functional extensionality, and standard finite-map facts, the claimed mechanization is real; any hidden axiom or unverified use of Lynch's Theorems 13.4/13.5 would expose a trust gap. Separately, a concrete counterexample—an implementation whose tracker is inhabited in every admitted augmented run yet whose behavior differs from every atomic run—would directly refute soundness.

Watch

Extended reading notes

Core claim

The paper's central claim is an adequacy biconditional: an implementation is linearizable exactly when, in every run augmented with ghost 'tracker' state, the final tracker contains at least one atomic configuration consistent with the run. Soundness says an inhabited tracker forces the existence of a linearization; completeness says every linearizable implementation keeps its tracker inhabited. The authors formalize runs, atomic runs, behavior equality, and the tracker's evolution function in Rocq, and they prove the biconditional as the theorem 'linearizable impl ↔ ∀r, ∃σ f, (final r).(tracker) σ f'. As an end-to-end demonstration, they build a machine-checked linearizability proof for a r

Load-bearing premise

The formalized notion of linearizability is the atomic-run definition taken from Lynch, and the paper relies on a cited, not machine-checked, equivalence to Herlihy-Wing's history-based definition; if that equivalence is unfaithful, the end-to-end verified guarantee attaches to a different correctness condition.

Editorial extensions

If this is right

New linearizability proofs using meta-configuration tracking can now be checked end to end in a proof assistant, with soundness and completeness already mechanized.
The proof burden for a concrete data structure reduces to showing that the tracker in every admitted augmented run remains inhabited, rather than constructing an explicit linearization from scratch.
Future-dependent algorithms, whose linearization points cannot be decided online, remain provable in a forward reasoning style because the tracker keeps all possible linearizations alive.
The register case study supplies a verified implementation of a double-width write using only read and CAS on a single-width cell, connecting the metatheory to a practical hardware gap.

Reading between the lines

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

A natural next step is to mechanize the cited equivalence between the formalized atomic-run definition and Herlihy-Wing histories, which would close the remaining trust gap in the end-to-end guarantee.
The same tracker framework should generalize to other refinement-based correctness conditions, such as sequential consistency or set-linearizability, by changing the atomic dynamics and the evolve rules.
Because the tracker is a set rather than a single simulation, automated invariant discovery could target the tracker directly, offering a machine-checkable route to verifying more complex concurrent structures.
A stress test would be to replay the earlier TLAPS-verified examples, such as the Herlihy-Wing queue or union-find, inside this Rocq framework without trusting an unmechanized metatheory.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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

The paper's real contribution is the first Rocq mechanization of the meta-theory behind Jayanti et al.'s meta-configuration tracking: soundness and completeness of the adequacy theorem, plus a register case study that is genuinely end-to-end and future-dependent. That is useful and, if the artifact checks out, worth a serious referee. But as submitted, the central theorem is misstated and there is no artifact, so I can't endorse the current version.

What's good: the formalization is coherent, the definitions (runs, well-formedness, behavior, linearizability, trackers) are laid out carefully, and the soundness/completeness proof outline follows a sensible induction. The register example is a good stress test because its linearization really is future-dependent, so it demonstrates the technique rather than just retreading a trivially linearizable example. Credit where due: this is the first mechanization of this particular metatheory and would shrink the TCB for this line of verification.

The soft spots are real. First, the Rocq statement of Theorem 1 in Section 4 is `linearizable impl <-> forall r, exists sigma f, (final r).(tracker) sigma f`. The `run` inductive type allows arbitrary ill-formed runs, e.g. `Initial c` with an empty tracker. Such a run makes the right side false regardless of the implementation, so as written the theorem is refutable. The proof of Lemma 2 explicitly uses `WF_aug r`; without that hypothesis the induction doesn't go through. The stress-test note about this is not a nitpick. I assume this is a typo in the write-up and not in the actual Rocq development, but it is load-bearing and must be fixed with an explicit `WF_aug r` (or by defining `final`/`tracker` only for well-formed runs).

Second, no artifact, build script, or commit hash is shipped. For a paper whose entire claim is "fully mechanized," the absence of the development is a blocker for verification. Third, the completeness proof is omitted from the text. Fine if the artifact covers it, but it makes the paper hard to referee. Fourth, the equivalence between the formalized behavior-based linearizability and Herlihy-Wing is cited via Lynch Theorems 13.4/13.5, not mechanized. I think that's acceptable—it is a standard result—but the paper should state clearly that the end-to-end guarantee is relative to a provably equivalent formulation, not the exact H-W definition.

Bottom line: the underlying work is sound in intent, the method is worthwhile, and a corrected version with artifact deserves a serious referee. Don't desk-reject; send it out, but require the artifact and the fixed theorem statement before accepting.

Referee Report

4 major / 5 minor

Summary. The paper claims to mechanize in Rocq the metatheory of meta-configuration tracking, a forward-reasoning technique for proving linearizability introduced by Jayanti et al. It formalizes a small concurrent language, an implementation semantics, a Lynch-style behavior-based definition of linearizability, augmented runs with tracker state, and states an Adequacy theorem (Theorem 1) connecting linearizability to the inhabitedness of trackers. It also reports a case study: an end-to-end proof of linearizability for a read/write register implemented with read and CAS. The paper contains informal proof sketches, Rocq snippets, and claims that all proofs are mechanized in about 3250 lines of Rocq, but it provides no artifact, repository link, or commit hash.

Significance. If fully machine-checked, this would be a valuable contribution: it would be the first mechanized proof of soundness and completeness for the meta-configuration tracking technique, and the first end-to-end linearizability proof built on that metatheory. The formalization is careful in many places—the run semantics, the distinction between implementation runs and atomic runs, and the inductive definition of well-formedness are all concrete, and the paper explicitly names the key adequacy theorem and its two directions. The register case study is well chosen because it illustrates future-dependent linearizability. However, the absence of a machine-checked artifact and the incomplete informal proofs prevent the reader from verifying the central claim as presented.

major comments (4)

[§4, Theorem 1] The displayed Rocq statement `Theorem adequacy : linearizable impl ↔ ∀r, ∃σ f, (final r).(tracker) σ f` is false as written. Because the type `run` (§3.1) admits `Initial c` for arbitrary configurations `c`, choose `r = Initial c` where `c`'s tracker is empty; then `(final r).(tracker) σ f` is false for all σ and f, making the right-hand side false even for a linearizable implementation. The informal proof of Lemma 2 also says "Because we assume that r is well-formed," but the lemma statement says "arbitrary augmented run r." The theorem must be quantified over well-formed augmented runs, e.g. `∀r, WF_aug r → ...`, and the formal statement must match the proof. This is a load-bearing issue for the central adequacy claim.
[§6, Mechanization] The paper's central claim is that all proofs are "fully mechanized in Rocq," but no development is provided: there is no repository URL, commit hash, buildable artifact, or even a listing of the main proof files. Section 6 states that the mechanization amounts to about 3250 lines of Rocq, but gives the reader no way to inspect, reproduce, or check that claim. In a mechanized-metatheory paper, the artifact is essential evidence. Please provide a public artifact and a clear mapping from the paper's theorem and lemma names to the corresponding Rocq definitions and proofs.
[§4, Lemma 3] The completeness direction of Adequacy is load-bearing: Theorem 1's reverse direction depends on Lemma 3, which asserts that every linearization's final atomic configuration appears in the tracker. However, the paper says only "For brevity, we omit an informal proof of completeness here." No artifact is available to supply the missing details. As a result, the completeness half of the central theorem is unsupported in the manuscript. Please include an informal proof or a detailed proof sketch, and ensure the artifact contains the complete machine-checked proof of Lemma 3.
[§3.4, Linearizability] The formal predicate `linearizable` is defined as: every well-formed implementation run has behavior syntactically equal to the behavior of some well-formed atomic run. This is not the original Herlihy-Wing definition; the paper cites Lynch's Theorems 13.4 and 13.5 for the equivalence, but that equivalence is not mechanized. Since the abstract emphasizes "verified end-to-end proofs of linearizability" and "reducing the trusted computing base," this unmechanized equivalence remains in the trusted base. Please either mechanize the equivalence, or explicitly state that the end-to-end result is for the behavior-based (Lynch) notion of linearizability.

minor comments (5)

[§5, object definitions] In defining the base object type, the text says "Define OP RWCELL to be {Read, CAS}", but this should be `OP_RCASCELL`, the operation set for the compare-and-swap cell.
[Figure 5] The Step-Invoke rule has a stray trailing comma in its conclusion: `⟨σ,[Pendingop arg/π]f,⟩`. It should be `⟨σ,[Pendingop arg/π]f⟩`.
[§6 and §7] Minor typos: "extenstionally" should be "extensionally" in §6, and "asychronous" should be "asynchronous" in §7.
[Template and front matter] The paper uses CVIT 2016 template placeholders (conference name, DOI `10.4230/LIPIcs.CVIT.2016.23`, page numbering). These should be updated to the actual venue and DOI before publication.
[§4, Lemma 2 proof] The informal soundness proof omits the Intermediate and Response cases after saying they are similar and "included in the mechanization." Without the artifact, these cases are not inspectable; even an informal treatment of the Response case would help the reader.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the adequacy theorem is proved from the formal semantics rather than imported from prior work.

full rationale

Walking the derivation chain, the central claim is Theorem 1, which is a machine-checked biconditional between `linearizable impl` (defined in §3.4 from run behaviors and atomic runs, independent of the tracker) and the inhabitability of the tracker's final metaconfiguration. The tracker's evolution (`evolve`/`linearize_pending`) is an auxiliary definition, not an assumed conclusion; Lemmas 2 and 3 establish the connection by induction over runs. No parameter is fitted to the target claim, and the case-study register proof uses the metatheorem only after it is proved. The only imported external result is Lynch's equivalence of the formalized run-behavior definition to Herlihy-Wing linearizability [25, Theorems 13.4/13.5], which is cited as an assumption rather than mechanized; that is a trust-base/faithfulness issue, not circularity. The authors' prior work [16] is cited as the origin of meta-configuration tracking and for the historical claim that it is the first complete forward-reasoning method, but the paper's adequacy theorem is not derived from that paper's soundness/completeness results; it is re-proved from the formal semantics provided here. For completeness, note that the displayed Rocq statement of Theorem 1 omits the `WF_aug` hypothesis that the proof (e.g., Lemma 2) relies on; this is a correctness risk in the paper text, not a circularity construct. No circular step can be exhibited from the paper's own equations or definitions.

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

No free parameters are fit to data. The axioms are standard (functional extensionality), a library dependency, and the unmechanized Lynch equivalence theorem. No new empirical entities are introduced; the meta-configuration tracker is a proof device from prior work, not a postulated entity.

assumptions (3)

standard math Functional extensionality is assumed to equate extensionally equal functions over maps.
Section 6: 'we axiomatize functional extensionality so that extensionally equal functions representing maps are indeed equal.' This is a common, consistency-safe axiom in CIC-based provers and is used for finite map reasoning.
domain assumption The stdpp finite map library is sound and is used as a dependency.
Section 6: 'We also depend on the stdpp package, from which we employ its finite maps.' The library is treated as trusted infrastructure.
domain assumption Lynch's equivalence theorem: behavior-based linearizability is equivalent to Herlihy-Wing linearizability.
Section 3.4: 'Lynch proves that this definition of linearizability is equivalent to Herlihy and Wing's original definition [25] (Theorems 13.4 and 13.5).' This is cited, not mechanized, so the connection to the standard definition is an external assumption.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs." pith.science (2026). https://pith.science/paper/7ZZPGUHH

@misc{pith2026250906872,
  author       = {Pith},
  title        = {Pith review of: Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7ZZPGUHH}},
  note         = {Machine review of arXiv:2509.06872}
}

read the original abstract

In the past decade, many techniques have been developed to prove linearizability, the gold standard of correctness for concurrent data structures. Intuitively, linearizability requires that every operation on a concurrent data structure appears to take place instantaneously, even when interleaved with other operations. Most recently, Jayanti et al. presented the first sound and complete "forward reasoning" technique for proving linearizability that relates the behavior of a concurrent data structure to a reference atomic data structure as time moves forward. This technique can be used to produce machine-checked proofs of linearizability in TLA+. However, while Jayanti et al.'s approach is shown to be sound and complete, a mechanization of this important metatheoretic result is still outstanding. As a result, it is not possible to produce verified end-to-end proofs of linearizability. To reduce the size of this trusted computing base, we formalize this forward reasoning technique and mechanize proofs of its soundness and completeness in Rocq. As a case study, we use the approach to produce a verified end-to-end proof of linearizability for a simple concurrent register.

Figures

Figures reproduced from arXiv: 2509.06872 by the authors.

**Figure 5.** As expected, there are three rules corresponding to the invocation, linearization, [PITH_FULL_IMAGE:figures/full_fig_p011_5.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

15 extracted references · 11 canonical work pages

[11]

Leveson and C.S

24 N.G. Leveson and C.S. Turner. An investigation of the Therac-25 accidents.Computer, 26(7):18–41, 1993.doi:10.1109/MC.1993.274940. 25 Nancy A. Lynch.Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA,

work page arXiv 1993
[1990]

16 Prasad Jayanti, Siddhartha Jayanti, Ugur Yavuz, and Lizzie Hernandez

doi: 10.1145/78969.78972. 16 Prasad Jayanti, Siddhartha Jayanti, Ugur Yavuz, and Lizzie Hernandez. A universal, sound, and complete forward reasoning technique for machine-verified proofs of linearizability.Proc. ACM Program. Lang., 8(POPL), January 2024.doi:10.1145/3632924. 17 Siddhartha V. Jayanti and Robert E. Tarjan. A randomized concurrent algorithm ...

arXiv 2024
[1996]

Visibility reasoning for concurrent snapshot algorithms.Proc

26 Joakim Öhman and Aleksandar Nanevski. Visibility reasoning for concurrent snapshot algorithms.Proc. ACM Program. Lang., 6(POPL), January 2022.doi:10.1145/3498694. 27 Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen. A compositional theory of linearizability. Proc. ACM Program. Lang., 7(POPL), January 2023.doi:10.1145/3571231. 28Kevin Poulsen. Software...

doi:10.1145/3498694 2022
[1997]

On decomposing and refining specifications of distributed systems

19 Bengt Jonsson. On decomposing and refining specifications of distributed systems. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors,Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Nether- lands, May 29 - June 2, 1989, Proceedings, volume 430 ofLecture Notes in Computer Science,...

work page 1989
[1998]

A sound and complete proof technique for linearizability of concurrent data structures.ACM Trans

30 Gerhard Schellhorn, John Derrick, and Heike Wehrheim. A sound and complete proof technique for linearizability of concurrent data structures.ACM Trans. Comput. Logic, 15(4), September 2014.doi:10.1145/2629496. Z. Kent, U.Y. Yavuz, S. Jayanti, S. Balzer, and G. Blelloch 23:19 31 Viktor Vafeiadis. Modular fine-grained concurrency verification. Technical ...

work page doi:10.1145/2629496 2014
[2008]

cam.ac.uk/techreports/UCAM-CL-TR-726.pdf,doi:10.48456/tr-726

URL:https://www.cl. cam.ac.uk/techreports/UCAM-CL-TR-726.pdf,doi:10.48456/tr-726. 32 Viktor Vafeiadis. Shape-value abstraction for verifying linearizability. In Neil D. Jones and Markus Müller-Olm, editors,Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20,

work page doi:10.48456/tr-726 2009
[2009]

Springer, 2009.doi:10.1007/978-3-540-93900-9\_27

Proceedings, volume 5403 ofLecture Notes in Computer Science, pages 335–348. Springer, 2009.doi:10.1007/978-3-540-93900-9\_27. CVIT 2016

work page doi:10.1007/978-3-540-93900-9 2009
[2011]

13 Google Graph Mining team

Association for Computing Machinery.doi:10.1145/1993636.1993687. 13 Google Graph Mining team. The Graph Mining Library. GitHub repository.Url:https: //github.com/google/graph-mining,

work page arXiv

Show all 15 references

[2012]

9 Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner

Springer Berlin Heidelberg. 9 Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. TaDA: A logic for time and data abstraction. In Richard Jones, editor,ECOOP 2014 – Object-Oriented Programming, pages 207–231, Berlin, Heidelberg,

2014
[2015]

11 Brijesh Dongol and John Derrick

Association for Computing Machinery.doi:10.1145/2676726.2676963. 11 Brijesh Dongol and John Derrick. Verifying linearisability: A comparative survey.ACM Comput. Surv., 48(2), September 2015.doi:10.1145/2796550. 12 Wojciech Golab, Lisa Higham, and Philipp Woelfel. Linearizable ...

2015
[2016]

doi:10.1145/2933057.2933108

Association for Computing Machinery. doi:10.1145/2933057.2933108. 18 Mike Jones. What really happened on Mars Rover Pathfinder.The Risks Digest, 19(49):1–2,
[2017]

3 Daphna Amit, Noam Rinetzky, Thomas W

doi:10.1007/s10009-016-0415-4. 3 Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. Comparison under abstraction for verifying linearizability. In Werner Damm and Holger Hermanns, editors, Computer Aided Verification, 19th International Conference, CAV 20...

2007 doi
[2018]

doi:10.1017/S0956796818000151

Accepted Author Manuscript. doi:10.1017/S0956796818000151. 22 Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. The future is ours: prophecy variables in separation logic. Proc. ACM Program. Lang., 4(POPL), Decemb...

2019 doi
[2023]

Henzinger, Ali Sezgin, and Viktor Vafeiadis

CVIT 2016 23:18 Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs 14 Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Aspect-oriented linearizability proofs. In Pedro R. D’Argenio and Hernán Melgratti, editors,CONCUR 2013 – Concurrency Theo...

2016
[2024]

TLA+ proofs

8 Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA+ proofs. In Dimitra Giannakopoulou and Dominique Méry, editors,FM 2012: Formal Methods, pages 147–154, Berlin, Heidelberg,

2012

Pith tools

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

[1] [11]

Leveson and C.S

24 N.G. Leveson and C.S. Turner. An investigation of the Therac-25 accidents.Computer, 26(7):18–41, 1993.doi:10.1109/MC.1993.274940. 25 Nancy A. Lynch.Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA,

work page arXiv 1993

[2] [1990]

16 Prasad Jayanti, Siddhartha Jayanti, Ugur Yavuz, and Lizzie Hernandez

doi: 10.1145/78969.78972. 16 Prasad Jayanti, Siddhartha Jayanti, Ugur Yavuz, and Lizzie Hernandez. A universal, sound, and complete forward reasoning technique for machine-verified proofs of linearizability.Proc. ACM Program. Lang., 8(POPL), January 2024.doi:10.1145/3632924. 17 Siddhartha V. Jayanti and Robert E. Tarjan. A randomized concurrent algorithm ...

arXiv 2024

[3] [1996]

Visibility reasoning for concurrent snapshot algorithms.Proc

26 Joakim Öhman and Aleksandar Nanevski. Visibility reasoning for concurrent snapshot algorithms.Proc. ACM Program. Lang., 6(POPL), January 2022.doi:10.1145/3498694. 27 Arthur Oliveira Vale, Zhong Shao, and Yixuan Chen. A compositional theory of linearizability. Proc. ACM Program. Lang., 7(POPL), January 2023.doi:10.1145/3571231. 28Kevin Poulsen. Software...

doi:10.1145/3498694 2022

[4] [1997]

On decomposing and refining specifications of distributed systems

19 Bengt Jonsson. On decomposing and refining specifications of distributed systems. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors,Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, The Nether- lands, May 29 - June 2, 1989, Proceedings, volume 430 ofLecture Notes in Computer Science,...

work page 1989

[5] [1998]

A sound and complete proof technique for linearizability of concurrent data structures.ACM Trans

30 Gerhard Schellhorn, John Derrick, and Heike Wehrheim. A sound and complete proof technique for linearizability of concurrent data structures.ACM Trans. Comput. Logic, 15(4), September 2014.doi:10.1145/2629496. Z. Kent, U.Y. Yavuz, S. Jayanti, S. Balzer, and G. Blelloch 23:19 31 Viktor Vafeiadis. Modular fine-grained concurrency verification. Technical ...

work page doi:10.1145/2629496 2014

[6] [2008]

cam.ac.uk/techreports/UCAM-CL-TR-726.pdf,doi:10.48456/tr-726

URL:https://www.cl. cam.ac.uk/techreports/UCAM-CL-TR-726.pdf,doi:10.48456/tr-726. 32 Viktor Vafeiadis. Shape-value abstraction for verifying linearizability. In Neil D. Jones and Markus Müller-Olm, editors,Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20,

work page doi:10.48456/tr-726 2009

[7] [2009]

Springer, 2009.doi:10.1007/978-3-540-93900-9\_27

Proceedings, volume 5403 ofLecture Notes in Computer Science, pages 335–348. Springer, 2009.doi:10.1007/978-3-540-93900-9\_27. CVIT 2016

work page doi:10.1007/978-3-540-93900-9 2009

[8] [2011]

13 Google Graph Mining team

Association for Computing Machinery.doi:10.1145/1993636.1993687. 13 Google Graph Mining team. The Graph Mining Library. GitHub repository.Url:https: //github.com/google/graph-mining,

work page arXiv