对并发程序进行推理的一个直接方法是将其行为定义为单个线程的原子行动的所有可能的交织集合。 然而，事实证明，用交错法进行推理对人类和计算机来说都太困难了，因为可能的交织法的数量增长很快。

并发的非交织模型，如 pomset 语言和事件结构，试图通过为程序行为集提出更紧凑的表示来解决这个问题。 近年来，对非交织并发模型重新产生了兴趣，例如，在宽松的内存模型、并发程序的模型检查和基于模型的突变测试方面。

这个项目的目标是在 Coq Proof Assistant 中开发一个非交织并发模型的机械化理论。 该图书馆应有助于感兴趣的研究人员正式证明这些模型的属性，并开发新的理论应用。

项目代码库