Given two programs $p_1$ and $p_2$, typically two versions of the same program, the goal of regression verification is to mark pairs of functions from $p_1$ and $p_2$ that are equivalent, given a definition of equivalence. The most common definition is that of partial equivalence, namely that the two functions emit the same output if they are fed with the same input and they both terminate. The strategy used by the Regression Verification Tool (RVT) is to progress bottom up on the call graphs of $P_1,P_2$, abstract those functions that were already proven to be equivalent with uninterpreted functions, turn loops into recursion, and abstract the recursive calls also with uninterpreted functions. This enables it to create verification conditions in the form of small programs that are loop- and recursion-free. This method works well for recursive functions as long as they are in sync, and typically fails otherwise. In this work we study the problem of proving equivalence when the two recursive functions are not in sync. Effectively we extend previous work that studied this problem for functions with a single recursive call site, to the general case. We also introduce a method for detecting automatically the unrolling that is necessary for making two recursive functions synchronize, when possible. We show examples of pairs of functions with multiple recursive calls that can now be proven equivalent with our method, but cannot be proven equivalent with any other automated verification system.
翻译:考虑到两个程序,通常是同一个程序的两个版本,即$_1美元和$2美元,回归核查的目标是根据对等性的定义,从$_1美元和$2美元对等功能对等功能进行标记。最常见的定义是部分等值,即两个函数如果以相同的输入输入输入,并且两者都终止,就会产生相同的输出。回归核查工具(RVT)使用的战略是,在调用 $P_1,P_2美元时向上推进,那些已经证明等同于未解释的函数的抽象函数,将循环转换成递归,并抽象的循环呼叫也与非解释的函数相对等值。这样,两个函数可以以不循环和递归的方式创建核查条件。这个方法在同步的同时,对于递归性功能来说,我们所研究的先前工作与自动递归对等性功能是无法自动递解的。这个方法的,在反复递归性功能被验证时,我们可以用一个被证实的系统对等值来验证。我们用一个被验证的系统来自动解析的重复性的方法来显示一个可能的循环。