Value-centric dynamic partial order reduction Chatterjee, Krishnendu ; https://orcid.org/0000-0002-4561-241X Pavlogiannis, Andreas ; https://orcid.org/0000-0002-8943-0722 Toman, Viktor ; https://orcid.org/0000-0001-9036-063X safety risk reliability and quality software ddc:000 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. ACM 2019 info:eu-repo/semantics/conferenceObject doc-type:conferenceObject text http://purl.org/coar/resource_type/c_5794 https://research-explorer.ista.ac.at/record/10190 https://research-explorer.ista.ac.at/download/10190/10278 Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>. Vol 3. ACM; 2019. doi:<a href="https://doi.org/10.1145/3360550">10.1145/3360550</a> eng info:eu-repo/semantics/altIdentifier/doi/10.1145/3360550 info:eu-repo/semantics/altIdentifier/e-issn/2475-1421 info:eu-repo/semantics/altIdentifier/arxiv/1909.00989 info:eu-repo/semantics/openAccess