July 21, 2021
Isabel García
Automatic static analysis tools allow inferring properties about software without executing it and without the need for human interaction. When these tools are based on formal methods, the properties are guaranteed to hold and come with a mathematical proof. The usage of these tools during the coding, testing, and maintenance phases of the software development cycle helps reduce efforts in terms of time and cost, as they contribute to the early detection of bugs, automatic optimizations, or automatic documentation. The increasing importance of the reliability of evolving software is evidenced by the current number of tools and on-line platforms for continuous integration and deployment. In this setting, when changes happen fast, analysis tools are only useful if they are precise and, at the same time, scalable enough to provide results before the next change happens. In this thesis we study scalable analyses in the context of abstract interpretation. Since a way to improve scalability is to perform coarser abstractions, we first inspect what effect this may have in effectively proving the absence of bugs. Second, we present a framework for scalable static analyses which is generic, that is, independent of the data abstraction of the program. We present several algorithms for incrementally reanalyzing whole programs in a context-sensitive manner, reusing as much as possible previous analysis results. A key novel aspect of the approach is to take advantage of the modular structure of programs, typically as defined by the programmer, while keeping a fine-grained relation between the analysis result and the source program. Additionally, we present a mechanism for the programmer to help the analyzer in terms of precision and performance by means of assertions. We show that these assertions together with incremental analysis are specially useful when analyzing generic code. All these algorithms have been implemented and evaluated for different abstract domains within the CiaoPP framework. Lastly, we present an application of the analysis framework to perform on-the-fly assertion checking, providing continuous and almost instantaneous feedback to the programmer as the code is written. Here the incrementality and modular nature of the presented algorithms, and the locality of the changes, are key to achieving fast response times.