一种基于精化约束重用的并行程序增量式回归验证方法

摘要

本发明公开了一种基于精化约束重用的并行程序增量式回归验证方法，本发明方法包括在针对当前程序版本Mi进行基于精化约束抽象精化的并行程序验证时，每执行一轮验证过程中的迭代，则针对当前程序版本Mi对应的程序抽象的事件顺序图中的环生成关键源并记录到关键源库中，对关键源库进行关键源有效性判定，分别对各个有效关键源通过精化约束适配生成精化约束以参与下一轮验证过程中的迭代。本发明基于现有基于调度约束抽象精化的并行程序验证方法实现了增量式回归验证技术，通过精确计算代码修改对精化约束的影响和开展精化约束的适配，可实现对前面程序版本验证中的精化约束进行重用，从而有效提高代码演化环境下并行程序的回归验证效率。