公开(公告)号：CN106294148A

公开(公告)日：2017-01-04

申请号：CN201610645892.X

申请日：2016-08-08

Applicant: 清华大学

Inventor： 孙家广 ,  王得希 ,  张超 ,  陈光 ,  贺飞 ,  顾明

IPC: G06F11/36

Abstract: 本发明提供了一种基于扩展符号变迁系统的C语言程序软件验证方法及装置。该方法包括：对待测对象C语言程序源代码插入验证属性描述；对插入验证属性的C语言程序源代码按照扩展的符号变迁系统ELTS语法构造ELTS程序模型；根据所述ELTS程序模型，生成可满足性求解SMT的模型路径；使用SMT工具对所述ELTS程序模型模型路径进行可达性的分析和验证；根据可达性分析和验证的结果生成ELTS程序模型反例，根据所述ELTS程序模型反例映射生成C语言程序反例。本发明实施例自动化建立ELTS程序模型，结合模型检测和严格的数学推理得到验证结果，相比于其它形式化方法具有准确率更高、程序覆盖率更好的特点，提高了软件验证的效率和准确性。

公开(公告)号：CN106294148B

公开(公告)日：2018-12-11

申请号：CN201610645892.X

申请日：2016-08-08

Applicant: 清华大学

Inventor： 孙家广 ,  王得希 ,  张超 ,  陈光 ,  贺飞 ,  顾明

IPC: G06F11/36

Abstract: 本发明提供了一种基于扩展符号变迁系统的C语言程序软件验证方法及装置。该方法包括：对待测对象C语言程序源代码插入验证属性描述；对插入验证属性的C语言程序源代码按照扩展的符号变迁系统ELTS语法构造ELTS程序模型；根据所述ELTS程序模型，生成可满足性求解SMT的模型路径；使用SMT工具对所述ELTS程序模型模型路径进行可达性的分析和验证；根据可达性分析和验证的结果生成ELTS程序模型反例，根据所述ELTS程序模型反例映射生成C语言程序反例。本发明实施例自动化建立ELTS程序模型，结合模型检测和严格的数学推理得到验证结果，相比于其它形式化方法具有准确率更高、程序覆盖率更好的特点，提高了软件验证的效率和准确性。