基于动态内存和状态管理的模型检测新方法

模型检测是并发系统验证的主要形式化方法之一，但其存在因状态空间爆炸而导致内存不够的问题，这也是大规模并发系统验证的瓶颈。很多研究人员尽管做了很多相关研究，但仍然没有很好地解决这个问题。在研究动态内存和状态管理的基础上，提出了一种新的模型检测方法，避免了因为内存不足而无法模型检则的问题。