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

作者：陈波

来源：科技视界, 2018, (28): 162-163.

DOI：10.19694/j.cnki.issn2095-2457.2018.28.074

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

形式化方法在硬件、软件的设计和验证中的应用越来越广泛,基于不同理论的形式化验证工具应运而生。本文对形式化验证工具定理证明系统HOL作了介绍,并结合例子说明HOL系统在硬件设计中的应用。

• 单位
  山东理工大学