带索引谓词的谓词抽象
摘要：谓词抽象为使用决策程序和最初用于有限状态模型检查的符号方法相结合，提供了一种验证无穷状态系统属性的强大工具。我们考虑包含一阶状态变量的模型，其中系统状态包括可变函数和谓词。这样的模型可以描述包含任意大的内存、缓冲区和相同进程数组的系统。我们描述了一种谓词抽象形式，构建一个关于一组全称量化变量的公式来描述一阶状态变量的不变性属性。我们提供了我们方法可靠性的形式证明，并描述了它如何用于验证几个硬件和软件设计，包括基于目录的缓存一致性协议。
作者：Shuvendu K. Lahiri, Randal E. Bryant
论文ID：cs/0407006
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23