基于HOL4的形式化方法

摘要：

针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.

关键词：定理证明、形式化方法、高阶逻辑、乘法器、HOL4、形式化建模

所属期刊栏目：25

分类号：TP3;TP2

资助基金：国家自然科学基金61373034

在线出版日期：2016-08-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：202-207