WG211/M23Kellogg

Static Program Reduction via Specification Slicing (Martin Kellogg)

Program reduction is the process of making a program smaller while preserving a property of interest, such as the presence or absence of a particular warning from a compiler or other static analysis tool. Traditional approaches to program reduction are dynamic: they use a delta-debugging-like algorithm to iteratively reduce the program while preserving the property of interest. In this talk, I will present a static program reduction technique, called specification slicing, that exploits the modularity of extant analysis tools whose output we are interested in preserving (e.g., type systems) to accomplish program reduction without the need to repeatedly run the analysis. The key advantage of this program reduction technique are its cost and ease of application: it does not require that we run the analysis whose output we are trying to preserve at all, and so it can be run in a tight loop. I will also discuss new uses of program reduction that this advantage unlocks (especially in the context of combining verification tools and large language models).

This talk is about work in progress.

Slides (pdf)