pith. sign in

arxiv: 2606.20134 · v1 · pith:FY2LMMAEnew · submitted 2026-06-18 · 💻 cs.LO · cs.PL

An MSO Framework for Weak-Memory Verification and Robustness

Giovanna Kobus Conrado , Andreas Pavlogiannis This is my paper

Pith reviewed 2026-06-26 15:18 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords weak memory modelsMSO logictreewidthprogram verificationreads-from robustnessTSOsequential consistencyrelease acquire
0
0 comments X

The pith

Sequential consistency executions have bounded treewidth while TSO executions do not, allowing MSO to axiomatize some but not all weak memory models for verification.

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

The paper establishes that executions under sequential consistency admit bounded treewidth, in contrast to those under total store order. It further shows that a range of models including release/acquire and RC20 can be expressed in monadic second-order logic, whereas strong release/acquire and TSO cannot unless the orthogonal vectors problem admits a linear-time algorithm. These facts yield an algorithm that, for any program, either verifies it under an MSO-axiomatizable model or reports that the program fails reads-from robustness. The results supply a uniform metatheory for handling verification and robustness questions across multiple memory models at once.

Core claim

Executions under SC have bounded treewidth while those under TSO do not; a broad range of models including Release/Acquire and RC20 are MSO-axiomatizable while Strong Release/Acquire and TSO are not unless the Orthogonal Vectors problem can be solved in linear time; for MSO-axiomatizable MM there is an algorithm that for every program P either verifies P under MM or reports that P is not reads-from robust against MM.

What carries the argument

Monadic second-order logic (MSO) axiomatizations of memory models paired with treewidth bounds on their executions.

If this is right

  • For any MSO-axiomatizable model MM an algorithm exists that decides verification of P under MM or detects failure of reads-from robustness.
  • SC executions admit bounded treewidth while TSO executions do not.
  • Release/Acquire and the full RC20 model are MSO-axiomatizable.
  • Strong Release/Acquire and TSO are not MSO-axiomatizable unless Orthogonal Vectors has a linear-time algorithm.

Where Pith is reading between the lines

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

  • The same treewidth separation could be used to compare the algorithmic complexity of verification under additional memory models beyond those studied.
  • If reads-from robustness turns out to be decidable for non-MSO models by other means, the framework would still separate the models that allow uniform MSO treatment from those that do not.
  • The bounded-treewidth property for SC might extend to other strong consistency models whose executions remain series-parallel or have low treewidth.

Load-bearing premise

The claim that certain models are not MSO-axiomatizable in linear time rests on the Orthogonal Vectors problem requiring quadratic time.

What would settle it

An explicit linear-time algorithm for Orthogonal Vectors on worst-case instances would falsify the non-axiomatizability results for TSO and Strong Release/Acquire.

read the original abstract

Memory models are formal specifications of concurrent-program executions, accounting for weak behaviors introduced by compiler and architectural optimizations. The increase of their number and complexity has spawned efforts for uniform verification across whole classes of models, by axiomatizing the models in an adequate metatheory that admits a uniform treatment. In this work, we formally study Monadic Second-Order logic (MSO) as a metatheory for weak memory, by proving results on the treewidth and MSO-expressibility of various popular weak-memory models, as this combination allows us to uniformly tackle several verification problems. In summary, our results are as follows. First, we prove that executions under Sequential Consistency ($\mathsf{SC}$) have bounded treewidth, while already those under Total Store Order ($\mathsf{TSO}$) do not. Second, we prove that a broad range of models, including Release/Acquire and the full RC20, are MSO-axiomatizable, while others, such as Strong Release/Acquire and $\mathsf{TSO}$, are not, unless the Orthogonal Vectors problem $\unicode{x2013}$ which requires quadratic time under SETH $\unicode{x2013}$ can be solved in linear time. Finally, we introduce the notion of reads-from robustness, as an extension to recent work on coarse robustness criteria. We show that our treewidth bounds (both upper and lower) have far-reaching algorithmic implications for any of our MSO-axiomatizable models $\mathsf{MM}$: there is an algorithm that, for every program $\mathsf{P}$, either verifies $\mathsf{P}$ under $\mathsf{MM}$ or reports that $\mathsf{P}$ is not reads-from robust against $\mathsf{MM}$. Overall, our results establish a rich and versatile theoretical framework for weak-memory verification and robustness.

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.

