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

• 作者: 于林宇 王颖 裘宗燕 陈钢
• 来源期刊: 北京大学学报（自然科学版）
• 学科: 工学
• 关键词: 形式化方法 逻辑系统 验证技术
• 年，卷（期）: 2016,（2）
• 所属期刊栏目: 述评
• 页码范围: 363-373
• 页数: 11页
• 分类号: TP301
• 字数: 12107字
• 语种: 中文
• DOI: 10.13209/j.0479-8023.2015.131

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	于林宇		6	37	3.0	6.0
3	裘宗燕	北京大学数学学院信息科学系	15	93	5.0	9.0
4	陈钢		3	12	1.0	3.0
7	王颖		2	27	2.0	2.0