We present a new technique for inferring expressive invariants over array programs. To overcome the challenges in statically reasoning about arrays that can often confound analyses, both because of side-effecting array update operations, and the need to reason about quantified invariants on array indices, our approach first infers very coarse invariant templates, and then uses test suites that exercise the functionality of the program to instantiate these templates with more precise (likely) invariants. These inferred invariants are subsequently encoded within an expressive dependent type system for validation. Experimental results demonstrate the utility of our approach, with respect to both expressivity of the invariants inferred, and the time necessary to converge to a result.
Technique descriptions of ASolve and its proof of correctness can be found in this manuscript [pdf].
The source codes and an environment for compiling and running can be downloaded as a virtual machine image (VirtualBox, VMware, etc).
The benchmarks, for our experiments, can be downloaded here: Benchmarks.