Coexecutability: How To Automatically Verify Loops

Abstract—Verification of web applications is a very important problem, and verifying loops is necessary to achieve that goal. However, loop verification is a long studied and very difficult problem. We find that interdependence of iterations is a major cause of this difficulty. We present coexecution- a way to model a loop that avoids the problem of iteration interdependence. We introduce the coexecutability condition that implies that coexe-cution is a correct model. Through experiments, we demonstrate that coexecution reduces the number of inconclusive verification results by three times, and in 43 % of cases increases performance of verification by at least an order of magnitude. Keywords—Verification, Loops I