Nikhil Pimpalkhare will present an MSE talk entitled "Context-Free Counter-Based Procedure Summarization" on April 26, 2023 at 4pm in CS 402.

The committee is as follows: Zachary Kincaid (adviser) and David Walker (reader)

All are welcome to attend.

Title: "Context-Free Counter-Based Procedure Summarization". My abstract is as follows:

Abstract:

Program analyses aim to formally reason about program behavior without ever running them. A typical structure of a program analysis is to compute a logical summary of an input program that over-approximates its behavior as narrowly as possible, then use automated reasoning algorithms to prove statements about program behavior. This paper addresses procedure summarization for a particularly challenging domain, nonlinear recursive programs, in a way that is both compositional and monotone. We summarize program transformations using vector addition systems with resets (VASR), a model that is simultaneously strong enough to capture interesting numerical behavior and weak enough for its reachability to remain 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. We additionally introduce a novel method to synthesize linear bounds on recursive depth, increasing the specificity of our summary. Together, these techniques combine for a summarization procedure which is performant, powerful, and predictable.