|
|||||
|
|
| 基于逻辑的形式化验证方法: 进展及应用 | |
| 引用本文： | 陈钢,于林宇,裘宗燕,王颖.基于逻辑的形式化验证方法: 进展及应用[J].北京大学学报(自然科学版),2016,52(2):363-373. |
| 作者姓名： | 陈钢 于林宇 裘宗燕 王颖 |
| 作者单位： | 1. 北京京航计算通讯研究所, 北京 100074 2. 哈尔滨工业大学航天学院, 哈尔滨 150001 3. 北京大学数学学院信息科学系, 北京 100871 |
| 摘 要： | 近年来, 形式化方法发展很快, 一些技术已经产生工业应用。以逻辑系统为主线, 分析几个影响力比较大的形式化验证技术和验证工具, 以帮助应用工程师选择并使用形式化工具。主要包括命题演算和时态逻辑方面的SAT、BDD、模型检测和SMT, 谓词逻辑方面的ACL2、VDM方法和B方法, 以及高阶逻辑方面的HOL、PVS 和COQ。还介绍形式化方法在学术界和工业界的应用情况, 最后给出几个商业化的形式化验证工具。 |
| 关 键 词： | 形式化方法 逻辑系统 验证技术 |
| 收稿时间： | 2014-06-20 |
Logic Based Formal Verification Methods: Progress and Applications |
|
| CHEN Gang,YU Linyu,QIU Zongyan,WANG Ying.Logic Based Formal Verification Methods: Progress and Applications[J].Acta Scientiarum Naturalium Universitatis Pekinensis,2016,52(2):363-373. | |
| Authors: | CHEN Gang YU Linyu QIU Zongyan WANG Ying |
| Institution: | 1. Beijing Jinghang Research Institute of Computing and Communication, Beijing 100074 2. School of Astronautics, Harbin Institute of Technology, Harbin 150001 3. Department of Information Science, School of Mathematical Science, Peking University, Beijing 100871 |
| Abstract: | |
| Keywords: | formal methods logic systems verification techniques |
| 本文献已被 CNKI 万方数据 等数据库收录！ | |
| 点击此处可从《北京大学学报(自然科学版)》浏览原始摘要信息 | |
| 点击此处可从《北京大学学报(自然科学版)》下载免费的PDF全文 | |