Referee Report

0 major / 2 minor

Summary. The paper claims that executions under Sequential Consistency (SC) have bounded treewidth while those under Total Store Order (TSO) do not; a broad range of models including Release/Acquire and the full RC20 are MSO-axiomatizable while Strong Release/Acquire and TSO are not unless the Orthogonal Vectors problem can be solved in linear time under SETH; and for any MSO-axiomatizable memory model MM there is an algorithm that, for every program P, either verifies P under MM or reports that P is not reads-from robust against MM.

Significance. If the results hold, they establish a versatile theoretical framework for weak-memory verification by combining MSO axiomatizations with treewidth bounds, enabling uniform algorithmic treatment of verification and robustness problems via Courcelle-type results. The paper explicitly separates models via treewidth upper/lower bounds, provides direct MSO axiomatizations for several models, and frames conditional non-expressibility results as standard fine-grained complexity lower bounds under SETH rather than unconditional claims. These elements support the algorithmic consequence for reads-from robustness.

minor comments (2)
  1. [Abstract] Abstract, final paragraph: the statement that TSO and Strong RA 'are not' MSO-axiomatizable should be qualified in the abstract itself as 'are not, unless OV is solvable in linear time under SETH' to match the precise conditional claim made later in the manuscript.
  2. [Introduction] The manuscript would benefit from an explicit pointer in the introduction or §1 to the location of the treewidth proofs (upper bound for SC, lower bound for TSO) and the MSO axiomatization constructions, as the abstract only asserts their existence.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our results on treewidth bounds, MSO axiomatizability, and the algorithmic implications for reads-from robustness, as well as for recommending minor revision.

Circularity Check

0 steps flagged

No significant circularity; derivations are self-contained theoretical proofs

full rationale

The paper presents direct proofs of treewidth bounds (SC bounded, TSO unbounded), explicit MSO axiomatizations for models like Release/Acquire and RC20, and conditional non-expressibility results for TSO/Strong RA that rest on the external SETH assumption for Orthogonal Vectors (standard fine-grained complexity). The algorithmic consequence for reads-from robustness follows from the MSO + bounded-treewidth combination via Courcelle's theorem. No self-definitional steps, fitted inputs renamed as predictions, load-bearing self-citations, or ansatzes smuggled via prior work are present in the abstract or described claims. All central results are framed as new proofs independent of the paper's own fitted quantities or prior author results.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based on the abstract alone, no free parameters, ad-hoc axioms, or invented entities are specified; the work relies on standard concepts from logic and complexity theory such as MSO and SETH.

pith-pipeline@v0.9.1-grok · 5859 in / 1212 out tokens · 21065 ms · 2026-06-26T15:18:04.440196+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

