Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp01cc08hj91v
Title: Counter-Based Summarization of Recursive Procedures
Authors: Pimpalkhare, Nikhil
Advisors: Kincaid, Zachary
Department: Computer Science
Class Year: 2023
Publisher: Princeton, NJ : Princeton University
Abstract: The work of this thesis lies within the field of program analysis, which seeks to provideformal reasoning about the behavior of programs without ever executing them. The approach that we use for program analysis involves computing a logical summary of an input program that narrowly over-approximates its behavior, followed by auto- mated reasoning algorithms to prove statements about program behavior. This thesis presents a compositional and monotone approach to the summarization of procedures with potentially multiple recursive calls, a particularly challenging domain. We sum- marize the dynamics of programs using vector addition systems with resets (VASR), a model that is simultaneously strong enough to capture interesting numerical be- havior and weak enough for its reachability relation to be computable. We show how to compute a VASR that is a best abstraction of an input program, how to compute the reachability of a VASR-weighted pushdown system, and how to combine these algorithms to produce summaries of programs. Together, these techniques combine for a summarization procedure that is performant, is capable of proving useful as- sertions in real-world programs, and makes theoretical guarantees about its relative performance on related programs. Our work offers a valuable contribution to the field of program analysis and paves the way for future advancements in verified software.
URI: http://arks.princeton.edu/ark:/88435/dsp01cc08hj91v
Type of Material: Academic dissertations (M.S.E.)
Language: en
Appears in Collections:Computer Science, 2023

Files in This Item:
File Description SizeFormat 
Pimpalkhare_princeton_0181G_14577.pdf402.27 kBAdobe PDFView/Download


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