高阶逻辑验证系统HOL及其应用初探  

The Higher Order Logic System HOL and Its Applications

作　　者：陈波[1] CHEN Bo(College of Computer Science and Technology,Shandong University of Technology,Zibo Shandong 255049,China)

机构地区：[1]山东理工大学计算机科学与技术学院,山东淄博255049

出　　处：《科技视界》2018年第28期162-163,共2页Science & Technology Vision

摘　　要：形式化方法在硬件、软件的设计和验证中的应用越来越广泛,基于不同理论的形式化验证工具应运而生。本文对形式化验证工具定理证明系统HOL作了介绍,并结合例子说明HOL系统在硬件设计中的应用。Formal method has been used in both practical hardware and software design and verification widely, Formal verification tools based on different theory emerge as the times require.The paper discusses the higher order logic theory prover HOL and illustrates specification and verification in hardware design.

关 键 词：形式化验证方法 HOL逻辑 HOL系统 带复位的奇偶校验器 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论] TP309[自动化与计算机技术—计算机科学与技术]