Pith. sign in

REVIEW 2 major objections 6 minor 43 references

Revisiting Stateful Partial-Order Reduction

T0 review · 2 major / 6 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 claims that stateful partial-order reduction cannot be approximated within any polynomial factor unless P=NP, and it backs the claim with a 3-SAT reduction plus a practical heuristic algorithm.

desk verdict A genuinely useful reformulation of stateful POR with a plausible but currently unproven lower bound; Lemma 29 needs a missing argument and Lemma 17 needs a correction. read the letter →

arxiv 2411.16921 v1 pith:24AGV4VI submitted 2024-11-25 cs.LO

Frédéric Herbreteau , Sarah Larroze-Jardiné , Gérald Point , Igor Walukiewicz This is my paper · ORCID
classification cs.LO MSC 68Q6068Q8568Q17
keywords statefulpartial-orderreductionMazurkiewicztracessleepsetscoveringsourceIFSoracleNP-hardnessmodelcheckingconcurrentsystems
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 tackles stateful partial-order reduction, where the goal is to build a reduced transition system containing one representative run from each equivalence class of a concurrent system's runs. Its central result is negative: assuming P is not equal to NP, no algorithm can construct a sound and complete reduced transition system whose size is bounded by any polynomial in the size of the smallest possible such system while running in polynomial time in input plus output. The positive contribution is to isolate a simple oracle, IFS, which asks whether exploration from a state is already covered, and to show that this oracle is NP-hard. The paper then develops polynomial-time heuristic approximations of IFS, packaged into a sound and complete reduction algorithm that uses sleep sets and covering source sets, and reports experiments where it outperforms persistent-set-based reduction by orders of magnitude.

What carries the argument

The central objects are first sets and covering source sets. For a por-equivalence on runs, first(u) is the set of actions that can start a run equivalent to u, and a covering source set in a state intersects the first set of every maximal run from that state; following only actions in covering source sets preserves all equivalence classes. The IFS oracle asks whether a given set B includes the first set of some maximal run from state s. Sleep sets record which actions need not be explored because equivalent runs were already seen, and lexicographic ordering selects representative runs. The heuristic PIFS replaces the global run-existence question by local runs of individual processes and a sticking closure between actions, while closure(s,b) builds a covering source set from a chosen action. The carrying mechanism is the pattern of Lemma 32, a staircase of actions whose domains successively wrap all enabled actions, which characterizes exactly when IFS holds.

What would settle it

Run the Section 8 construction on a 3-CNF formula with exponentially many satisfying assignments: if any algorithm, in polynomial time, outputs a sound and complete reduced transition system for the resulting client/server system with fewer states than the number of satisfying valuations, then Theorem 26 is refuted.

Watch

Extended reading notes

Core claim

The paper's main claim is Theorem 26: if P is not equal to NP, then no excellent partial-order reduction algorithm exists, meaning no algorithm that, in time polynomial in the size of the input system plus the minimal reduced transition system, outputs a sound and complete reduced transition system of size at most polynomial in that minimum. In other words, the smallest sound and complete reduced state graph cannot be efficiently approximated within any polynomial factor. The paper also proves that the IFS oracle, which asks whether a given set of actions contains the first set of some maximal run from a state, is NP-complete. In response to these hardness results, it proposes an idealized trace-optimal algorithm based on lexicographic order and sleep sets, and then a practical algorithm replacing IFS with the PIFS and rPIFS heuristics, with a proof that the resulting reduced transition system is sound and complete.

Load-bearing premise

The lower-bound argument relies on treating a state in a reduced transition system as a genuine global state: if several histories reach the same node, any outgoing transition must be executable after every one of those histories, and merging states cannot create transitions that are valid for only some of them.

Editorial extensions

