Incremental Static Program Analysis through Modularity

Today, developers have come to rely on static analysis tools to verify a wide range program properties without actually running the program. As such, static analyses are typically integrated into
modern development environments and continuous integration systems to guarantee requirements on software quality throughout the development process. In this setting, it is not only important for the static analysis to deliver precise feedback, but also to efficiently update that feedback upon changes to the source code of the
program. For this purpose, an incremental static analysis avoids a full recomputation of the analysis upon a change in the program by reusing and updating the previously computed analysis result.

It is challenging to develop an incremental analysis that is powerful enough to verify a wide range of program properties and supports complex language features found in contemporary programming languages. We aim to design a novel approach to construct such analyses through modularity. That is, we posit that an analysis with a modular design can isolate the impact of a change more efficiently to the component that was affected by the change, so that only that component, and components transitively depending on it, need to be reanalyzed. Specifically, in this proposal we formulate a systematic approach to render a fundamental class of modular analyses incremental to increase their performance in real-life development processes.