pith. sign in

arxiv: 2512.23996 · v3 · submitted 2025-12-30 · 💻 cs.PL

State Space Estimation for DPOR-based Model Checkers(Extended Version)

A. R. Balasubramanian , Mohammad Hossein Khoshechin Jorshari , Rupak Majumdar , Umang Mathur , Minjian Zhang This is my paper

Pith reviewed 2026-05-16 19:37 UTC · model grok-4.3

classification 💻 cs.PL
keywords concurrent programsmodel checkingDPORMazurkiewicz tracesMonte Carlo estimationstate space estimationunbiased estimator
0
0 comments X

The pith

DPOR explorations yield unbiased poly-time estimates for the number of Mazurkiewicz traces in concurrent programs.

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

The paper tackles the problem of estimating how many distinct Mazurkiewicz trace classes a bounded concurrent program produces under interleaving. Exact counting is #P-hard and cannot be approximated efficiently, so the authors instead convert the exploration tree built by any stateless optimal DPOR algorithm into an unbiased Monte Carlo estimator. They apply Knuth's classical tree estimator to this structure and add stochastic enumeration to keep variance low. The result is the first provably unbiased polynomial-time method for this quantity, which directly informs how long a model-checking run will take and what fraction of the space has been covered so far. Experiments on shared-memory benchmarks show that a few hundred trials produce stable estimates even when the true number of traces reaches 10^5 to 10^6.

Core claim

By treating the search performed by a stateless optimal DPOR algorithm as a bounded-depth, bounded-width tree whose leaves are exactly the maximal Mazurkiewicz traces, Knuth's estimator produces an unbiased count of those traces in polynomial time; stochastic enumeration of a small population of partial paths at each depth controls variance without introducing bias.

What carries the argument

Knuth's tree estimator applied to the DPOR exploration tree, with stochastic enumeration maintaining coupled populations of partial paths at each depth to bound variance.

If this is right

  • Model checkers obtain a running estimate of total search-space size to decide when to stop or allocate more resources.
  • The fraction of the space already explored can be reported during a run as the ratio of completed traces to the current estimate.
  • The same weighted-graph version of the estimator gives an unbiased prediction of total model-checking cost.
  • Stable estimates within roughly 20 percent are obtained with only a few hundred trials on spaces containing up to a million traces.

Where Pith is reading between the lines

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

  • The technique could be lifted to other partial-order reduction schemes whose search trees have similar bounded-width structure.
  • Dynamic resource allocation in verification tools becomes feasible once running estimates of remaining work are available.
  • Hybrid algorithms that combine the estimator with directed or priority-based search could focus effort on high-variance regions of the trace space.

Load-bearing premise

The DPOR exploration must form a bounded-depth bounded-width tree whose leaves correspond exactly to the maximal Mazurkiewicz traces.

What would settle it

Run the estimator on a small program whose exact number of maximal Mazurkiewicz traces is already known by exhaustive enumeration and check whether repeated independent runs converge to that exact number.

Figures

Figures reproduced from arXiv: 2512.23996 by A. R. Balasubramanian, Minjian Zhang, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur.

