GenMC：并发C程序模型检查器

GenMC是一款开源的C/C++并发程序模型检查器，支持RC11、IMM和LKMM内存模型。它基于一种无状态的模型检查算法，该算法在内存模型的选择上具有参数化特性。在满足关于内存模型的几个基本条件下，该算法具有健全性、完备性和最优性，因为它可以精确地探索程序根据模型的每个一致执行，并且不会探索不一致的执行或进行无效的探索路径。GenMC包含许多优化，例如锁感知和屏障感知的偏序约简、对称约简和自动自旋循环限制。