Relational Verification of Programs with Integer Data

This work presents novel methods for verication of reachabilityand termination properties of programs that manipulateunbounded integer data. Most of these methodsare based on acceleration techniques which compute transitiveclosures of program loops.Firtly, we present an algorithm that accelerates severalclasses of integer relations and show that the new methodperforms up to four orders of magnitude better than theprevious ones. On the theoretical side, our frameworkprovides a common solution to the acceleration problemby proving that the considered classes of relations are periodic.Subsequently, we introduce a semi-algorithmic reachabilityanalysis technique that tracks relations between variablesof integer programs and applies the proposed accelerationalgorithm to compute summaries of proceduresin a modular way. Next, we present an alternative approachto reachability analysis that integrates predicateabstraction with our acceleration techniques to increasethe likelihood of convergence of the algorithm. We evaluatethese algorithms and show that they can handlea number of complex integer programs where previousapproaches failed.Finally, we study the termination problem for severalclasses of program loops and show that it is decidable.Moreover, for some of these classes, we design a polynomialtime algorithm that computes the exact set ofprogram congurations from which non-terminating runsexist. We further integrate this algorithm into a semialgorithmicmethod that analyzes termination of integer programs, and show that the resulting technique can verifytermination properties of several non-trivial integerprograms.