Coexecutability for Efficient Verification of Data Model Updates

Abstract—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 coexecution, 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 coexecution. We provide a customized verification technique for coexecutable loops that results in more effective verification. In our experiments we observed that, in 45 % of cases, modeling loops using coexecution 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. I