If this is right

  • Any future stateful partial-order method aimed at guaranteed near-optimal reduced graphs must overcome the P versus NP barrier, so heuristic or approximate methods are the only viable route.
  • The IFS viewpoint reframes partial-order reduction from deciding which actions to explore into deciding when to stop; any correct heuristic must answer 'yes' whenever IFS holds, giving a one-sided error condition.
  • For non-blocking read/write systems without synchronization primitives, the IFS test becomes linear-time, yielding a simple trace-optimal stateless exploration algorithm for that class.
  • The closure-based covering source sets are always covering and are no larger than the persistent sets used as the baseline, which explains the reported gains of the new algorithm across the benchmark models.
  • Because the lower-bound construction uses only binary synchronizations with blocking, the inapproximability transfers to any model that can encode this client/server pattern.

Reading between the lines

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

  • The lower bound likely extends to stateless partial-order reduction in the presence of blocking, since the proof does not rely on stored states; if so, the recent trace-optimal polynomial-memory stateless algorithms for non-blocking systems cannot be adapted to locks without losing polynomial-time near-optimality.
  • The IFS heuristic framework suggests a concrete research line: approximate IFS with SAT solvers or with k-Cartesian abstractions, both of which the paper mentions as possibilities but does not evaluate.
  • Combining race-reversal heuristics with PIFS is a natural next step, since the paper shows race reversal is another approximation of IFS but leaves its integration with the new algorithm open.
  • The implementation claims rest on an empirical completeness check rather than a machine-checked proof of the code, so a formally verified implementation of Listing 6 would be a natural follow-up.
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.

Referee Report

2 major / 6 minor

Summary. The paper develops a stateful partial-order reduction framework for client/server systems with blocking, centered on an "includes first set" (IFS) oracle. It presents an idealized lex-first exploration algorithm with sleep sets and an IFS oracle (Listings 1 and 2), proves NP-hardness of the IFS test, and states a strong lower bound (Theorem 26) claiming that no polynomial-time algorithm can construct a reduced transition system whose size is polynomially close to the minimum unless P=NP. It then introduces one-sided heuristics PIFS and rPIFS, a closure-based covering source set construction, and a practical algorithm (Listing 6), with an implementation and experiments on several benchmarks.

Significance. If the lower bound can be made rigorous, it would be the first inapproximability result for stateful partial-order reduction in the presence of blocking, and the IFS/PIFS viewpoint is a genuinely useful conceptual reframing of the "when to stop exploring" question. The constructive side is promising: the PIFS characterization (Lemma 32), the closure construction (Lemma 37), and the experimental validation against independently computed complete transition systems via Proposition 7 are concrete strengths. The paper does not ship machine-checked proofs or code, but the completeness checks on random and literature models give useful evidence for the implementation. However, two load-bearing technical points -- the state-counting step in Lemma 29 and the internal contradiction around Lemma 17(i) -- need to be resolved before the main claims can be accepted.

major comments (2)
  1. [§8, Lemma 29 and Definition 5] The proof of Lemma 29 infers that, because the global states s1 and s2 reached after e on w_v1 and w_v2 are distinct for distinct satisfying valuations, every sound and complete reduced transition system for P_phi must have at least as many states as satisfying valuations. This inference is not licensed by Definition 5, which only requires every full run of TSr to be a full run of TS and does not require the states of TSr to be states of TS(P). A small acyclic action-deterministic transition system can contain exponentially many full runs (for example, a chain q0 -> q1 -> ... -> qm with two differently labeled transitions at each level), so distinct global states may be merged in TSr. Since Corollary 30 and Theorem 26 rely on this state-counting step, the main inapproximability result is not established as written. The authors should either provide a genuine lower bound on the number of states needed by any TSr whose full-run language contains all runs w_v while remaining a subset of the full runs of TS(P), or explicitly restrict Definition 5 and Definition 25 to reduced transition systems whose states are states of TS(P) (or nodes of the exploration graph) and restate the theorem for that setting.
  2. [§6, Lemma 17] Lemma 17(i) states that every full run in the graph built by Listing 2 is a full lex-run of TS(P), but the paragraph immediately before the lemma says that edges added by the subsumption rule may create paths that are not lex-runs. The proof of (i) is only "direct from the algorithm," which is inconsistent with the preceding remark. This matters because the correctness argument for Listing 6 in §10.3 invokes Lemma 17 as the correctness statement for Listing 2. Please remove or repair (i), prove the soundness and completeness parts separately, and prove the lex-usefulness of states without relying on (i).
