arxiv: 2605.10625 · v1 · submitted 2026-05-11 · 💻 cs.PL

Recognition: no theorem link

Verifying Sequential Consistency under Bounded Preemptions

R. Govind , S. Krishna , Sanchari Sil , B. Srivathsan

Authors on Pith no claims yet

Pith reviewed 2026-05-12 05:22 UTC · model grok-4.3

classification 💻 cs.PL

keywords sequential consistencybounded preemptionsNP-hardnessExponential Time Hypothesisprogram verificationinterleavingsconcurrent programscomplexity trichotomy

0 comments

The pith

Verification of sequential consistency with bounded preemptions is polynomial-time for single-writer programs and NP-hard for two-writer programs.

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

The paper examines whether a given trace of reads and writes from a multi-threaded program admits a sequentially consistent interleaving that uses at most a fixed number of preemptions. This restricted version of the classic consistency-checking problem appears in software testing and inside dynamic partial-order reduction algorithms. The authors prove a trichotomy in complexity: the check runs in polynomial time when each variable has only a single writer thread, becomes NP-hard as soon as two writers are allowed per variable, and carries a conditional exponential lower bound under the Exponential Time Hypothesis once three writers appear. They additionally show that the problem is W[1]-hard when the preemption bound is treated as the sole parameter.

Core claim

The problem of deciding whether an observed sequence of memory operations is sequentially consistent under an interleaving with at most π preemptions is solvable in polynomial time when the program is single-writer, NP-hard for two-writer programs, and, for three-writer programs, has no 2^{o(π)} algorithm unless the Exponential-Time Hypothesis fails. When π is unbounded the problem is W[1]-hard parameterized by π.

What carries the argument

The trichotomy classification of the bounded-preemption sequential-consistency verification problem according to the number of writers per variable.

If this is right

Single-writer programs admit efficient verification even when the number of allowed preemptions is small.
Two writers per variable already suffice to make the verification problem NP-hard.
Three writers trigger a conditional lower bound showing that no algorithm significantly faster than brute force over preemptions exists.
The problem remains hard in the parameterized sense when the preemption limit is the only parameter.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Dynamic partial-order reduction tools can gain efficiency on single-writer code by exploiting the polynomial-time case.
Similar complexity thresholds based on writer multiplicity may appear under other memory models.
Testing procedures could prioritize or isolate single-writer patterns to scale to larger programs.

Load-bearing premise

The complexity results depend on the precise definition of sequential consistency and the exact way preemptions are counted in an interleaving.

What would settle it

A polynomial-time algorithm for the two-writer case, or a 2^{o(π)} algorithm for the three-writer case that does not violate the Exponential Time Hypothesis.

Figures

Figures reproduced from arXiv: 2605.10625 by B. Srivathsan, R. Govind, Sanchari Sil, S. Krishna.

**Figure 1.** Figure 1: The partial interleaving (1 : w(x, 1))(3 : r(x, 1))(1 : w(x, 2)) has only one preemption at (1 : w(x, 1)) while the interleaving (1 : w(x, 1))(3 : r(x, 1))(1 : w(x, 2))(2 : r(x, 2))(2 : w(y, 1))(1 : r(y, 1)) has two preemptions at (1 : w(x, 1)) and (1 : w(x, 2)). Classification of programs In our analysis, we classify programs based on the number of threads that write to a variable. A concurrent program is… view at source ↗

**Figure 2.** Figure 2: Schema for the algorithm for 1-Writer programs 3 Polynomial-time algorithm for 1-Writer programs We begin our analysis with 1-Writer programs, and the main result of this section is to prove the following theorem. Theorem 1. VSCπadmits a polynomial-time solution for 1-Writer programs. For the rest of this section, fix a 1-Writer program Prog with k threads having a total of n events across all threads, and… view at source ↗

