Skip navigation
Please use this identifier to cite or link to this item:
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorKincaid, Zachary
dc.contributor.authorDattatri, Adithya
dc.description.abstractWith software becoming increasingly complex, the tasks of maintaining, debugging and understanding the behavior of software has become difficult. With these increasing trend of difficulties, automated frameworks that can analyze the code of a program and generate analyses are our helping hand. Farzan and Kincaid provide such an automated framework known as Compositional Recurrence Analysis (CRA) \cite{farzan2015compositional}. CRA approximates loop behavior in a program by converting the loop body to a logical formula and extracting recurrence inequations from this formula. These recurrence inequations approximate the behavior of the loop. This part of CRA uses an algorithm that takes as input a logical formula and computes the convex hull of solutions over linear rational arithmetic. This handles the case when program variables range over rational numbers. However, when program variables range over integers, stronger recurrence inequations can be extracted by using an algorithm that takes as input a logical formula and computes the convex hull of solutions over linear integer arithmetic. This is an important problem as stronger recurrence inequations translates to closer analyses of loop and thereby program behavior. In this work, we design such an algorithm, show its correctness, implement variations of this algorithm and show cases where this stronger analysis makes a difference.
dc.titleConvex Hull Procedure for Linear Integer Arithmetic
dc.typePrinceton University Senior Theses
pu.departmentComputer Science
Appears in Collections:Computer Science, 1988-2023

Files in This Item:
File Description SizeFormat 
DATTATRI-ADITHYA-THESIS.pdf365.66 kBAdobe PDF    Request a copy

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