minor comments (6)
  1. [§6, Listings 1 and 2] The comment on line 6 of both listings, "Sl = sleep(n) union {labels of transitions outgoing from n}," is misleading; it should say "labels of transitions already explored from n," since Sl is built incrementally in the while loop.
  2. [§6, Remark 21] The claim that Listing 1 remains optimal when line 9 chooses actions arbitrarily rather than in the fixed linear order is plausible but not proved; the proof of Lemma 15 uses the fixed order in an essential way, so a separate argument should be supplied if the remark is retained.
  3. [§8, Figure 7] The two client processes for each variable are hard to distinguish in Figure 7, and the text "Similarly, for client Ci but now we have theta_i, lambda_i, and x_i actions" is difficult to parse; please clarify the notation and the figure labels.
  4. [§11, Table 1] Several rows of Table 1 are difficult to read in the current formatting, with missing or misplaced entries (for example, the fs rows); please reformat the table so that each column is clearly aligned.
  5. [§11, implementation paragraph] The sentence "Even if we verified the abstract algorithm from Listing 6 in Coq, that we are not capable of" is confusing and could be misread as claiming a Coq verification was performed; rephrase to state clearly that no such formal verification was done.
  6. [References] References [3] and [15] are incomplete (missing publication venue/year), and reference [32] lacks the journal name; please complete the bibliographic data.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the lower bound and NP-hardness results are self-contained SAT reductions, and the heuristics are validated against independently computed complete systems.

full rationale

The paper's central theoretical claims are not circular. The lex-first exploration algorithm with sleep sets and the IFS oracle (Lemma 15 and Lemma 17) is proved by an induction on the construction tree, using first-set and sleep-set invariants; it does not assume trace-optimality. The NP-hardness of the IFS test (Proposition 23) is a direct encoding of 3SAT into a client/server system, and the conclusion is read off from satisfiability rather than from the definition of IFS. Theorem 26 is a conditional lower bound: assuming P != NP, an excellent POR algorithm would solve SAT by running on a formula-derived system, with the size gap supplied by the number of satisfying valuations. This is a reduction, not an equation of a result with its input. The heuristic PIFS/rPIFS tests are explicit over-approximations with a proven one-sided-error direction (Lemma 34), and they are not fitted to benchmark data; the experimental claims are checked against independently computed first sets using Proposition 7, which itself has a self-contained proof. The skeptical concern about Lemma 29—that distinct global states reached after different satisfying valuations are asserted to force distinct states in every sound and complete reduced transition system, although Definition 5 permits arbitrary abstract states—is a proof-gap/correctness concern, not a circularity: the step is not justified by the definitions, but it is also not an instance of a fitted input being relabeled as a prediction, nor of a self-citation carrying the argument. Self-citations such as [17] appear only as an application topic in the introduction and are not load-bearing. No uniqueness theorem is imported from the authors' prior work, and no known result is merely renamed while being presented as new; the paper explicitly attributes the source-set formulation to [1]. Overall, the derivation chain is self-contained, so no circular step is exhibited.

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

No free parameters are fitted; the algorithms contain no numeric constants chosen on data. The analysis rests on standard assumptions (P≠NP, acyclicity of clients, Mazurkiewicz trace equivalence, action determinism). No new entities are postulated.

