Systematic software analyses, such as model checking and symbolic execution, perform systematic exploration of program behaviors to find faults in software systems. While the usefulness of systematic software analyses for improving software reliability has long been established, scaling them to real-world applications remains a key technical challenge, since the state spaces of these applications typically are large and computationally expensive to explore systematically.
This project develops a memoization-based approach to enhance scalability of systematic analyses. Specifically, the analysis results are re-used to amortize the cost of analysis over multiple successive executions of the analysis. The project investigates foundations that provide the basic tool-set for enabling reuse of analysis results, optimizations that specialize memoized analyses in the context of change, and the use of parallel techniques to effectively utilize the available computing resources. The technical contributions of the project could significantly enhance the efficacy of systematic analyses, which could have a broad impact by improving the quality of software systems.
