基于逻辑的形式化验证方法:进展及应用

摘要：

近年来,形式化方法发展很快,一些技术已经产生工业应用.以逻辑系统为主线,分析几个影响力比较大的形式化验证技术和验证工具,以帮助应用工程师选择并使用形式化工具.主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT,谓词逻辑方面的ACL2、VDM方法和B方法,以及高阶逻辑方面的HOL、PVS和COQ.还介绍形式化方法在学术界和工业界的应用情况,最后给出几个商业化的形式化验证工具.

关键词：形式化方法、逻辑系统、验证技术

所属期刊栏目：52

分类号：TP301(计算技术、计算机技术)

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

页数：共11页

页码：363-373