Incremental static program analysis through reified computational dependencies

Over the last few decades, computers have become an indispensable part of modern society. As the programs running on these computers play an essential role in
everyday life, for example in banking and communication, it is crucial that they are reliable. To this end, developers have come to rely on static analysis tools to verify a wide range of program properties without actually running the program. Static analyses are typically integrated into modern software development environments and continuous integration systems to safeguard software quality throughout the entire development process.

During the development process, software developers continuously apply small changes to the program. It is therefore not only important for a static analysis
to deliver precise feedback, but also to efficiently update its feedback whenever the program is modified. To this end, an incremental static analysis avoids a full
recomputation of the analysis result. Instead, upon a change in the program, it reuses and updates the previously computed result, saving valuable analysis time.

It is challenging to develop an incremental analysis that is sufficiently powerful to verify a wide range of program properties and that supports complex language
features found in contemporary programming languages. In this work, we present a novel generic approach to construct such analyses by using reified computational dependencies. We show how an analysis that reifies the computational dependencies within the analysed program can be rendered incremental. By
relying on these dependencies, our incremental analysis restricts the impact of a change to the affected parts of the analysis result. Moreover, we impose minimal
requirements on the analysis itself, allowing a broad applicability of our approach to incrementalisation.

To preserve the precision of the resulting incremental analysis, we introduce three complementary result-invalidation strategies that limit the loss in precision.
These strategies are built around the core idea of interleaving invalidation with computation.