**Figure 3.** Figure 3: In the figure, there are two programs Prog1 and Prog2 . For Prog1 , Step 1 guesses the preemption points to be w(y, 1) from S2, w(x, 2) from S3 and the first r(x, 2) from S4. For Prog2 , the guessed preemption points are w(x, 1) from S1 and w(y, 1) from S2. Step 2.1. A Block-Program from the Blocks. Using these points, the program can be divided into blocks as shown in the right of [PITH_FULL_IMAGE:figur… view at source ↗

**Figure 3.** Figure 3: Programs Prog1 and Prog2 on the left, their corresponding block-programs on the right w.r.t. chosen preemption points. Inner blocks are coloured in violet, and outer blocks in green. The blue edges denote edges in the conflict graph of the outer nodes. a block appear contiguously. Therefore, selecting an interleaving with these preemption points amounts to finding a suitable interleaving of the blocks, wh… view at source ↗

**Figure 4.** Figure 4: A permutation of inner blocks (above), and an interleaving obtained by [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗

**Figure 5.** Figure 5: Illustration of the various complexity results [PITH_FULL_IMAGE:figures/full_fig_p010_5.png] view at source ↗

**Figure 6.** Figure 6: Illustrating the preemption points within a selector thread [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗

read the original abstract

Gibbons and Korach studied a fundamental problem in 1997: given an observed sequence of reads and writes of a multi-threaded program, does there exist an interleaving which is sequentially consistent? Apart from applications in testing shared memory implementations, a procedure for this problem is employed in Dynamic Partial-Order-Reduction (DPOR) algorithms. The problem is known to be NP-hard even when different syntactic parameters are kept bounded. In this paper, we consider a restriction on the kind of interleaving required: does there exist a sequentially-consistent interleaving with at most {\pi} preemptions? Empirical evidence suggests that several bugs manifest within a few preemptive switches. This motivates us to investigate the problem under bounded preemptions. Our results exhibit a trichotomy: the problem lends to a polynomial-time algorithm for the class of single-writer programs where for each variable, there is a single thread writing to it; it becomes NP-hard for two-writer programs and finally, for three-writer programs, we get a conditional lower bound under the Exponential-Time-Hypothesis. When the number of preemptions {\pi} is not bounded, we show the problem to be W[1]-hard, and hence unlikely to be fixed-parameter-tractable with parameter {\pi}.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper maps sequential consistency verification under bounded preemptions to a clean trichotomy by writer count per variable, plus W[1]-hardness in the preemption bound.

read the letter

The main takeaway is a trichotomy for deciding whether a trace has a sequentially consistent interleaving using at most π preemptions: polynomial time for single-writer programs, NP-hard once two writers appear per variable, and an ETH-based lower bound at three writers. They also show the problem is W[1]-hard when parameterized by π alone. This refines the 1997 Gibbons-Korach NP-hardness result by adding the preemption restriction and the writer-based split, both of which are new. The motivation from DPOR algorithms and the observation that many bugs appear with few preemptions is straightforward and ties the theory to tool-building practice. The claims rest on standard reductions and the ETH assumption with no circularity or self-referential parameters visible in the abstract. The model of sequential consistency and explicit preemption counting is stated up front and matches the usual setting for this problem. One soft spot is that the abstract states the polynomial algorithm and the hardness constructions without showing their details, so it is not yet possible to check constants, tightness, or whether small changes in preemption counting would move the boundaries. That said, nothing in the stated results contradicts itself or relies on hidden fitting. This work is aimed at people who build or analyze verification tools for concurrent programs, especially those working on DPOR or memory-model testing. A reader who needs to know when exact checks are feasible versus when heuristics are required will get direct value from the classification. It deserves a serious referee because the trichotomy is precise enough to influence tool design choices and the parameterized result adds a new angle. Recommendation: send it to peer review.

Referee Report

0 major / 3 minor

Summary. The paper studies the complexity of checking whether an observed trace of reads and writes from a multi-threaded program admits a sequentially consistent interleaving that uses at most π preemptions. Building on the 1997 Gibbons-Korach result, it establishes a trichotomy: the problem is solvable in polynomial time for single-writer programs (one writer per variable), NP-hard for two-writer programs, and admits an ETH-based conditional lower bound for three-writer programs. It additionally proves W[1]-hardness when parameterized by π (unbounded case).

Significance. If the stated reductions and algorithm hold, the work supplies a fine-grained complexity map for a practically motivated restriction of SC verification, directly relevant to DPOR algorithms and concurrency testing. The single-writer polynomial-time case and the clean separation at two versus three writers are the most useful contributions; the ETH lower bound and parameterized hardness further delineate the boundary between tractable and intractable regimes under the standard SC model with explicit preemption counting.

minor comments (3)

The abstract and introduction use the notation {π} (presumably LaTeX artifacts); replace with standard math mode throughout for readability.
Section 3 (or wherever the single-writer algorithm is presented) should include a brief high-level description of the dynamic-programming or graph-search technique before the formal proof, to help readers verify the claimed polynomial bound.
The ETH lower-bound construction for three-writer programs would benefit from an explicit statement of the source problem (e.g., 3-SAT or multicolored clique) and the precise blow-up in the reduction, even if details are in an appendix.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper, accurate capture of the trichotomy results (polynomial-time for single-writer programs, NP-hardness for two-writer programs, and the ETH-based lower bound for three-writer programs), and the recommendation for minor revision. The report correctly identifies the relevance to DPOR and concurrency testing.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper establishes complexity-theoretic results (P for single-writer programs, NP-hard for two-writer, ETH lower bound for three-writer, and W[1]-hardness parameterized by π) via explicit reductions from known hard problems and a polynomial-time algorithm for the single-writer case. These steps rely on standard SC semantics and preemption counting as declared inputs; no equation, definition, or self-citation reduces a claimed result to a quantity defined in terms of itself or to a fitted parameter. The 1997 Gibbons-Korach reference is external prior work with no author overlap, and the trichotomy follows directly from the reductions without circular renaming or ansatz smuggling.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rely on the standard definition of sequential consistency and the Exponential Time Hypothesis; no free parameters or new entities are introduced.

axioms (1)

domain assumption Exponential Time Hypothesis (ETH)
Invoked to obtain the conditional lower bound for three-writer programs.

pith-pipeline@v0.9.0 · 5530 in / 1335 out tokens · 52519 ms · 2026-05-12T05:22:01.889348+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

87 extracted references · 87 canonical work pages

[1]

Coons and Madan Musuvathi and Kathryn S

Katherine E. Coons and Madan Musuvathi and Kathryn S. McKinley , title =

work page
[2]

Margalit, Roy and Lahav, Ori , year = 2021, journal =

work page 2021
[3]

and Johnson, David S

Garey, Michael R. and Johnson, David S. , title =. 1990 , isbn =

work page 1990
[4]

and Kohli, Prince and Hutto, Phillip W

Ahamad, Mustaque and Neiger, Gil and Burns, James E. and Kohli, Prince and Hutto, Phillip W. , title =. 1995 , issue_date =. doi:10.1007/BF01784241 , journal =

work page doi:10.1007/bf01784241 1995
[6]

Desnoyers, Mathieu and McKenney, Paul E and Stern, Alan S and Dagenais, Michel R and Walpole, Jonathan , year = 2011, journal =

work page 2011
[7]

and Kaminsky, Michael and Andersen, David G

Lloyd, Wyatt and Freedman, Michael J. and Kaminsky, Michael and Andersen, David G. , year = 2011, booktitle =

work page 2011
[8]

POPL'16 , pages =

Ori Lahav and Nick Giannarakis and Viktor Vafeiadis , title =. POPL'16 , pages =. 2016 , publisher =

work page 2016
[9]

Optimal Reads-From Consistency Checking for C11-Style Memory Models , year =

Tun. Optimal Reads-From Consistency Checking for C11-Style Memory Models , year =. doi:10.1145/3591251 , journal =

work page doi:10.1145/3591251
[10]

ICALP'15 , pages =

Ori Lahav and Viktor Vafeiadis , title =. ICALP'15 , pages =. doi:10.1007/978-3-662-47666-6\_25 , year =

work page doi:10.1007/978-3-662-47666-6
[11]

Sebastian Burckhardt , year = 2014, journal =

work page 2014
[12]

Talha Imran, Ivan Puddu, Sanidhya Kashyap, Hasan Al Maruf, Onur Mutlu, and Aasheesh Kolli

Luo, Weiyu and Demsky, Brian , title =. 2021 , publisher =. doi:10.1145/3445814.3446711 , booktitle=

work page doi:10.1145/3445814.3446711 2021
[13]

PLDI 2017 , year =

Lahav, Ori and Vafeiadis, Viktor and Kang, Jeehoon and Hur, Chung-Kil and Dreyer, Derek , title =. PLDI 2017 , year =. doi:10.1145/3062341.3062352 , note =

work page doi:10.1145/3062341.3062352 2017
[14]

POPL'11 , year =

Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark , title =. POPL'11 , year =

work page
[15]

Iason Marmanis and Michalis Kokologiannakis and Viktor Vafeiadis , title =

work page
[16]

Madanlal Musuvathi and Shaz Qadeer , title =

work page
[17]

Subcubic Equivalences between Path, Matrix and Triangle Problems , booktitle =

Virginia. Subcubic Equivalences between Path, Matrix and Triangle Problems , booktitle =

work page
[18]

Subcubic Equivalences Between Path, Matrix, and Triangle Problems , journal =

Virginia. Subcubic Equivalences Between Path, Matrix, and Triangle Problems , journal =

work page
[19]

Stubborn Sets for Reduced State Space Generation , Booktitle =

Antti Valmari. Stubborn Sets for Reduced State Space Generation , Booktitle =. 1991 , Address =

work page 1991
[20]

Springer-Verlag

Doron A. Peled , Title =. Computer Aided Verification , Location =. 1993 , Publisher = "Springer-Verlag", Address = "London, UK", Url =

work page 1993
[21]

Symposium on Principles of Programming Languages , series =

Abdulla, Parosh and Aronis, Stavros and Jonsson, Bengt and Sagonas, Konstantinos , title =. Symposium on Principles of Programming Languages , series =. 2014 , publisher =

work page 2014
[22]

2017 , issn =

Abdulla, Parosh Aziz and Aronis, Stavros and Jonsson, Bengt and Sagonas, Konstantinos , title =. 2017 , issn =. doi:10.1145/3073408 , acmid =

work page doi:10.1145/3073408 2017
[23]

Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem

Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. doi:10.1007/3-540-60761-7 , note = "Also, volume 1032 of

work page doi:10.1007/3-540-60761-7
[24]

Clarke and Orna Grumberg and Marius Minea and Doron A

Edmund M. Clarke and Orna Grumberg and Marius Minea and Doron A. Peled , title =. 1999 , publisher =

work page 1999
[25]

Computer Aided Verification , location =

Parosh Aziz Abdulla and Mohamed Faouzi Atig and Bengt Jonsson and Carl Leonardsson , title =. Computer Aided Verification , location =. 2016 , series =

work page 2016
[26]

Parosh Aziz Abdulla and Mohamed Faouzi Atig and Bengt Jonsson and Tuan Phong Ngo , title =

work page
[27]

Acta Inf

Parosh Aziz Abdulla and Stavros Aronis and Mohamed Faouzi Atig and Bengt Jonsson and Carl Leonardsson and Konstantinos Sagonas , title =. Acta Inf. , volume =

work page
[28]

Parosh Aziz Abdulla and Stavros Aronis and Bengt Jonsson and Konstantinos Sagonas , title =

work page
[29]

Michalis Kokologiannakis and Iason Marmanis and Vladimir Gladstein and Viktor Vafeiadis , title =. Proc. 2022 , url =

work page 2022
[30]

Krishnendu Chatterjee and Andreas Pavlogiannis and Viktor Toman , title =. Proc. 2019 , url =

work page 2019
[31]

Gibbons and Ephraim Korach , title =

Phillip B. Gibbons and Ephraim Korach , title =

work page
[32]

Papadimitriou , title =

Christos H. Papadimitriou , title =

work page
[33]

Umang Mathur and Andreas Pavlogiannis and Mahesh Viswanathan , title =

work page
[34]

Optimal stateless model checking for reads-from equivalence under sequential consistency , journal =

Parosh Aziz Abdulla and Mohamed Faouzi Atig and Bengt Jonsson and Magnus L. Optimal stateless model checking for reads-from equivalence under sequential consistency , journal =

work page
[35]

Pratyush Agarwal and Krishnendu Chatterjee and Shreya Pathak and Andreas Pavlogiannis and Viktor Toman , title =

work page
[36]

Partial-Order Reduction for Context-bounded State Exploration

Madanlal Musuvathi and Shaz Qadeer. Partial-Order Reduction for Context-bounded State Exploration. 2007

work page 2007
[37]

Russell Impagliazzo and Ramamohan Paturi and Francis Zane , title =. J. Comput. Syst. Sci. , volume =

work page
[38]

Simple and tight complexity lower bounds for solving Rabin games , booktitle =

Antonio Casares and Marcin Pilipczuk and Michal Pilipczuk and U. Simple and tight complexity lower bounds for solving Rabin games , booktitle =

work page
[39]

Lower bounds based on the Exponential Time Hypothesis , journal =

Daniel Lokshtanov and D. Lower bounds based on the Exponential Time Hypothesis , journal =

work page
[40]

Marek Chalupa and Krishnendu Chatterjee and Andreas Pavlogiannis and Nishant Sinha and Kapil Vaidya , title =. Proc

work page
[41]

Tovey , title =

Craig A. Tovey , title =. Discret. Appl. Math. , volume =

work page
[42]

A Framework for Consistency Algorithms , booktitle =

Peter Chini and Prakash Saivasan , editor =. A Framework for Consistency Algorithms , booktitle =. 2020 , url =. doi:10.4230/LIPICS.FSTTCS.2020.42 , timestamp =

work page doi:10.4230/lipics.fsttcs.2020.42 2020
[43]

Leslie Lamport , title =. Commun

work page
[44]

Soham Chakraborty and Shankara Narayanan Krishna and Umang Mathur and Andreas Pavlogiannis , title =. Proc

work page
[45]

Fomin and Lukasz Kowalik and Daniel Lokshtanov and D

Marek Cygan and Fedor V. Fomin and Lukasz Kowalik and Daniel Lokshtanov and D. Parameterized Algorithms , publisher =

work page
[46]

Myreen , title =

Peter Sewell and Susmit Sarkar and Scott Owens and Francesco Zappa Nardelli and Magnus O. Myreen , title =. Commun

work page
[47]

Cantin and Mikko H

Jason F. Cantin and Mikko H. Lipasti and James E. Smith , title =

work page
[48]

Ahmed Bouajjani and Constantin Enea and Rachid Guerraoui and Jad Hamza , title =

work page
[49]

Yunji Chen and Yi Lv and Weiwu Hu and Tianshi Chen and Haihua Shen and Pengyu Wang and Hong Pan , title =

work page
[50]

Chaiyasit Manovit and Sudheendra Hangal , title =

work page
[51]

Shaz Qadeer , title =

work page
[52]

Reps , title =

Akash Lal and Thomas W. Reps , title =

work page
[53]

Biswas, Ranadeep and Enea, Constantin , title =. Proc. ACM Program. Lang. , month = oct, articleno =. 2019 , issue_date =. doi:10.1145/3360591 , abstract =

work page doi:10.1145/3360591 2019
[54]

Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II 31 , pages=

On the complexity of checking consistency for replicated data types , author=. Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II 31 , pages=. 2019 , organization=

work page 2019
[55]

ACM Trans

Furbach, Florian and Meyer, Roland and Schneider, Klaus and Senftleben, Maximilian , title =. ACM Trans. Embed. Comput. Syst. , month = sep, articleno =. 2015 , issue_date =. doi:10.1145/2753761 , abstract =

work page doi:10.1145/2753761 2015
[56]

25th Annual European Symposium on Algorithms (ESA 2017) , pages =

Chini, Peter and Kolberg, Jonathan and Krebs, Andreas and Meyer, Roland and Saivasan, Prakash , title =. 25th Annual European Symposium on Algorithms (ESA 2017) , pages =. 2017 , volume =. doi:10.4230/LIPIcs.ESA.2017.27 , annote =

work page doi:10.4230/lipics.esa.2017.27 2017
[57]

International conference on tools and algorithms for the construction and analysis of systems , pages=

Context-bounded model checking of concurrent software , author=. International conference on tools and algorithms for the construction and analysis of systems , pages=. 2005 , organization=

work page 2005
[58]

Proceedings of the ACM on Programming Languages , volume=

The reads-from equivalence for the TSO and PSO memory models , author=. Proceedings of the ACM on Programming Languages , volume=. 2021 , publisher=

work page 2021
[59]

Linear Time Memory Consistency Verification , year=

Hu, Weiwu and Chen, Yunji and Chen, Tianshi and Qian, Cheng and Li, Lei , journal=. Linear Time Memory Consistency Verification , year=

work page
[60]

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) , year=

Global model checking of ordered multi-pushdown systems , author=. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) , year=

work page 2010
[61]

34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) , year=

