文献类型：期刊文章

作　　者：陈钢[1] 于林宇[1,2] 裘宗燕[3] 王颖[1]

机构地区：[1]北京京航计算通讯研究所,北京100074 [2]哈尔滨工业大学航天学院,哈尔滨150001 [3]北京大学数学学院信息科学系,北京100871

出　　处：《北京大学学报（自然科学版）》

年　　份：2016

卷　　号：52

期　　号：2

起止页码：363-373

语　　种：中文

收录情况：AJ、BDHX、BDHX2014、CAS、CSCD、CSCD2015_2016、EI、IC、INSPEC、JST、MR、PROQUEST、RCCSE、RSC、SCOPUS、WOS、ZGKJHX、ZMATH、ZR、核心刊

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

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

分 类 号：TP301]