Skip navigation
Please use this identifier to cite or link to this item:
Title: Decidability of an Array Separation Logic fragment with Data Constraints
Authors: Mehta, Vaibhav
Advisors: Kincaid, Zachary
Department: Computer Science
Class Year: 2023
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.
Type of Material: Princeton University Senior Theses
Language: en
Appears in Collections:Computer Science, 1987-2023

Files in This Item:
File Description SizeFormat 
MEHTA-VAIBHAV-THESIS.pdf407.14 kBAdobe PDF    Request a copy

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.