正确编写并发算法很困难。 普通的测试技术在并发程序中帮助不大，因为这些程序的行为是非决定性的，而且一些错误只能在特定的环境中表现出来（例如，在特定硬件的松弛型内存模型中）。

模型检查是一种形式化的验证技术，它通过在受控环境中系统地探索程序的各种执行痕迹来帮助发现并发程序中的错误。

在这个项目中，我们正在开发新的技术来解决这个问题，试图改进现有的并发程序的模型检查工具，并在现实世界的软件项目中对它们进行实地测试。