@inproceedings{10190,
  abstract     = {The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning.},
  author       = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Toman, Viktor},
  booktitle    = {Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications},
  issn         = {2475-1421},
  keywords     = {safety, risk, reliability and quality, software},
  location     = {Athens, Greece},
  publisher    = {ACM},
  title        = {{Value-centric dynamic partial order reduction}},
  doi          = {10.1145/3360550},
  volume       = {3},
  year         = {2019},
}