98 extracted references · 75 canonical work pages

  1. [1]

    2020 , isbn =

    Mathur, Umang and Pavlogiannis, Andreas and Viswanathan, Mahesh , title =. 2020 , isbn =. doi:10.1145/3373718.3394783 , booktitle =

    work page doi:10.1145/3373718.3394783 2020

  2. [2]

    Reasoning

    Cyriac, Aiswarya and Gastin, Paul , year = 2014, journal =. Reasoning. doi:10.4230/LIPICS.FSTTCS.2014.11 , abstract =

    work page doi:10.4230/lipics.fsttcs.2014.11 2014

  3. [3]

    Stateless

    Agarwal, Pratyush and Chatterjee, Krishnendu and Pathak, Shreya and Pavlogiannis, Andreas and Toman, Viktor , editor =. Stateless. Computer. doi:10.1007/978-3-030-81685-8_16 , url =

    work page doi:10.1007/978-3-030-81685-8_16

  4. [4]

    Proceedings of the 24th European Conference on Object-Oriented Programming , pages =

    Owens, Scott , title =. Proceedings of the 24th European Conference on Object-Oriented Programming , pages =. 2010 , isbn =

    2010

  5. [5]

    Narayan , editor =

    Cyriac, Aiswarya and Gastin, Paul and Kumar, K. Narayan , editor =. doi:10.1007/978-3-642-32940-1_38 , abstract =

    work page doi:10.1007/978-3-642-32940-1_38

  6. [6]

    Sistla, A. P. and Clarke, E. M. , title =. J. ACM , month = jul, pages =. 1985 , issue_date =. doi:10.1145/3828.3837 , abstract =

    work page doi:10.1145/3828.3837 1985

  7. [7]

    Egor Derevenetc , title =

  8. [8]

    Podkopaev, Anton and Lahav, Ori and Vafeiadis, Viktor , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2019 , issue_date =. doi:10.1145/3290382 , abstract =

    work page doi:10.1145/3290382 2019

  9. [9]

    and Vafeiadis, Viktor

    Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Godbole, Adwait and Krishna, S. and Vafeiadis, Viktor. The Decidability of Verification under PS 2.0. Programming Languages and Systems. 2021

    2021

  10. [10]

    Formal Methods in System Design , volume =

    A Formal Hierarchy of Weak Memory Models , author =. Formal Methods in System Design , volume =. doi:10.1007/s10703-012-0161-5 , abstract =

    work page doi:10.1007/s10703-012-0161-5

  11. [11]

    Pulte, Christopher and Flur, Shaked and Deacon, Will and French, Jon and Sarkar, Susmit and Sewell, Peter , title =. Proc. ACM Program. Lang. , month = dec, articleno =. 2017 , issue_date =. doi:10.1145/3158107 , abstract =

    work page doi:10.1145/3158107 2017

  12. [12]

    and Parri, Andrea and Stern, Alan , year = 2018, month = mar, series =

    Alglave, Jade and Maranget, Luc and McKenney, Paul E. and Parri, Andrea and Stern, Alan , year = 2018, month = mar, series =. Frightening. Proceedings of the. doi:10.1145/3173162.3177156 , abstract =

    work page doi:10.1145/3173162.3177156 2018

  13. [13]

    Proceedings of the ACM on Programming Languages , volume =

    Truly Stateless, Optimal Dynamic Partial Order Reduction , author =. Proceedings of the ACM on Programming Languages , volume =. doi:10.1145/3498711 , abstract =

    work page doi:10.1145/3498711

  14. [14]

    Pattern-

    Esparza, Javier and Ganty, Pierre and Poch, Tom. Pattern-. ACM Trans. Program. Lang. Syst. , volume =. doi:10.1145/2629644 , abstract =

    work page doi:10.1145/2629644

  15. [15]

    Context-

    Qadeer, Shaz and Rehof, Jakob , editor =. Context-. Tools and. doi:10.1007/978-3-540-31980-1_7 , abstract =

    work page doi:10.1007/978-3-540-31980-1_7

  16. [16]

    The Reads-from Equivalence for the

    Bui, Truc Lam and Chatterjee, Krishnendu and Gautam, Tushar and Pavlogiannis, Andreas and Toman, Viktor , year = 2021, month = oct, journal =. The Reads-from Equivalence for the. doi:10.1145/3485541 , abstract =

    work page doi:10.1145/3485541 2021

  17. [17]

    Stateless Model Checking for TSO and PSO

    Abdulla, Parosh Aziz and Aronis, Stavros and Atig, Mohamed Faouzi and Jonsson, Bengt and Leonardsson, Carl and Sagonas, Konstantinos. Stateless Model Checking for TSO and PSO. Tools and Algorithms for the Construction and Analysis of Systems. 2015

    2015

  18. [18]

    On the Verification Problem for Weak Memory Models , booktitle =

    Atig, Mohamed Faouzi and Bouajjani, Ahmed and Burckhardt, Sebastian and Musuvathi, Madanlal , year = 2010, month = jan, series =. On the Verification Problem for Weak Memory Models , booktitle =. doi:10.1145/1706299.1706303 , abstract =

    work page doi:10.1145/1706299.1706303 2010

  19. [19]

    Nagar, Kartik and Sahoo, Anmol and Chowdhury, Romit Roy and Jagannathan, Suresh , title =. Proc. ACM Program. Lang. , month = oct, articleno =. 2024 , issue_date =. doi:10.1145/3689802 , abstract =

    work page doi:10.1145/3689802 2024

  20. [20]

    2017 , month = jan, journal =

    Automatically Comparing Memory Consistency Models , author =. 2017 , month = jan, journal =. doi:10.1145/3093333.3009838 , abstract =

    work page doi:10.1145/3093333.3009838 2017

  21. [21]

    and Gupta, Ashutosh and Tuppe, Omkar

    Abdulla, Parosh and Atig, Mohamed Faouzi and Krishna, S. and Gupta, Ashutosh and Tuppe, Omkar. Optimal Stateless Model Checking for Causal Consistency. Tools and Algorithms for the Construction and Analysis of Systems. 2023

    2023

  22. [22]

    An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic , year =

    Hammond, Angus and Liu, Zongyuan and P\'. An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic , year =. Proc. ACM Program. Lang. , month = jan, articleno =. doi:10.1145/3632863 , abstract =

    work page doi:10.1145/3632863

  23. [23]

    SIGPLAN Not

    Vafeiadis, Viktor and Narayan, Chinmay , title =. SIGPLAN Not. , month = oct, pages =. 2013 , issue_date =. doi:10.1145/2544173.2509532 , abstract =

    work page doi:10.1145/2544173.2509532 2013

  24. [24]

    31st European Conference on Object-Oriented Programming (ECOOP 2017) , pages =

    Kaiser, Jan-Oliver and Dang, Hoang-Hai and Dreyer, Derek and Lahav, Ori and Vafeiadis, Viktor , title =. 31st European Conference on Object-Oriented Programming (ECOOP 2017) , pages =. 2017 , volume =. doi:10.4230/LIPIcs.ECOOP.2017.17 , annote =

    work page doi:10.4230/lipics.ecoop.2017.17 2017

  25. [25]

    Probabilistic

    Gao, Mingyu and Chakraborty, Soham and Ozkan, Burcu Kulahcioglu , year = 2023, month = jan, series =. Probabilistic. Proceedings of the 28th. doi:10.1145/3575693.3575729 , abstract =

    work page doi:10.1145/3575693.3575729 2023

  26. [26]

    doi:10.1145/3445814.3446711 , numpages = 17, keywords =

    Luo, Weiyu and Demsky, Brian , year = 2021, booktitle =. doi:10.1145/3445814.3446711 , numpages = 17, keywords =

    work page doi:10.1145/3445814.3446711 2021

  27. [27]

    Graph Minors

    Robertson, Neil and Seymour, P.D , year =. Graph Minors. Journal of Combinatorial Theory, Series B , volume =. doi:10.1016/0095-8956(86)90030-4 , url =

    work page doi:10.1016/0095-8956(86)90030-4

  28. [28]

    Lahav, Ori and Boker, Udi , year =. What's. ACM Transactions on Programming Languages and Systems , volume =. doi:10.1145/3505273 , abstract =

    work page doi:10.1145/3505273

  29. [29]

    2022 , month = oct, journal =

    Haas, Thomas and Meyer, Roland and. 2022 , month = oct, journal =. doi:10.1145/3563292 , url =

    work page doi:10.1145/3563292 2022

  30. [30]

    Di Giusto, Cinzia and Ferr. A. 2023 , month = jan, journal =. doi:10.1145/3571248 , url =

    work page doi:10.1145/3571248 2023

  31. [31]

    Kater: Automating Weak Memory Metatheory and Consistency Checking

    Kokologiannakis, Michalis and Lahav, Ori and Vafeiadis, Viktor , year =. Kater:. Reproduction package for article: "Kater: Automating Weak Memory Metatheory and Consistency Checking" , volume =. doi:10.1145/3571212 , url =

    work page doi:10.1145/3571212

  32. [32]

    2019 , issue_date =

    Pavlogiannis, Andreas , title =. 2019 , issue_date =. doi:10.1145/3371085 , journal =

    work page doi:10.1145/3371085 2019

  33. [33]

    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

  34. [34]

    2021 , eprint=

    Non-Sequential Theory of Distributed Systems , author=. 2021 , eprint=

    2021

  35. [35]

    Graph minors

    Neil Robertson and P.D Seymour , doi =. Graph minors. II. Algorithmic aspects of tree-width , url =. Journal of Algorithms , number =. 1986 , bdsk-url-1 =

    1986

  36. [36]

    TSO to SC via Symbolic Execution , isbn =

    Wehrheim, Heike and Travkin, Oleg , year =. TSO to SC via Symbolic Execution , isbn =

  37. [37]

    IEEE Transactions on Computers , volume =

    How to. IEEE Transactions on Computers , volume =. doi:10.1109/TC.1979.1675439 , abstract =

    work page doi:10.1109/tc.1979.1675439 1979

  38. [38]

    Guohao Li, Hasan Abed Al Kader Hammoud, Hani Itani, Dmitrii Khizbullin, and Bernard Ghanem

    Time, Clocks, and the Ordering of Events in a Distributed System , author =. 1978 , month = jul, journal =. doi:10.1145/359545.359563 , abstract =

    work page doi:10.1145/359545.359563 1978

  39. [39]

    , year =

    Sewell, Peter and Sarkar, Susmit and Owens, Scott and Nardelli, Francesco Zappa and Myreen, Magnus O. , year =. X86-. Communications of the ACM , volume =. doi:10.1145/1785414.1785443 , abstract =

    work page doi:10.1145/1785414.1785443

  40. [40]

    Bollig, Benedikt and Di Giusto, Cinzia and Finkel, Alain and Laversa, Laetitia and Lozes, Etienne and Suresh, Amrita , editor =. A. 2021 , journal =. doi:10.4230/LIPICS.CONCUR.2021.14 , url =

    work page doi:10.4230/lipics.concur.2021.14 2021

  41. [41]

    2011 , month = jan, journal =

    The Tree Width of Auxiliary Storage , author =. 2011 , month = jan, journal =. doi:10.1145/1925844.1926419 , url =

    work page doi:10.1145/1925844.1926419 2011

  42. [42]

    Repairing Sequential Consistency in

    Lahav, Ori and Vafeiadis, Viktor and Kang, Jeehoon and Hur, Chung-Kil and Dreyer, Derek , year =. Repairing Sequential Consistency in. Proceedings of the 38th. doi:10.1145/3062341.3062352 , abstract =

    work page doi:10.1145/3062341.3062352

  43. [43]

    Mathematizing

    Batty, Mark and Owens, Scott and Sarkar, Susmit and Sewell, Peter and Weber, Tjark , year =. Mathematizing. Proceedings of the 38th Annual. doi:10.1145/1926385.1926394 , url =

    work page doi:10.1145/1926385.1926394

  44. [44]

    38th International Symposium on Distributed Computing (DISC 2024) , pages =

    Casta\. 38th International Symposium on Distributed Computing (DISC 2024) , pages =. 2024 , volume =. doi:10.4230/LIPIcs.DISC.2024.11 , annote =

    work page doi:10.4230/lipics.disc.2024.11 2024

  45. [45]

    Adve, S. V. and Hill, Mark D. , year = 1993, month = jun, journal =. A. doi:10.1109/71.242161 , abstract =

    work page doi:10.1109/71.242161 1993

  46. [46]

    Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , pages =

    Abdulla, Parosh Aziz and Arora, Jatin and Atig, Mohamed Faouzi and Krishna, Shankaranarayanan , title =. Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , pages =. 2019 , isbn =. doi:10.1145/3314221.3314649 , abstract =

    work page doi:10.1145/3314221.3314649 2019

  47. [47]

    Bulletin of the American Mathematical Society , year=

    A variant of a recursively unsolvable problem , author=. Bulletin of the American Mathematical Society , year=

  48. [48]

    Graph minors. I. Excluding a forest , author=. Journal of Combinatorial Theory, Series B , volume=

  49. [49]

    Graph minors. II. Algorithmic aspects of tree-width , author=. Journal of algorithms , volume=. 1986 , publisher=

    1986

  50. [50]

    and Kowalik, Lukasz and Lokshtanov, Daniel and Marx, Daniel and Pilipczuk, Marcin and Pilipczuk, Michal and Saurabh, Saket , title =

    Cygan, Marek and Fomin, Fedor V. and Kowalik, Lukasz and Lokshtanov, Daniel and Marx, Daniel and Pilipczuk, Marcin and Pilipczuk, Michal and Saurabh, Saket , title =. 2015 , isbn =

    2015

  51. [51]

    The monadic second-order logic of graphs

    Bruno Courcelle , doi =. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs , url =. Information and Computation , number =. 1990 , bdsk-url-1 =

    1990

  52. [52]

    Seese , doi =

    D. Seese , doi =. The structure of the models of decidable monadic theories of graphs , url =. Annals of Pure and Applied Logic , number =. 1991 , bdsk-url-1 =

    1991

  53. [53]

    Definability equals recognizability for graphs of bounded treewidth , year =

    Boja\'. Definability equals recognizability for graphs of bounded treewidth , year =. Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science , pages =. doi:10.1145/2933575.2934508 , abstract =

    work page doi:10.1145/2933575.2934508

  54. [54]

    , title =

    Boehm, Hans-J. , title =. Proceedings of the 2012 ACM SIGPLAN Workshop on Memory Systems Performance and Correctness , pages =. 2012 , isbn =. doi:10.1145/2247684.2247688 , abstract =

    work page doi:10.1145/2247684.2247688 2012

  55. [56]

    Explaining

    Lahav, Ori and Vafeiadis, Viktor , editor =. Explaining. doi:10.1007/978-3-319-48989-6_29 , abstract =

    work page doi:10.1007/978-3-319-48989-6_29

  56. [57]

    , title =

    Bodlaender, Hans L. , title =. 1993 , isbn =. doi:10.1145/167088.167161 , booktitle =

    work page doi:10.1145/167088.167161 1993

  57. [58]

    In: Castagna, G., Gordon, A.D

    Kang, Jeehoon and Hur, Chung-Kil and Lahav, Ori and Vafeiadis, Viktor and Dreyer, Derek , year = 2017, month = jan, series =. A Promising Semantics for Relaxed-Memory Concurrency , booktitle =. doi:10.1145/3009837.3009850 , abstract =

    work page doi:10.1145/3009837.3009850 2017

  58. [59]

    Bounding Data Races in Space and Time , booktitle =

    Dolan, Stephen and Sivaramakrishnan, Kc and Madhavapeddy, Anil , year = 2018, month = jun, pages =. Bounding Data Races in Space and Time , booktitle =. doi:10.1145/3192366.3192421 , abstract =

    work page doi:10.1145/3192366.3192421 2018

  59. [60]

    Vafeiadis, Viktor and Balabonski, Thibaut and Chakraborty, Soham and Morisset, Robin and Zappa Nardelli, Francesco , year = 2015, month = jan, pages =. Common. Proceedings of the 42nd. doi:10.1145/2676726.2676995 , abstract =

    work page doi:10.1145/2676726.2676995 2015

  60. [61]

    2017 , month = jan, journal =

    On Verifying Causal Consistency , author =. 2017 , month = jan, journal =. doi:10.1145/3093333.3009888 , abstract =

    work page doi:10.1145/3093333.3009888 2017

  61. [62]

    Margalit, Roy and Kokologiannakis, Michalis and Itzhaky, Shachar and Lahav, Ori , year = 2025, month = jun, journal =. Dynamic. doi:10.1145/3729277 , abstract =

    work page doi:10.1145/3729277 2025

  62. [63]

    Richard Büchi, Weak second-order arithmetic and finite automata , Z

    Büchi, J. Richard , title =. Mathematical Logic Quarterly , volume =. doi:https://doi.org/10.1002/malq.19600060105 , url =. https://onlinelibrary.wiley.com/doi/pdf/10.1002/malq.19600060105 , year =

    work page doi:10.1002/malq.19600060105

  63. [64]

    Non-Sequential Theory of Distributed Systems , publisher =

    Bollig, Benedikt and Gastin, Paul , keywords =. Non-Sequential Theory of Distributed Systems , publisher =. 2019 , copyright =. doi:10.48550/ARXIV.1904.06942 , url =

    work page doi:10.48550/arxiv.1904.06942 2019

  64. [65]

    Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , pages =

    Lahav, Ori and Margalit, Roy , title =. Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation , pages =. 2019 , isbn =. doi:10.1145/3314221.3314604 , abstract =

    work page doi:10.1145/3314221.3314604 2019

  65. [66]

    Moiseenko, Evgenii and Meluzzi, Matteo and Meleshchenko, Innokentii and Kabashnyi, Ivan and Podkopaev, Anton and Chakraborty, Soham , year =. Relaxed. Xmm Model Checker Benchmarks , volume =. doi:10.1145/3704908 , url =

    work page doi:10.1145/3704908

  66. [67]

    Chakraborty, Soham and Krishna, Shankara Narayanan and Mathur, Umang and Pavlogiannis, Andreas , year =. How. Proceedings of the ACM on Programming Languages , volume =. doi:10.1145/3632908 , url =

    work page doi:10.1145/3632908

  67. [68]

    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

  68. [69]

    Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I , pages =

    Kokologiannakis, Michalis and Vafeiadis, Viktor , title =. Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I , pages =. 2021 , isbn =. doi:10.1007/978-3-030-81685-8_20 , abstract =

    work page doi:10.1007/978-3-030-81685-8_20 2021

  69. [70]

    Reconciling Preemption Bounding with DPOR

    Marmanis, Iason and Kokologiannakis, Michalis and Vafeiadis, Viktor. Reconciling Preemption Bounding with DPOR. Tools and Algorithms for the Construction and Analysis of Systems. 2023

    2023

  70. [71]

    Chini, Peter and Kolberg, Jonathan and Krebs, Andreas and Meyer, Roland and Saivasan, Prakash , year = 2017, journal =. On the. doi:10.4230/LIPICS.ESA.2017.27 , abstract =

    work page doi:10.4230/lipics.esa.2017.27 2017

  71. [72]

    SIGPLAN Not

    Musuvathi, Madanlal and Qadeer, Shaz , title =. SIGPLAN Not. , month = jun, pages =. 2007 , issue_date =. doi:10.1145/1273442.1250785 , abstract =

    work page doi:10.1145/1273442.1250785 2007

  72. [73]

    Getting Rid of Store-Buffers in TSO Analysis

    Atig, Mohamed Faouzi and Bouajjani, Ahmed and Parlato, Gennaro. Getting Rid of Store-Buffers in TSO Analysis. Computer Aided Verification. 2011

    2011

  73. [74]

    Verification under TSO with an infinite Data Domain

    Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Furbach, Florian and Garg, Shashwat. Verification under TSO with an infinite Data Domain. Tools and Algorithms for the Construction and Analysis of Systems. 2024

    2024

  74. [75]

    Dynamic Partial-Order Reduction for Model Checking Software , booktitle =

    Flanagan, Cormac and Godefroid, Patrice , year = 2005, month = jan, series =. Dynamic Partial-Order Reduction for Model Checking Software , booktitle =. doi:10.1145/1040305.1040315 , abstract =

    work page doi:10.1145/1040305.1040315 2005

  75. [76]

    Optimal Dynamic Partial Order Reduction , booktitle =

    Abdulla, Parosh and Aronis, Stavros and Jonsson, Bengt and Sagonas, Konstantinos , year = 2014, month = jan, series =. Optimal Dynamic Partial Order Reduction , booktitle =. doi:10.1145/2535838.2535845 , abstract =

    work page doi:10.1145/2535838.2535845 2014

  76. [77]

    Proceedings of the ACM on Programming Languages , volume =

    Data-Centric Dynamic Partial Order Reduction , author =. Proceedings of the ACM on Programming Languages , volume =. doi:10.1145/3158119 , abstract =

    work page doi:10.1145/3158119

  77. [78]

    2017 , eprint=

    Computing Tree Decompositions with FlowCutter: PACE 2017 Submission , author=. 2017 , eprint=

    2017

  78. [79]

    On the State Reachability Problem for Concurrent Programs Under Power

    Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Bouajjani, Ahmed and Derevenetc, Egor and Leonardsson, Carl and Meyer, Roland. On the State Reachability Problem for Concurrent Programs Under Power. Networked Systems. 2021

    2021

  79. [80]

    doi:10.1145/3276505 , issue_date =

    Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Jonsson, Bengt and Ngo, Tuan Phong , year = 2018, journal =. doi:10.1145/3276505 , issue_date =

    work page doi:10.1145/3276505 2018

  80. [81]

    doi:10.1007/978-3-662-47666-6\_25 , editor =

    Lahav, Ori and Vafeiadis, Viktor , year = 2015, booktitle =. doi:10.1007/978-3-662-47666-6\_25 , editor =

    work page doi:10.1007/978-3-662-47666-6 2015

Showing first 80 references.