Decidability of an Array Separation Logic fragment with Data Constraints

Abstract

Arrays are among the most commonly used data structures in programs. In order for a program analysis to be effective, it must be able to reason about both the memory safety and the contents of an array. Over the past couple of decades, advances have been made in proving memory safety using separation logic. While other lines of work have looked at proving properties about the contents of arrays. In this thesis, we present a new Array Separation Logic (ASL), that combines Separation Logic with the first-order theory of arrays. Therefore, this logic is capable of reasoning about memory safety, and the contents of the array. We study the satisfiability, and entailment problems for this logic. In order to study entailment, we define a graph-based semantics and present a decision procedure using graph homomorphisms. We implement, and evaluate our decision procedure, for a small number of example entailments.