State Space Estimation for DPOR-Based Model Checkers
summary
Proves counting Mazurkiewicz classes is #P-hard and inapproximable, then builds a polynomial‑time Monte Carlo estimator by turning an optimal stateless DPOR (TruSt) search tree into a Knuth-style sampler and reducing variance with stochastic enumeration. Implements the estimators in the JMC model checker and evaluates on shared‑memory benchmarks: the DAG method fails, the tree estimator stabilizes typically within a 20% band after a few hundred trials for spaces of 10^5–10^6 traces and gives 66% of benchmarks within 80–120% in one minute.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 2:59Mazurkiewicz classes hardness
- 4:46Unbiased estimators for DPOR
- 9:25Mazurkiewicz classes tree
- 13:18Evaluating estimators
- 16:39Question and answer session
related talks
20mTruly Stateless, Optimal Dynamic Partial Order Reduction
10mNerv: Probabilistic Dynamic Partial Order Reduction for Hardware
55mJava PathFinder: going to Mars without bugs and deadlocks
23mRandomized Testing of Distributed Systems with Probabilistic Guarantees
42mSurprise yourself with Property Based Testing
34mSymbolic Execution for Randomized Programs
16mSoftware Model Checking via Summary-Guided Search
22mCompositional Programming and Testing of Dynamic Distributed Systems