Coexecutability for Efficient Verification of Data Model Updates

Modern applications use back-end data stores for persistent data. Automated verification of the code that updates the data store would prevent bugs that can cause loss or corruption of data. In this paper, we focus on the most challenging part of this problem: automated verification of code that updates the data store and contains loops. Due to dependencies between loop iterations, verification of code that contains loops is a hard problem, and typically requires manual assistance in the form of loop invariants. We present a fully automated technique that improves verifiability of loops. We first define co execution, a method for modeling loop iterations that simplifies automated reasoning about loops. Then, we present a fully automated static program analysis that detects whether the behavior of a given loop can be modeled using co execution. We provide a customized verification technique for co executable loops that results in more effective verification. In our experiments we observed that, in 45% of cases, modeling loops using co execution reduces verification time between 1 and 4 orders of magnitude. In addition, the rate of inconclusive verification results in the presence of loops is reduced from 65% down to 24%, all without requiring loop invariants or any manual intervention.