Model Checking C/C++ with Mixed-Size Accesses

Explore a 21-minute conference talk from POPL 2025 that introduces Mixer, an optimal dynamic partial order reduction (DPOR) algorithm for verifying concurrent C/C++ programs with mixed-size accesses. Learn how researchers Iason Marmanis, Michalis Kokologiannakis, and Viktor Vafeiadis from MPI-SWS and ETH Zurich address the challenge of model checking programs where atomic instructions access different bytes of the same word—a common pattern in code using C/C++ union types. The presentation demonstrates how Mixer enables automatic verification of such programs by allowing multi-byte reads to be revisited by multiple writes together, extending verification capabilities to transactional programs under certain conditions. The talk includes functional artifacts that have been evaluated and are available for reference through Zenodo, with the full research article accessible via ACM Digital Library.