Get the latest tech news
GenMC: Model checking for concurrent C programs
A model checker for weak memory models Summary GenMC is an open-source state-of-the-art model checker for verifying concurrent C/C++ programs under the RC11, IMM, and LKMM memory models. GenMC is based on a stateless model checking algorithm that is parametric in the choice of memory model.
In ASPLOS 2020 (March 2020)[Paper (15 pages)][@ACM][Artifact @Zenodo] BAM: Efficient model checking for barriers. In FMCAD 2021 (October 2021)[Paper (10 pages)] Truly stateless, optimal dynamic partial order reduction. In CAV 2023 (July 2023)[Paper (19 pages)][Technical appendix][Artifact @Zenodo] SPORE: Combining Symmetry and Partial Order Reduction.
Or read this on Hacker News
