Counter-Based Summarization of Recursive Procedures

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.