公开(公告)号：CN116340183A

公开(公告)日：2023-06-27

申请号：CN202310357127.8

申请日：2023-04-06

Applicant: 南京大学

Inventor： 卜磊 ,  谢准一 ,  郭骁 ,  孙羽 ,  马乐之 ,  赵建华 ,  李宣东

IPC: G06F11/36

Abstract: 本发明公开了一种基于路径遍历的代码验证方法、装置、介质及设备。该方法通过对循环体步进分解的方式，在控制流图中找出所有从程序入口至所述目标语句的路径长度不超过K的路径，组成路径集合；然后遍历路径，对所遍历的路径进行可达验证；在对路径进行可达验证时，通过对表达式简化计算将数组变量简化成数组元素，结合变量的约束替换，将关于数组变量的操作展开成关于数组元素的SMT约束表达式，从而使得SMT约束求解能够处理数组相关的变量，同时也降低了SMT约束求解的复杂度，免去了不可达路径片段的求解分析，从而提高了分析效率。

公开(公告)号：CN111444112B

公开(公告)日：2023-12-12

申请号：CN202010344638.2

申请日：2020-04-27

Applicant: 南京大学

Inventor： 卜磊 ,  闾乐成 ,  谢准一 ,  郭育鲲 ,  赵建华 ,  李宣东

IPC: G06F11/36 ,  G06F8/41

Abstract: 本发明公开了一种基于共享不可行路径池的代码并行验证方法和装置。该方法分为初始化过程、找出潜在路径过程和对潜在路径分析过程。在初始化过程中，输入的源程序和验证目标被构建成相应的SAT约束编码G。然后通过对不可行路径池中路径和SAT约束编码G的SAT求解，得到其SAT解对应的路径作为潜在路径存入并行任务池。再以多线程并行方式对并行任务池各个潜在路径进行SMT求解，若SMT无解，则抽取不可满足的最小集合X对应的不可行程序路径片段加入至不可行路径池。由此通过迭代，最终得到验证目标是否可达。为提高验证效率，本发明还增加了对不可行路径剪枝步骤。相比于现有技术，本发明大大提高代码验证效率。

公开(公告)号：CN111444112A

公开(公告)日：2020-07-24

申请号：CN202010344638.2

申请日：2020-04-27

Applicant: 南京大学

Inventor： 卜磊 ,  闾乐成 ,  谢准一 ,  郭育鲲 ,  赵建华 ,  李宣东

IPC: G06F11/36 ,  G06F8/41

Abstract: 本发明公开了一种基于共享不可行路径池的代码并行验证方法和装置。该方法分为初始化过程、找出潜在路径过程和对潜在路径分析过程。在初始化过程中，输入的源程序和验证目标被构建成相应的SAT约束编码G。然后通过对不可行路径池中路径和SAT约束编码G的SAT求解，得到其SAT解对应的路径作为潜在路径存入并行任务池。再以多线程并行方式对并行任务池各个潜在路径进行SMT求解，若SMT无解，则抽取不可满足的最小集合X对应的不可行程序路径片段加入至不可行路径池。由此通过迭代，最终得到验证目标是否可达。为提高验证效率，本发明还增加了对不可行路径剪枝步骤。相比于现有技术，本发明大大提高代码验证效率。