assumptions (4)
  • standard math P ≠ NP
    Theorem 26 is conditional on this; if P=NP the stated lower bound is vacuous.
  • domain assumption Clients are acyclic; every action synchronizes exactly one client and one server
    Definition 2 and Remark 4: this guarantees the global transition system TS(P) is acyclic, which is needed for Proposition 7, the algorithms, and the lower bound construction.
  • domain assumption Mazurkiewicz trace equivalence is the por-equivalence
    Definition 10 and Proposition 11: all results are for trace equivalence based on domain-disjoint independence; coarser equivalences are explicitly left to future work.
  • domain assumption Action determinism of transition systems
    Definition 1: at most one outgoing transition per label per state, used in the proof of Lemma 15 and in the state-identity argument in Lemma 29.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Revisiting Stateful Partial-Order Reduction." pith.science (2026). https://pith.science/paper/24AGV4VI

@misc{pith2026241116921,
  author       = {Pith},
  title        = {Pith review of: Revisiting Stateful Partial-Order Reduction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/24AGV4VI}},
  note         = {Machine review of arXiv:2411.16921}
}
read the original abstract

The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective. We focus on a stateful method for systems with blocking operations, like locks. First, we show a simple algorithm with an oracle that is trace-optimal if used as a stateless algorithm. The algorithm is not practical, though, as the oracle uses an NP-hard test. Next, we present a significant negative result showing that in stateful exploration with blocking, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. This lower bound result justifies looking for heuristics for our simple algorithm with an oracle. As the third contribution, we present a practical algorithm going beyond the standard stubborn/persistent/ample set approach. We report on the implementation and evaluation of the algorithm.

Figures

Figures reproduced from arXiv: 2411.16921 by the authors.

