基于一阶符号轨迹计算理论的模型检测

项目名称： 基于一阶符号轨迹计算理论的模型检测

项目编号： No.61170073

项目类型： 面上项目

立项/批准年度： 2012

项目学科： 自动化技术、计算机技术

项目作者： 李勇坚

作者单位： 中国科学院软件研究所

项目金额： 56万元

中文摘要： 符号轨迹计算方法是目前工业界应用最为成功的形式化验证方法之一，在Intel芯片设计的形式化验证中取得了巨大的成功。但到目前为止，STE仅局限于基于布尔类型的硬件电路系统的验证，还不能用于基于字(word)或者整数等一阶数据类型的高层硬件或者软件系统设计的验证。本项目申请将在经典STE研究的基础上，吸取其结合X值抽象与符号模拟的基本思想，对其进行扩展，建立起一阶STE的形式语义理论。主要内容包括：(1)一阶STE语义模型的研究；(2)一阶STE模型检测算法的研究以及实现；(3)基于一阶STE的抽象方法的研究；(4)一阶 STE方法与定理证明技术的结合；(5)一阶STE工具的实现与集成以及在实际软硬件系统验证中的应用。其成果可望对STE理论本身产生积极的影响，拓宽STE技术的研究范围,推动STE技术在高层硬件与软件系统的形式验证方面的应用。

中文关键词： 一阶轨迹符号计算；模型检测；定理证明；归纳不变式；形式化方法

英文摘要：

英文关键词： first-order STE；model-checking；theorem proving；indutive invariants；formal methods