Paper Info
Title
Regression Verification for Unbalanced Recursive Functions.
Abstract
We address the problem of proving the equivalence of two recursive functions that have different base-cases and/or are not in lockstep. None of the existing software equivalence checkers (like REVE, RVT, SYMDIFF), or general unbounded software model-checkers (like SEAHORN, HSFC, AUTOMIZER) can prove such equivalences. We show a proof rule for the case of different base cases, based on separating the proof into two parts-inputs which result in the base case in at least one of the two compared functions, and all the rest. We also show how unbalanced unrolling of the functions can solve the case in which the functions are not in lock-step. In itself this type of unrolling may again introduce the problem of the different base cases, and we show a new proof rule for solving it. We implemented these rules in our regression-verification tool RVT. We conclude by comparing our approach to that of Felsig et al.'s counterexample-based refinement, which was implemented lately in their equivalence checker REVE.
Year
DOI
Venue
2016
10.1007/978-3-319-48989-6_39
Lecture Notes in Computer Science
Field
DocType
Volume
Regression,Computer science,Theoretical computer science,Software,Equivalence (measure theory),Recursive partitioning,Recursive functions,Counterexample
Conference
9995
ISSN
Citations 
PageRank 
0302-9743
5
0.42
References 
Authors
11
2
Name
Order
Citations
PageRank
Ofer Strichman1107163.61
Maor Veitsman250.42