Regression verification of unbalanced recursive functions with multiple calls (long version)
share
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.
READ FULL TEXT