conference paper published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Andreas Pavlogiannis author 49704004-F248-11E8-B48F-1D18A9856A870000-0002-8943-0722 Viktor Toman author 3AF3DA7C-F248-11E8-B48F-1D18A9856A870000-0001-9036-063X GradSch department KrCh department OOPSLA: Object-oriented Programming, Systems, Languages and Applications Efficient Algorithms for Computer Aided Verification project Game Theory project Rigorous Systems Engineering project Moderne Concurrency Paradigms project 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. https://research-explorer.ista.ac.at/download/10190/10278/2019_ACM_Chatterjee.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ ACM2019Athens, Greece eng safetyriskreliability and qualitysoftware 2475-1421 1909.0098910.1145/3360550 3 https://research-explorer.ista.ac.at/record/10199 K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019. Chatterjee, K., Pavlogiannis, A., &#38; Toman, V. (2019). 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). Athens, Greece: ACM. <a href="https://doi.org/10.1145/3360550">https://doi.org/10.1145/3360550</a> Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “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. <a href="https://doi.org/10.1145/3360550">https://doi.org/10.1145/3360550</a>. K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Athens, Greece, 2019, vol. 3. Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, vol. 3, 124, ACM, 2019, doi:<a href="https://doi.org/10.1145/3360550">10.1145/3360550</a>. 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> Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124. 101902021-10-27T14:57:06Z2026-04-08T07:00:31Z