Title: Permission Inference for Array Programs,
Abstract: Information about the memory locations accessed by a program is, for
instance, required for program parallelisation and program verification.
Existing inference techniques for this information provide only partial
solutions for the important class of array-manipulating programs. In this
paper, we present a static analysis that infers the memory footprint of an
array program in terms of permission pre- and postconditions as used, for
example, in separation logic. This formulation allows our analysis to handle
concurrent programs and produces specifications that can be used by
verification tools. Our analysis expresses the permissions required by a loop
via maximum expressions over the individual loop iterations. These maximum
expressions are then solved by a novel maximum elimination algorithm, in the
spirit of quantifier elimination. Our approach is sound and is implemented; an
evaluation on existing benchmarks for memory safety of array programs
demonstrates accurate results, even for programs with complex access patterns
and nested loops.