On bounded reachability analysis of shared memory systems , author=. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014) , year=

work page 2014
[62]

IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science , year=

Analyzing asynchronous programs with preemption , author=. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science , year=

work page
[63]

International Conference on Concurrency Theory , pages=

On the reachability analysis of acyclic networks of pushdown systems , author=. International Conference on Concurrency Theory , pages=. 2008 , organization=

work page 2008
[64]

22nd Annual IEEE symposium on logic in computer science (LICS 2007) , pages=

A robust class of context-sensitive languages , author=. 22nd Annual IEEE symposium on logic in computer science (LICS 2007) , pages=. 2007 , organization=

work page 2007
[65]

International Conference on Concurrency Theory , pages=

Reachability of multistack pushdown systems with scope-bounded matching relations , author=. International Conference on Concurrency Theory , pages=. 2011 , organization=

work page 2011
[66]

Adve and Kourosh Gharachorloo , title =

Sarita V. Adve and Kourosh Gharachorloo , title =. Computer , volume =. 1996 , url =. doi:10.1109/2.546611 , timestamp =

work page doi:10.1109/2.546611 1996
[67]

Steinke and Gary J

Robert C. Steinke and Gary J. Nutt , title =. J. 2004 , url =. doi:10.1145/1017460.1017464 , timestamp =

