Convex Hull Procedure for Linear Integer Arithmetic

Abstract

With software becoming increasingly complex, the tasks of maintaining, debugging and understanding the behavior of software has become difficult. With these increasing trend of difficulties, automated frameworks that can analyze the code of a program and generate analyses are our helping hand. Farzan and Kincaid provide such an automated framework known as Compositional Recurrence Analysis (CRA) \cite{farzan2015compositional}. CRA approximates loop behavior in a program by converting the loop body to a logical formula and extracting recurrence inequations from this formula. These recurrence inequations approximate the behavior of the loop. This part of CRA uses an algorithm that takes as input a logical formula and computes the convex hull of solutions over linear rational arithmetic. This handles the case when program variables range over rational numbers. However, when program variables range over integers, stronger recurrence inequations can be extracted by using an algorithm that takes as input a logical formula and computes the convex hull of solutions over linear integer arithmetic. This is an important problem as stronger recurrence inequations translates to closer analyses of loop and thereby program behavior. In this work, we design such an algorithm, show its correctness, implement variations of this algorithm and show cases where this stronger analysis makes a difference.