Skip navigation
Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorKincaid, Zachary-
dc.contributor.authorMehta, Vaibhav-
dc.description.abstractArrays 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.en_US
dc.titleDecidability of an Array Separation Logic fragment with Data Constraintsen_US
dc.typePrinceton University Senior Theses
pu.departmentComputer Scienceen_US
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.