work page doi:10.1145/1017460.1017464 2004
[68]

Thinniyam and Georg Zetzsche , editor =

Pascal Baumann and Moses Ganardi and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche , editor =. Context-Bounded Analysis of Concurrent Programs (Invited Talk) , booktitle =. 2023 , url =. doi:10.4230/LIPICS.ICALP.2023.3 , timestamp =

work page doi:10.4230/lipics.icalp.2023.3 2023
[69]

Bounded Verification of Multi-threaded Programs via Lazy Sequentialization , journal =

Omar Inverso and Ermenegildo Tomasco and Bernd Fischer and Salvatore. Bounded Verification of Multi-threaded Programs via Lazy Sequentialization , journal =. 2022 , url =. doi:10.1145/3478536 , timestamp =

work page doi:10.1145/3478536 2022
[70]

Optimal Bounded Partial Order Reduction , booktitle =

Iason Marmanis and Viktor Vafeiadis , editor =. Optimal Bounded Partial Order Reduction , booktitle =. 2023 , url =. doi:10.34727/2023/ISBN.978-3-85448-060-0\_16 , timestamp =

work page doi:10.34727/2023/isbn.978-3-85448-060-0 2023
[71]

Formal Methods in System Design , volume =

Patrice Godefroid , title =. Formal Methods in System Design , volume =. 2005 , pages =

