Program Checking and Indexed Data Structures

by Martin Sulzmann

In this talk, I'll provide a framework to perform program checking of programs that deal with indexed data structures such as matrices, arrays etc. For instance, I consider static program analyses to perform array-bounds checking. The task is to detect errors earlier, rather than to perform program optimizations. Previous approaches rely on the concept of dependent or shape types. In contrast, I consider a purely constraint-based approach which I believe has a couple of advantages. In previous work, there can already be found some use of constraints. Therefore, the constraint-based approach seems more natural. This opens an avenue to extend and incorporate other constraint-based analyses respectively it makes it easier to reuse other constraint-based approaches. The combination of indexed data structures and constraints leads to the concept of constrained data types. The concept of constrained data types increases the applicability of our form of program checking notably.