Abstract:
RVT is a regression verification tool for proving partial equivalance for pairs of programs, i.e., that the two functions emit the same output if they are fed with the same input and they both terminate. To do so, RVT traverses bottom-up on the call graphs of the pair, turn loops into recursions, abstract the recursive calls with uninterpreted functions and abstract pairs that are proved as equivalent 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 as long as the two compared recursions are in sync. In this work we study the problem of proving equivalence when the two recursive functions are not in sync. We extend previous work that studied this problem for functions with a single recursive call 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.