work page 2005
[72]

Finding and Reproducing Heisenbugs in Concurrent Programs , booktitle =

Madanlal Musuvathi and Shaz Qadeer and Thomas Ball and G. Finding and Reproducing Heisenbugs in Concurrent Programs , booktitle =. 2008 , pages =

work page 2008
[73]

Maria Christakis and Alkis Gotovos and Konstantinos Sagonas , title =. Sixth. 2013 , pages =

work page 2013
[74]

Programming Language Design and Implementation (PLDI) , location =

Naling Zhang and Markus Kusano and Chao Wang , title =. Programming Language Design and Implementation (PLDI) , location =. 2015 , publisher =

work page 2015
[75]

2016 , issn =

Brian Norris and Brian Demsky , title =. 2016 , issn =. doi:10.1145/2806886 , acmid =

work page doi:10.1145/2806886 2016
[76]

2022 , url =

Ori Lahav and Udi Boker , title =. 2022 , url =. doi:10.1145/3505273 , timestamp =

work page doi:10.1145/3505273 2022
[77]

An Introduction to Parallel Algorithms , publisher =

Joseph J. An Introduction to Parallel Algorithms , publisher =. 1992 , isbn =

work page 1992
[78]

Kokologiannakis, Michalis and Lahav, Ori and Sagonas, Konstantinos and Vafeiadis, Viktor , title =. Proc. ACM Program. Lang. , month = dec, articleno =. 2017 , issue_date =. doi:10.1145/3158105 , abstract =

work page doi:10.1145/3158105 2017
[79]

Computer Aided Verification - 33rd International Conference,

Michalis Kokologiannakis and Viktor Vafeiadis , title =. Computer Aided Verification - 33rd International Conference,. 2021 , series =

work page 2021
[80]

Kokologiannakis, Michalis and Lahav, Ori and Vafeiadis, Viktor , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2023 , issue_date =. doi:10.1145/3571212 , abstract =

work page doi:10.1145/3571212 2023
[81]

Margalit, Roy and Lahav, Ori , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2021 , issue_date =. doi:10.1145/3434285 , abstract =

work page doi:10.1145/3434285 2021

Showing first 80 references.