2026-07-20T05:27:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23976 2025-11-12T13:25:12Z ddc:004 open_access

Optimal Concolic Dynamic Partial Order Reduction Khoshechin Jorshari, Mohammad Hossein Kokologiannakis, Michalis Majumdar, Rupak Nagendra, Srinidhi Stateless model checking dynamic symbolic execution Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs. We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mohammad Hossein Khoshechin Jorshari and Michalis Kokologiannakis and Rupak Majumdar and Srinidhi Nagendra 2025 Is Part Of LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2025.26 urn:nbn:de:0030-drops-239765 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26 eng https://creativecommons.org/licenses/by/4.0/legalcode