Marius Bozga, Radu Iosif, Filip Konecny
Relational Analysis of Integer Programs (2012)
Relational Analysis of Integer Programs (2012)
TR-2012-10.pdf
Keywords: reachability analysis, acceleration, transitive closures, periodic relations, programs with integer data
Abstract: Verifying an integer program against safety requirements requires, in general, the computation of an invariant of the program, needed to prove the unreachability of one or several error states. Traditionally, such invariants are computed by handling finite representations of potentially infinite sets of states, such as abstract domains, boolean combination of predicates, etc. In this paper, we introduce a method of proving safety properties, that tracks relations instead of sets of states. As relations store, in general, more information about the system's behavior than reachability sets, they prove to be a useful tool in designing modular verification techniques, in which each function of the program is analysed separately, and its computed summary is plugged in at every call site. The key to computing accurate relations describing the behavior of a program is inferring the transitive closures of the relations labeling the control loops of the program. We describe an efficient algorithm for computing the transitive closures of difference bounds, octagonal and finite monoid affine relations. On the theoretical side, this framework provides a common solution to the acceleration problem, for all these classes of relations. In practice, according to our experiments, the new method performs up to four orders of magnitude better than existing acceleration algorithms, making it a promising approach for the verification of integer programs. The transitive closure algorithm has been implemented and integrated in a tool for the interprocedural analysis of integer programs.
