Separating Map Variables in a Logic-Based Intermediate Verification Language.

In SMT solver based verification, the program to be verified is often given in an intermediate verification language such as Boogie. We present a program transformation that aims at splitting mathematical arrays (i.e., maps, which are typically used to model arrays and specifically the heap) into different partitions, so that the resulting verification conditions are easier to solve (due to the need of fewer case splits when analysing the effect of reads and writes over the same array). Our method takes the similar role of classical preprocessing steps based on alias analysis; the difference is that it works on any (mathematical) map, as opposed to a data structure that is known to present a chunk of memory managed by some compiler. Having to forfeit the benefits of general assumptions about memory (e.g., allocate-before-use), we need to deal with additional difficulties but obtain a more general technique. In particular, our technique can be applied to arbitrary programs in the intermediate verification language, including programs that are not directly derived from a program in a production-type programming language, like C or Java. We have implemented a prototypical version of the program transformation in order to demonstrate that it can lead to up to exponential reductions in execution time for the Ultimate software verification tool, despite the cost of performing the initial static analysis.