Discovering Properties about Arrays via Path Dependence Analysis

Array, as a fundamental data structure, is widely used in programs. Automated reasoning about arrays needs to discover properties about ranges of elements at certain program points. Such properties are formally specified by universally quantified formulas. A universally quantified formula usually includes two parts: the index range and the properties of the corresponding array elements. In this paper, we first propose a classification of array-handling loops to understand the complexity of discovering two parts of properties about arrays, which is based on whether array variables appear in judgment statements (loop conditions and loop branch conditions). Secondly, for each type, we extend the path dependency automaton (PDA) to capture the dependencies between paths for an array-handling loop and discover useful facts about individual elements for each state of the PDA. Finally, an algorithm is proposed to identify the index range and generalize useful facts about individual elements to entire ranges for each state of the PDA. These properties are enough to verify the assertion of the end of the program. We show this method can be extended to programs with complex loops and nested loops as well. The result of experiments shows that this method outperforms several state-of-the-art tools on a suite of benchmarks from SV-COMP.