← 返回列表
基于位向量SMT的软件形式化验证方法、系统及设备
摘要文本
本发明提供了一种基于位向量SMT的软件形式化验证方法、系统及设备，该方法包括：获取待验证的软件源代码，将软件源代码转化为相应的位向量SMT公式；识别位向量SMT公式中存在的位向量运算，根据各类位向量运算满足的运算规则对位向量SMT公式进行重写化简；对重写化简后的位向量SMT公式中的线性等式系统采用高斯消元法进行变量化简，对得到的位向量SMT公式重新执行上述重写简化和变量简化，直到位向量SMT公式达到最简状态，得到目标位向量SMT公式；将目标位向量SMT公式转化为CNF合取范式，并调用SAT求解器求解CNF合取范式以实现软件形式化验证。本发明通过对位向量SMT公式进行重写化简，能够有效提高软件验证的效率，确保软件的质量和安全性。
申请人信息
- 申请人:晞德求索(北京)科技有限公司
- 申请人地址:100080 北京市海淀区海淀大街甲36号5层5014室
- 发明人: 晞德求索(北京)科技有限公司
专利详细信息
| 项目 | 内容 |
|---|---|
| 专利名称 | 基于位向量SMT的软件形式化验证方法、系统及设备 |
| 专利类型 | 发明申请 |
| 申请号 | CN202311570874.6 |
| 申请日 | 2023/11/23 |
| 公告号 | CN117573537A |
| 公开日 | 2024/2/20 |
| IPC主分类号 | G06F11/36 |
| 权利人 | 晞德求索(北京)科技有限公司 |
| 发明人 | 林锦坤 |
| 地址 | 北京市海淀区海淀大街甲36号5层5014室 |
专利主权项内容
1.一种基于位向量SMT的软件形式化验证方法，其特征在于，所述方法包括：S11、获取待验证的软件源代码，将所述软件源代码转化为相应的位向量SMT公式；S12、识别所述位向量SMT公式中存在的位向量运算，根据识别出的各类位向量运算满足的运算规则对所述位向量SMT公式进行重写化简；S13、对重写化简后的位向量SMT公式中的线性等式系统，采用高斯消元法进行变量化简；对变量化简后的位向量SMT公式重新执行步骤S12～S13，直到位向量SMT公式达到最简状态，将最简状态的位向量SMT公式作为目标位向量SMT公式；S14、将所述目标位向量SMT公式转化为CNF合取范式，并调用预设的SAT求解器求解所述CNF合取范式以实现软件形式化验证。