基于增量SMT问题求解的软件断言验证方法、系统及设备

专利主权项内容

1.一种基于增量SMT问题求解的软件断言验证方法，其特征在于，所述方法包括：获取待验证的软件源代码，按照代码执行路径将软件源代码中待验证的各个代码断言转化为相应的位向量SMT公式，得到位向量SMT公式集合；从位向量SMT公式集合中选取一个基础位向量SMT公式，根据位向量SMT公式集合各个位向量SMT公式所包括表达式之间的相似关系，将位向量SMT公式集合中其他位向量SMT公式相对于基础位向量SMT公式扩展出的增量表达式部分划分为多层上下文；对当前待求解的目标位向量SMT公式进行公式化简，并将化简后的目标位向量SMT公式转化为目标CNF合取范式；采用预设的简化后的SAT求解算法对目标CNF合取范式进行预求解，并在预求解过程中记录目标CNF合取范式中属于目标上下文的子句中所包括变量的变量标号，目标上下文为目标位向量SMT公式中相较于上一次求解的位向量SMT公式的增量部分的上下文；若预求解失败，则根据记录的目标上下文的子句中所包括变量的变量标号将包含相应变量标号的各个子句作为冗余子句进行删除；采用预设的完整的SAT求解算法对目标CNF合取范式进行求解。