Figure 1
Figure 1. Figure 1: The transition system T (r+w+w) To show that Algorithm K runs in poly-time, it suffices to show that the number of children of a node can be computed in poly-time. This is easy, since the number of children of each execution graph is exactly the number of available threads at an execution graph. Hence, Algorithm K is easy to implement in a random tester: it only requires that we intercept the scheduling ev… view at source ↗
Figure 2
Figure 2. Figure 2: shows the DAG T (r+rr) of the program. Although T (r+rr) has exactly one sink, there are three paths to reach the sink, and running Algorithm P on each path returns a different estimation. 𝐺0 𝐺1 𝐺2 𝐺3 𝐺4 init R(𝑦) R(𝑥) R(𝑥) [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The transition system D (r+w+w) While we have described an estimator for sequentially consistent executions, the Trust algorithm works as long as the memory model satisfies a set of requirements and in every such case, we get a poly-time unbiased estimator. We focus on sequential consistency for readability. Also, while there are different algorithms for optimal DPOR, some algorithms maintain additional hi… view at source ↗
Figure 4
Figure 4. Figure 4: The transition system D (r+nw) A simple heuristic to get better estimates is to always schedule writes first. This strategy does reduce the variance for this example. However, consider a small variation in which the second thread starts with a read of a different location: we are back to an exponential variance. 4.3 Stochastic Enumeration In order to reduce the variance, we use stochastic enumeration [45, … view at source ↗
Figure 5
Figure 5. Figure 5: Convergence vs. workload/maximal exe￾cutions. 1 6 11 16 21 26 31 36 41 46 Testor budget B 10 3 10 4 10 5 Trials to convergence (median, 25 75% interval) [PITH_FULL_IMAGE:figures/full_fig_p017_5.png] view at source ↗
read the original abstract

We study the estimation problem for concurrent programs: given a bounded program $P$, estimate the number of Mazurkiewicz trace-equivalence classes induced by its interleavings. This quantity informs two practical questions for enumeration-based model checking: how long a model checking run is likely to take, and what fraction of the search space has been covered so far. We first show the counting problem is #P-hard even for restricted programs and, unless $P=NP$, inapproximable within any subexponential factor, ruling out efficient exact or randomized approximation algorithms. We give a Monte Carlo approach to obtain a poly-time unbiased estimator: we convert a stateless optimal DPOR algorithm into an unbiased estimator by viewing its exploration as a bounded-depth, bounded-width tree whose leaves are the maximal Mazurkiewicz traces. A classical estimator by Knuth, when run on this tree, yields an unbiased estimate. To control the variance, we apply stochastic enumeration by maintaining a small population of partial paths per depth whose evolution is coupled. We have implemented our estimator in the JMC model checker and evaluated it on shared-memory benchmarks. With modest budgets, our estimator yields stable estimates, typically within a 20% band, within a few hundred trials, even when the state space has $10^5$--$10^6$ classes. We also show how the same machinery estimates model-checking cost by weighting all explored graphs, not only complete traces. Our algorithms provide the first provable poly-time unbiased estimators for counting traces, a problem of considerable importance when allocating model checking resources.

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

2 major / 3 minor

Summary. The paper studies estimation of the number of Mazurkiewicz trace-equivalence classes for bounded concurrent programs. It proves #P-hardness and inapproximability (unless P=NP) for exact counting or subexponential approximation. The core contribution is a Monte Carlo unbiased estimator obtained by recasting a stateless optimal DPOR run as a bounded-depth, bounded-width tree to which Knuth's classical estimator is applied; variance is controlled via stochastic enumeration that maintains coupled populations of partial paths. The method is implemented in JMC and evaluated on shared-memory benchmarks, yielding stable estimates (typically within a 20% band) for state spaces with 10^5--10^6 classes after a few hundred trials. The same framework is also used to estimate model-checking cost.

Significance. If the unbiasedness claim holds, the work supplies the first provable poly-time unbiased estimator for trace counts, a quantity directly useful for deciding resource allocation and coverage in enumeration-based model checkers. The hardness results supply useful context, and the experimental results indicate that modest budgets suffice for practical accuracy on realistic benchmarks. The approach is noteworthy for reusing an existing optimal DPOR algorithm without introducing fitted parameters.

major comments (2)
  1. [§4] §4 (Monte Carlo construction): The central claim that a stateless optimal DPOR exploration forms a bounded-width tree whose nodes have fixed children (allowing direct application of Knuth's estimator) is load-bearing. Sleep sets are updated in a history-dependent manner, so the legal branching factor at depth d is path-dependent rather than a static property of the node. The paper must explicitly define the probability space that folds sleep-set updates into the choice probabilities at every step; otherwise the estimator is biased because paths are not sampled with probability exactly inverse to the product of the (fixed) branching factors.
  2. [§5] §5 (stochastic enumeration): The variance-control claims rest on maintaining a small population of partial paths per depth whose evolution is coupled. No formal variance bound or proof that the coupling preserves unbiasedness is supplied; the experimental observation of estimates within a 20% band after a few hundred trials therefore lacks theoretical support and could be an artifact of the chosen benchmarks.
minor comments (3)
  1. [Abstract] Abstract and §6 (evaluation): The statement 'typically within a 20% band' should be accompanied by per-benchmark tables or plots showing mean, standard deviation, and number of trials rather than a qualitative summary.
  2. [§3] §3 (hardness): The restricted class of programs for which #P-hardness holds should be illustrated with a small concrete example to make the reduction easier to follow.
  3. [Notation] Notation throughout: Ensure that 'maximal Mazurkiewicz traces' and 'trace-equivalence classes' are used consistently; the current text occasionally switches between the two without explicit equivalence.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address the two major comments point by point below, clarifying the underlying probability space and the properties of the stochastic enumeration procedure. We plan to incorporate the suggested clarifications into the revised version.

read point-by-point responses

  1. Referee: [§4] §4 (Monte Carlo construction): The central claim that a stateless optimal DPOR exploration forms a bounded-width tree whose nodes have fixed children (allowing direct application of Knuth's estimator) is load-bearing. Sleep sets are updated in a history-dependent manner, so the legal branching factor at depth d is path-dependent rather than a static property of the node. The paper must explicitly define the probability space that folds sleep-set updates into the choice probabilities at every step; otherwise the estimator is biased because paths are not sampled with probability exactly inverse to the product of the (fixed) branching factors.

    Authors: We agree that an explicit definition of the probability space is necessary and will add it to §4. In the construction, each node of the exploration tree is a pair (trace prefix, sleep set). The children of such a node are exactly the enabled transitions not belonging to the current sleep set; we sample uniformly at random among these children. The branching factor used both for sampling and for the Knuth estimator is therefore the concrete number of legal children at that node, which incorporates the history-dependent sleep-set update. Because the sampling probability of any complete path is precisely the reciprocal of the product of the (path-specific) branching factors along it, and the estimator for that path is exactly the same product, the expectation remains equal to the total number of leaves. The estimator is therefore unbiased even though branching factors vary across nodes. We will revise the text to state this probability space formally, including the inductive definition of sleep-set updates at each step. revision: yes

  2. Referee: [§5] §5 (stochastic enumeration): The variance-control claims rest on maintaining a small population of partial paths per depth whose evolution is coupled. No formal variance bound or proof that the coupling preserves unbiasedness is supplied; the experimental observation of estimates within a 20% band after a few hundred trials therefore lacks theoretical support and could be an artifact of the chosen benchmarks.

    Authors: We acknowledge that §5 currently lacks both a formal variance bound and an explicit argument that the coupling step preserves unbiasedness. Each path in the maintained population is generated by the identical sampling procedure defined in §4; consequently the marginal distribution of any single path remains unchanged and the overall estimator (the average over the population) stays unbiased. The coupling is used only to share prefix computations and thereby reduce variance; it does not alter the sampling probabilities. We will add a short proof sketch in the revised §5 establishing that unbiasedness is preserved. While we do not supply a general closed-form variance bound (which would necessarily depend on program-specific structure), we will also expand the experimental discussion to include additional benchmarks and to note the empirical character of the observed stability. We believe these additions address the referee's concern without overclaiming theoretical guarantees. revision: partial

Circularity Check

0 steps flagged

No circularity: classical Knuth estimator applied to DPOR tree model

full rationale

The paper's central construction converts a stateless optimal DPOR run into an estimator by modeling its exploration as a bounded-depth bounded-width tree whose leaves are maximal Mazurkiewicz traces, then directly invokes the classical Knuth estimator on that tree. No equations define the target count in terms of the estimator itself, no parameters are fitted to a subset and then relabeled as a prediction, and no load-bearing uniqueness theorem or ansatz is imported via self-citation. The unbiasedness claim rests on the external Knuth method once the tree model is granted; the tree model is presented as a property of existing DPOR algorithms rather than a self-referential definition. This is a standard application of a known Monte Carlo technique to a new domain and therefore exhibits no circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the domain assumption that DPOR exploration yields a tree whose leaves are maximal traces, plus the classical correctness of Knuth's estimator; no new free parameters or invented entities are introduced.

axioms (1)
  • domain assumption The exploration performed by a stateless optimal DPOR algorithm forms a bounded-depth, bounded-width tree whose leaves are the maximal Mazurkiewicz traces.
    This modeling step is required to apply Knuth's estimator directly to the DPOR search process.

pith-pipeline@v0.9.0 · 5606 in / 1271 out tokens · 53628 ms · 2026-05-16T19:37:23.778422+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

56 extracted references · 56 canonical work pages

  1. [1]

    Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. InProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems-Volume 9035 (TACAS’15). 353–367. doi:10.1007/978-3-662- 46681-0_28

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

  2. [2]

    Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal dynamic partial order reduction. InProceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). ACM, New York, NY, USA, 373–384. doi:10.1145/2535838.2535845

    work page doi:10.1145/2535838.2535845 2014

  3. [3]

    Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, and Konstantinos Sagonas. 2024. Parsimonious optimal dynamic partial order reduction. InInternational Conference on Computer Aided Verification (CA V’24). Springer, 19–43. doi:10.1007/978-3-031-65630-9_2

    work page doi:10.1007/978-3-031-65630-9_2 2024

  4. [4]

    Marcelo Arenas, Luis Alberto Croquevielle, Rajesh Jayaram, and Cristian Riveros. 2020. Efficient Logspace Classes for Enumeration, Counting, and Uniform Generation.SIGMOD Rec.49, 1 (Sept. 2020), 52–59. doi:10.1145/3422648.3422661

    work page doi:10.1145/3422648.3422661 2020

  5. [5]

    Cambridge University Press, 2009.doi:10.1017/CBO9780511804090

    Sanjeev Arora and Boaz Barak. 2009.Computational Complexity: A Modern Approach. Cambridge University Press. doi:10.1017/CBO9780511804090

    work page doi:10.1017/cbo9780511804090 2009

  6. [6]

    Thomas Ball and James R. Larus. 1996. Efficient path profiling. InProceedings of the 29th Annual ACM/IEEE International Symposium on Microarchitecture(Paris, France)(MICRO 29). IEEE Computer Society, USA, 46–57. doi:10.1109/MICRO. 1996.566449

    work page doi:10.1109/micro 1996

  7. [7]

    Rudolf Bayer and Mario Schkolnick. 1977. Concurrency of Operations on B-Trees.Acta Informatica9 (1977), 1–21. doi:10.1007/BF00263762

    work page doi:10.1007/bf00263762 1977

  8. [8]

    Dirk Beyer and M Erkan Keremoglu. 2011. CPAchecker: A tool for configurable software verification. InInternational conference on computer aided verification. Springer, 184–190. doi:10.1007/978-3-642-22110-1_16

    work page doi:10.1007/978-3-642-22110-1_16 2011

  9. [9]

    Marcel Böhme. 2018. STADS: Software Testing as Species Discovery.ACM Trans. Softw. Eng. Methodol.27, 2, Article 7 (June 2018), 52 pages. doi:10.1145/3210309

    work page doi:10.1145/3210309 2018

  10. [10]

    Marcel Böhme, Danushka Liyanage, and Valentin Wüstholz. 2021. Estimating residual risk in greybox fuzzing. InProceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering(Athens, Greece)(ESEC/FSE 2021). Association for Computing Machinery, New York, NY, USA, 230–241. doi:10.1...

    work page doi:10.1145/3468264.3468570 2021

  11. [11]

    Marcel Böhme, Valentin J. M. Manès, and Sang Kil Cha. 2023. Boosting Fuzzer Efficiency: An Information Theoretic Perspective.Commun. ACM66, 11 (Oct. 2023), 89–97. doi:10.1145/3611019

    work page doi:10.1145/3611019 2023

  12. [12]

    Arkady Bron, Eitan Farchi, Yonit Magid, Yarden Nir, and Shmuel Ur. 2005. Applications of synchronization coverage. InProceedings of the Tenth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming(Chicago, IL, USA)(PPoPP ’05). Association for Computing Machinery, New York, NY, USA. doi:10.1145/1065944.1065972

    work page doi:10.1145/1065944.1065972 2005

  13. [13]

    Supratik Chakraborty, Kuldeep S Meel, and Moshe Y Vardi. 2013. A Scalable Approximate Model Counter. In International Conference on Principles and Practice of Constraint Programming. Springer, 200–216. doi:10.1007/978-3- 642-40627-0_18

    work page doi:10.1007/978-3- 2013

  14. [14]

    JMC: Java Model Checker. 2025. https://jmc.mpi-sws.org/

    work page 2025

  15. [15]

    Hana Chockler, Orna Kupferman, and Moshe Y. Vardi. 2003. Coverage Metrics for Formal Verification. InCorrect Hardware Design and Verification Methods, Daniel Geist and Enrico Tronci (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 111–125. doi:10.1007/978-3-540-39724-3_11

    work page doi:10.1007/978-3-540-39724-3_11 2003

  16. [16]

    Maria Christakis, Alkis Gotovos, and Konstantinos Sagonas. 2013. Systematic testing for detecting concurrency errors in Erlang programs. In2013 IEEE Sixth International Conference on Software Testing, Verification and Validation. IEEE, 154–163. doi:10.1109/ICST.2013.50

    work page doi:10.1109/icst.2013.50 2013

  17. [17]

    Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, and Marek Trtik. 2018. JBMC: A bounded model checking tool for verifying Java bytecode. InInternational Conference on Computer Aided Verification (CA V’18). Springer. doi:10.1007/978-3-319-96145-3_10

    work page doi:10.1007/978-3-319-96145-3_10 2018

  18. [18]

    Ankush Desai, Vivek Gupta, Ethan Jackson, Shaz Qadeer, Sriram Rajamani, and Damien Zufferey. 2013. P: safe asynchronous event-driven programming. InProceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation(Seattle, Washington, USA)(PLDI ’13). Association for Computing Machinery, New York, NY, USA, 321–332. doi:10.114...

    work page doi:10.1145/2491956.2462184 2013

  19. [19]

    Mike Dodds, Andreas Haas, and Christoph M. Kirsch. 2015. A Scalable, Correct Time-Stamped Stack. In42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Mumbai, India)(POPL ’15). ACM, New York, NY, USA, 233–246. doi:10.1145/2676726.2676963

    work page doi:10.1145/2676726.2676963 2015

  20. [20]

    Kolaitis

    Arnaud Durand, Miki Hermann, and Phokion G. Kolaitis. 2005. Subtractive reductions and complete problems for counting complexity classes.Theoretical Computer Science340, 3 (2005), 496–513. doi:10.1016/j.tcs.2005.03.012 Mathematical Foundations of Computer Science 2000

    work page doi:10.1016/j.tcs.2005.03.012 2005

  21. [21]

    Constantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, and Rupak Majumdar. 2024. Model Checking Distributed Protocols in Must.Proc. ACM Program. Lang.8, OOPSLA2, Article 338 (Oct. 2024), 28 pages. doi:10.1145/ 3689778

    work page 2024

  22. [22]

    Cormac Flanagan and Patrice Godefroid. 2005. Dynamic partial-order reduction for model checking software. InPOPL

    work page 2005

  23. [23]

    doi:10.1145/1040305.1040315

    ACM, New York, NY, USA, 110–121. doi:10.1145/1040305.1040315

    work page doi:10.1145/1040305.1040315

  24. [24]

    Phillip B Gibbons and Ephraim Korach. 1997. Testing shared memories.SIAM J. Comput.26, 4 (1997), 1208–1244. doi:10.1137/S0097539794279614

    work page doi:10.1137/s0097539794279614 1997

  25. [25]

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

    Patrice Godefroid. 1996.Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State- Explosion Problem. Lecture Notes in Computer Science, Vol. 1032. Springer. doi:10.1007/3-540-60761-7

    work page doi:10.1007/3-540-60761-7 1996

  26. [26]

    Patrice Godefroid. 1997. Model checking for programming languages using VeriSoft. InPOPL 1997(Paris, France). ACM, New York, NY, USA, 174–186. doi:10.1145/263699.263717

    work page doi:10.1145/263699.263717 1997

  27. [27]

    Klaus Havelund and Thomas Pressburger. 2000. Model Checking JAVA Programs using JAVA PathFinder.Int. J. Soft. Tool. Tech. Transf.2, 4 (2000), 366–381. doi:10.1007/S100090050043

    work page doi:10.1007/s100090050043 2000

  28. [28]

    Danny Hendler, Nir Shavit, and Lena Yerushalmi. 2004. A Scalable Lock-Free Stack Algorithm. InSPAA 2004(Barcelona, Spain). ACM, New York, NY, USA. doi:10.1145/1007912.1007944

    work page doi:10.1145/1007912.1007944 2004

  29. [29]

    2020.The Art of Multiprocessor Programming(2nd ed.)

    Maurice Herlihy, Nir Shavit, Victor Luchangco, and Michael Spear. 2020.The Art of Multiprocessor Programming(2nd ed.). Morgan Kaufmann Publishers Inc. doi:10.1016/C2011-0-06993-4

    work page doi:10.1016/c2011-0-06993-4 2020

  30. [30]

    2004.The SPIN model checker: Primer and reference manual

    Gerard J Holzmann. 2004.The SPIN model checker: Primer and reference manual. Vol. 1003. Addison-Wesley Reading

    work page 2004

  31. [31]

    Huber and Sangtae Kim

    Gary A. Huber and Sangtae Kim. 1996. Weighted-Ensemble Brownian Dynamics Simulations for Protein Association Reactions.Biophysical Journal70 (1996), 97–110. doi:10.1016/S0006-3495(96)79552-8

    work page doi:10.1016/s0006-3495(96)79552-8 1996

  32. [32]

    Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra

    work page

  33. [33]

    In36th International Conference on Concurrency Theory (CONCUR 2025), Vol

    Optimal Concolic Dynamic Partial Order Reduction. In36th International Conference on Concurrency Theory (CONCUR 2025), Vol. 348. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 26:1–26:22. https: //drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26

    work page doi:10.4230/lipics.concur.2025.26 2025

  34. [34]

    Donald E. Knuth. 1975. Estimating the Efficiency of Backtrack Programs.Math. Comp.29, 129 (1975), 121–136. doi:10.2307/2005469

    work page doi:10.2307/2005469 1975

  35. [35]

    Michalis Kokologiannakis, Rupak Majumdar, and Viktor Vafeiadis. 2024. Enhancing GenMC’s Usability and Perfor- mance. InTools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer Nature Switzerland, Cham, 66–84. doi:10.1007/978-3-031-57249-4_4

    work page doi:10.1007/978-3-031-57249-4_4 2024

  36. [36]

    Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, and Viktor Vafeiadis. 2022. Truly stateless, optimal dynamic partial order reduction.Proc. ACM Program. Lang.6, POPL, Article 49 (Jan. 2022), 26 pages. doi:10.1145/3498711

    work page doi:10.1145/3498711 2022

  37. [37]

    Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis. 2023. Unblocking Dynamic Partial Order Reduction. InCA V 2023 (LNCS, Vol. 13964), Constantin Enea and Akash Lal (Eds.). Springer, 230–250. doi:10.1007/978-3-031-37706- 8_12

    work page doi:10.1007/978-3-031-37706- 2023

  38. [38]

    Daniel Kroening and Michael Tautschnig. 2014. CBMC–C Bounded Model Checker: (Competition Contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14). Springer. doi:10.1007/978-3-642-54862-8_26

    work page doi:10.1007/978-3-642-54862-8_26 2014

  39. [39]

    Stephan Lipp, Daniel Elsner, Severin Kacianka, Alexander Pretschner, Marcel Böhme, and Sebastian Banescu. 2023. Green Fuzzing: A Saturation-Based Stopping Criterion using Vulnerability Prediction. InProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis(Seattle, WA, USA)(ISSTA 2023). Association for Computing Machiner...

    work page doi:10.1145/3597926.3598043 2023

  40. [40]

    Danushka Liyanage, Seongmin Lee, Chakkrit Tantithamthavorn, and Marcel Böhme. 2024. Extrapolating Coverage Rate in Greybox Fuzzing. InProceedings of the IEEE/ACM 46th International Conference on Software Engineering (Lisbon, Portugal)(ICSE ’24). Association for Computing Machinery, New York, NY, USA, Article 132, 12 pages. doi:10.1145/3597503.3639198

    work page doi:10.1145/3597503.3639198 2024

  41. [41]

    Kuldeep S Meel, Sourav Chakraborty, and Umang Mathur. 2024. A faster FPRAS for#NFA.Proceedings of the ACM on Management of Data2, 2 (2024), 1–22. doi:10.1145/3651613

    work page doi:10.1145/3651613 2024

  42. [42]

    Kuldeep S Meel and Alexis de Colnet. 2025. Towards practical FPRAS for#NFA: Exploiting the Power of Dependence. Proceedings of the ACM on Management of Data3, 2 (2025), 1–23. doi:10.1145/3725253

    work page doi:10.1145/3725253 2025

  43. [43]

    Michael and Michael L

    Maged M. Michael and Michael L. Scott. 1998. Nonblocking algorithms and preemption-safe locking on multipro- grammed shared memory multiprocessors.J. Parallel and Distrib. Comput.51 (1998). doi:10.1006/jpdc.1998.1446 State Space Estimation for DPOR-based Model Checkers 23

    work page doi:10.1006/jpdc.1998.1446 1998

  44. [44]

    Brian Norris and Brian Demsky. 2016. A practical approach for model checking C/C++ 11 code.ACM Transactions on Programming Languages and Systems (TOPLAS)38 (2016). doi:10.1145/2806886

    work page doi:10.1145/2806886 2016

  45. [45]

    John Penix, Willem Visser, and Peter Norvig. 2001. Coverage Metrics for Model Checking. (2001). https://ntrs.nasa. gov/citations/20010106055

    work page arXiv 2001

  46. [46]

    Leonard Pitt. 1987. A note on extending Knuth’s tree estimator to directed acyclic graphs.Inform. Process. Lett.24, 3 (1987), 203–206. doi:10.1016/0020-0190(87)90187-6

    work page doi:10.1016/0020-0190(87)90187-6 1987

  47. [47]

    Reuven Rubinstein. 2013. Stochastic enumeration method for counting NP-hard problems.Methodology and Computing in Applied Probability15, 2 (2013), 249–291. doi:10.1007/s11009-011-9242-y

    work page doi:10.1007/s11009-011-9242-y 2013

  48. [48]

    Larry Rudolph and Zary Segall. 1984. Dynamic decentralized cache schemes for mimd parallel processors. InProceedings of the 11th Annual International Symposium on Computer Architecture (ISCA ’84). Association for Computing Machinery, New York, NY, USA, 340–347. doi:10.1145/800015.808203

    work page doi:10.1145/800015.808203 1984

  49. [49]

    Stockmeyer

    Larry J. Stockmeyer. 1985. On Approximation Algorithms for #P.SIAM J. Comput.14, 4 (1985), 849–861. doi:10.1137/ 0214060

    work page 1985

  50. [50]

    SV-COMP. 2019. Competition on Software Verification (SV-COMP). https://sv-comp.sosy-lab.org/2019/

    work page 2019

  51. [51]

    Ali Taleghani and Joanne M. Atlee. 2009. State-Space Coverage Estimation. In2009 IEEE/ACM International Conference on Automated Software Engineering. 459–467. doi:10.1109/ASE.2009.24

    work page doi:10.1109/ase.2009.24 2009

  52. [52]

    Kent Treiber

    R. Kent Treiber. 1986.Systems Programming: Coping with Parallelism. Technical Report. Technical Report RJ5118, IBM. https://dominoweb.draco.res.ibm.com/58319a2ed2b1078985257003004617ef.html

    work page 1986

  53. [53]

    Radislav Vaisman and Dirk P Kroese. 2017. Stochastic enumeration method for counting trees.Methodology and Computing in Applied Probability19, 1 (2017), 31–73. doi:10.1007/s11009-015-9457-4

    work page doi:10.1007/s11009-015-9457-4 2017

  54. [54]

    The Kani Rust Verifier. 2025. https://model-checking.github.io/kani/

    work page 2025

  55. [55]

    Afek Yehuda, Gafni Eli, and Morrison Adam. 2007. Common2 extended to stacks and unbounded concurrency. Distributed Comput.20 (2007). doi:10.1007/S00446-007-0023-3

    work page doi:10.1007/s00446-007-0023-3 2007

  56. [56]

    Naling Zhang, Markus Kusano, and Chao Wang. 2015. Dynamic partial order reduction for relaxed memory models. InProceedings of the 36th ACM SIGPLAN conference on programming language design and implementation (PLDI’15). 250–259. doi:10.1145/2737924.2737956 24 Balasubramanian et al. A Complexity of Counting In this section, we prove our theoretical hardness...

    work page doi:10.1145/2737924.2737956 2015