Bounded translation validation (TV) is a common method used to check for the equivalence of two programs by unrolling all loops according to a user-supplied global bound. Unfortunately, large unroll bounds with multiple loops can increase the state space and the complexity of the TV. This paper proposes a systematic strategy for applying local unroll bounds for bounded TV of program pairs with loops. Our technique increases the coverage of the bounded TV in cases where the TV would otherwise timeout with the existing global unroll bounds. We introduce a lattice-based formulation of locally bounded program pairs and demonstrate that random sampling of local unroll bounds from this lattice admits a search-and-prune strategy that is effective for verification.

We have modified the Alive2 bounded TV to support local unroll bounds and evaluated our approach on benchmarks such as TSVC. The results show an increase in verification coverage with our lattice search-and-prune strategy combined with local unroll bounds.