Figure 1
Figure 1. An example of a client/server system (left) with clients [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. A counterexample to Proposition 7 in presence of infinite runs [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. A covering source set may not be a persistent set. [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Sleep sets are needed for optimality Pi∈[1,n] • • • • ai bi ci di Si∈[1,n] • ai, bi, ci, di Small transition system • • • • a1 b1 c1 d1 · · · • • • • an bn cn dn Big transition system • • • • • • • a1 b1 an bn . . . • • • • • • c1 d1 cn dn . . . 2 n [PITH_FULL_IMAGE:f…
Figure 5
Figure 5. Figure 5: A client/server system with two optimal transition systems, one of linear size and one of exponential size ba ∼ ab so this is not trace-optimal. Observe that with sleep sets we get a ∈ sleep(nb) which is exactly what is needed to block unnecessary exploration. So our i…
Figure 6
Figure 6. Figure 6: A client/server system Pφ encoding SAT(φ) for a 3CNF formula φ this algorithm because, as we show in this section, the IFS(s, B) test is NP-hard. This leads us to study approximations of this test in Section 9. In the NP-hardness proof, we construct client/server syste…
Figure 7
Figure 7. Figure 7: Program Pφ for the lower bound argument. • • • • • e θ1 θ1 λ1 λ1 • • • • θn θn λn λn • α 1 1 α 1 2 α 1 3 • • α k 1 α k 2 α k 3 • b [PITH_FULL_IMAGE:figures/full_fig_p017_7.png]
Figure 9
Figure 9. Figure 9: Conditions of Lemma 32 looking for a run u where every action a enabled in s which is not in B, is preceded by an action b such that dom(a) ∩ dom(b) ̸= ∅. As shown in [PITH_FULL_IMAGE:figures/full_fig_p020_9.png]
Figure 10
Figure 10. Figure 10: Comparison of algorithms reach, pset+sleep and full+sleep on the “Dining Philosophers” model, with the main loop unfolded once (left), and twice (right). Experiments have been ran on a MacBook Air M2 with 16Gb of memory, and with a timeout of 15min. 0 2x106 4x106 6x10…
Figure 11
Figure 11. Figure 11: Comparison of algorithms pset+sleep and full+sleep on the “Multi locks” model (full results on the left, focus on the smaller models on the right). Experiments have been ran on a MacBook Air M2 with 16Gb of memory, and with a timeout of 2min. set of processes (clients…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages

  1. [1]

    Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction

    Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. Journal of the ACM , 64(4):1–49, 2017

    work page 2017

  2. [2]

    Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs

    Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland, Sarbojit Das, Bengt Jonsson, Magnus Lang, and Konstantinos Sagonas. Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs. In ´Etienne Andr´ e and Jun Sun, editors, Automated Technology for Verification and Analysis , pages 176–198. Springer Nature Switzerland, 2023

    work page 2023

  3. [3]

    Parsimonious Optimal Dynamic Partial Order Reduction

    Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, and Kon- stantinos Sagonas. Parsimonious Optimal Dynamic Partial Order Reduction

    work page

  4. [4]

    Optimal stateless model checking for reads-from equiva- lence under sequential consistency

    Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lang, Tuan Phong Ngo, and Konstantinos Sagonas. Optimal stateless model checking for reads-from equiva- lence under sequential consistency. Proceedings of the ACM on Programming Languages, 3(OOPSLA):1–29, 2019

    work page 2019

  5. [5]

    Stateless Model Checking Under a Reads-Value-From Equivalence

    Pratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis, and Viktor Toman. Stateless Model Checking Under a Reads-Value-From Equivalence. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification, volume 12759, pages 341–366. Springer International Publishing, 2021

    work page 2021

  6. [6]

    Optimal dynamic partial order reduction with context-sensitive indepen- dence and observers

    Elvira Albert, Maria Garcia de la Banda, Miguel G´ omez-Zamalloa, Miguel Isabel, and Peter Stuckey. Optimal dynamic partial order reduction with context-sensitive indepen- dence and observers. Journal of Systems and Software , 202:111730, 2023. 31

    work page 2023

  7. [7]

    Data-centric dynamic partial order reduction

    Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages, 2(POPL):1–30, 2018

    work page 2018

  8. [8]

    A Pragmatic Approach to Stateful Partial Order Reduction

    Berk Cirisci, Constantin Enea, Azadeh Farzan, and Suha Orhun Mutluergil. A Pragmatic Approach to Stateful Partial Order Reduction. In Cezara Dragoi, Michael Emmi, and Jingbo Wang, editors, Verification, Model Checking, and Abstract Interpretation, volume 13881, pages 129–154. Springer Nature Switzerland, 2023

    work page 2023

Show all 43 references
  1. [9]

    Quasi-optimal partial order reduction

    Camille Coti, Laure Petrucci, C´ esar Rodr ´ ıguez, and Marcelo Sousa. Quasi-optimal partial order reduction. Formal Methods in System Design , 57(1):3–33, 2021

    2021

  2. [10]

    De Boer, Marcello Bonsangue, Einar Broch Johnsen, Violet Ka I Pun, S

    Frank S. De Boer, Marcello Bonsangue, Einar Broch Johnsen, Violet Ka I Pun, S. Lizeth Tapia Tarifa, and Lars Tveito. SymPaths: Symbolic Execution Meets Partial Order Reduction. In Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner H¨ ahnle, and Mattias Ulbrich, editors,...

    2020

  3. [11]

    Commutativity in Automated Verification

    Azadeh Farzan. Commutativity in Automated Verification. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages 1–7. IEEE, 2023

    2023

  4. [12]

    Sound sequentialization for concurrent program verification

    Azadeh Farzan, Dominik Klumpp, and Andreas Podelski. Sound sequentialization for concurrent program verification. In Proceedings of the 43rd ACM SIGPLAN Interna- tional Conference on Programming Language Design and Implementation , pages 506–

  5. [13]

    Stratified Commutativity in Verification Algorithms for Concurrent Programs

    Azadeh Farzan, Dominik Klumpp, and Andreas Podelski. Stratified Commutativity in Verification Algorithms for Concurrent Programs. Proceedings of the ACM on Program- ming Languages, 7(POPL):1426–1453, 2023

    2023

  6. [14]

    Dynamic Partial-Order Reduction for Model Checking Software

    Cormac Flanagan and Patrice Godefroid. Dynamic Partial-Order Reduction for Model Checking Software. In POPL’05, 2005

    2005

  7. [15]

    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 . PhD thesis

  8. [16]

    Using partial orders to improve automatic verification methods

    Patrice Godefroid. Using partial orders to improve automatic verification methods. In Edmund M. Clarke and Robert P. Kurshan, editors, Computer-Aided Verification, pages 176–185. Springer, 1991

    1991

  9. [17]

    Govind, Fr´ ed´ eric Herbreteau, Srivathsan, and Igor Walukiewicz

    R. Govind, Fr´ ed´ eric Herbreteau, Srivathsan, and Igor Walukiewicz. Abstractions for the local-time semantics of timed automata: A foundation for partial-order methods. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science , pages 1–14. ACM, 2022

    2022

  10. [18]

    Thread modularity at many levels: A pearl in compositional verification

    Jochen Hoenicke, Rupak Majumdar, and Andreas Podelski. Thread modularity at many levels: A pearl in compositional verification. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages , pages 473–485. ACM, 2017

    2017

  11. [19]

    Jensen, Anders Moller, Veselin Raychev, Dimitar Dimitrov, and Martin Vechev

    Casper S. Jensen, Anders Moller, Veselin Raychev, Dimitar Dimitrov, and Martin Vechev. Stateless model checking of event-driven applications. In Proceedings of the 2015 32 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications...

    2015

  12. [20]

    Awaiting for Godot Stateless Model Checking that Avoids Executions where Nothing Happens

    Bengt Jonsson, Magnus Lang, and Konstantinos Sagonas. Awaiting for Godot Stateless Model Checking that Avoids Executions where Nothing Happens. In {22nd Formal Methods in Computer-Aided Design, {FMCAD} 2022. IEEE, 2022

    2022

  13. [21]

    Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique

    Vineet Kahlon, Chao Wang, and Aarti Gupta. Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, volume 5643, pages 398–413. Springer Berlin Heidelberg, 2009

    2009

  14. [22]

    Verification of distributed programs using representative interleaving sequences

    Shmuel Katz and Doron Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6(2):107–120, 1992

    1992

  15. [23]

    Enhancing GenMC’s Usability and Performance

    Michalis Kokologiannakis, Rupak Majumdar, and Viktor Vafeiadis. Enhancing GenMC’s Usability and Performance. In Bernd Finkbeiner and Laura Kov´ acs, editors, Tools and Algorithms for the Construction and Analysis of Systems , pages 66–84. Springer Nature Switzerland, 2024

    2024

  16. [24]

    Truly stateless, optimal dynamic partial order reduction

    Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. Truly stateless, optimal dynamic partial order reduction. Proceedings of the ACM on Programming Languages, 6(POPL):1–28, 2022

    2022

  17. [25]

    Unblocking Dynamic Partial Order Reduction

    Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis. Unblocking Dynamic Partial Order Reduction. In Constantin Enea and Akash Lal, editors, Computer Aided Verification, volume 13964, pages 230–250. Springer Nature Switzerland, 2023

    2023

  18. [26]

    Model checking for weakly consistent libraries

    Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. Model checking for weakly consistent libraries. In Kathryn S. McKinley and Kathleen Fisher, editors, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implemen- tation, PLDI 2019, Phoe...

    2019

  19. [27]

    BAM: Efficient Model Checking for Barriers

    Michalis Kokologiannakis and Viktor Vafeiadis. BAM: Efficient Model Checking for Barriers. In Karima Echihabi and Roland Meyer, editors, Networked Systems , volume 12754, pages 223–239. Springer International Publishing, 2021

    2021

  20. [28]

    Partial Order Reduction for Event-Driven Multi-threaded Programs

    Pallavi Maiya, Rahul Gupta, Aditya Kanade, and Rupak Majumdar. Partial Order Reduction for Event-Driven Multi-threaded Programs. In Marsha Chechik and Jean- Fran¸ cois Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 680–697. Springer, 2016

    2016

  21. [29]

    Mazurkiewicz

    Antoni W. Mazurkiewicz. Introduction to trace theory. In Volker Diekert and Grzegorz Rozenberg, editors, The Book of Traces, pages 3–41. World Scientific, 1995

    1995

  22. [30]

    Trace aware random testing for distributed systems

    Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Simin Oraee. Trace aware random testing for distributed systems. Proceedings of the ACM on Programming Languages , 3(OOPSLA):1–29, 2019. 33

    2019

  23. [31]

    Partial-order reduction

    Doron Peled. Partial-order reduction. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking , pages 173–

  24. [32]

    Peterson

    Gary L. Peterson. Myths about the mutual exclusion problem. 12(3):115–116, 1981

    1981

  25. [33]

    Efficient State-Space Exploration for Asynchronous Distributed Pro- grams: Adapting Unfolding-Based Dynamic Partial Order Reduction to MPI Programs

    The Anh Pham. Efficient State-Space Exploration for Asynchronous Distributed Pro- grams: Adapting Unfolding-Based Dynamic Partial Order Reduction to MPI Programs . These de doctorat, Rennes, Ecole normale superieure, 2019

    2019

  26. [34]

    Unfolding-based Partial Order Reduction

    C´ esar Rodr ´ ıguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Unfolding-based Partial Order Reduction. LIPIcs, Volume 42, CONCUR 2015 , 42:456–469, 2015

    2015

  27. [35]

    Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha

    Samira Tasharofi, Rajesh K. Karmani, Steven Lauterburg, Axel Legay, Darko Marinov, and Gul Agha. TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs. In Holger Giese and Grigore Rosu, editors, Formal Techniques for Distributed Systems , page...

    2012

  28. [36]

    A State Space Tool for Concurrent System Models Expressed In C++

    Antti Valmari. A State Space Tool for Concurrent System Models Expressed In C++

  29. [37]

    Stubborn sets for reduced state space generation

    Antti Valmari. Stubborn sets for reduced state space generation. In G. Goos, J. Hart- manis, D. Barstow, W. Brauer, P. Brinch Hansen, D. Gries, D. Luckham, C. Moler, A. Pnueli, G. Seegm¨ uller, J. Stoer, N. Wirth, and Grzegorz Rozenberg, editors,Advances in Petri Nets 1990 , v...

    1990

  30. [38]

    The state explosion problem

    Antti Valmari. The state explosion problem. In Gerhard Goos, Juris Hartmanis, Jan Leeuwen, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Petri Nets I: Basic Models, volume 1491, pages 429–528. Springer Berlin Heidelberg, 1998

    1998

  31. [39]

    Stop It, and Be Stubborn! ACM Transactions on Embedded Computing Systems, 16(2):1–26, 2017

    Antti Valmari. Stop It, and Be Stubborn! ACM Transactions on Embedded Computing Systems, 16(2):1–26, 2017

    2017

  32. [40]

    Stubborn Set Intuition Explained

    Antti Valmari and Henri Hansen. Stubborn Set Intuition Explained. In Maciej Koutny, Jetty Kleijn, and Wojciech Penczek, editors, Transactions on Petri Nets and Other Mod- els of Concurrency XII , volume 10470, pages 140–165. Springer Berlin Heidelberg, 2017

    2017

  33. [41]

    Verifying multi-threaded software with impact

    Bjorn Wachter, Daniel Kroening, and Joel Ouaknine. Verifying multi-threaded software with impact. In 2013 Formal Methods in Computer-Aided Design , pages 210–217. IEEE, 2013

    2013

  34. [42]

    Peephole Partial Order Reduction

    Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. Peephole Partial Order Reduction. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems , volume 4963, pages 382–396. Springer Berlin Heidelberg, 2008

    2008

  35. [43]

    Yu Yang, Xiaofang Chen, Ganesh Gopalakrishnan, and Robert M. Kirby. Efficient State- ful Dynamic Partial Order Reduction. In Klaus Havelund, Rupak Majumdar, and Jens Palsberg, editors, Model Checking Software, pages 288–305. Springer, 2008. 34

    2008

Pith tools

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