Sound, Efficient, and Flexible Fixpoint Algorithms for Big-Step Abstract Interpreters

• Applicant: Professor Dr. Sebastian Erdweg
• Subject Area: Software Engineering and Programming Languages
• Term: since 2021
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 451545561

Static analysis of source code plays a crucial role in generating programmer feedback, validating correctness properties, and enabling compiler optimizations. In the past, many sound static analyses have been defined as abstract interpreters in small-step style, where the abstract semantics is described as a state transition system. More recently, the PI and other researchers have explored abstract interpreters in big-step style, where the abstract semantics can be simply described as recursive functions in a meta-language such as Haskell. This makes big-step abstract interpreters easier to define and easier to maintain. However, the scalability of abstract interpreters hinges on their fixpoint algorithm. Unfortunately, existing fixpoint algorithms of small-step abstract interpreters are not transferrable to big-step abstract interpreters, and thus no efficient big-step fixpoint algorithms exist to date.In this project, we will develop a family of fixpoint algorithms for big-step abstract interpreters. To ensure termination, these fixpoint algorithms must solve novel challenges that are specific to big-step evaluation. Besides termination, we target three important concerns. First, our fixpoint algorithms must be sound, meaning they over-approximate the ideal yet incomputable least fixpoint. We will establish a formal theory for big-step fixpoint algorithms that enables us to prove soundness. Second, our fixpoint algorithms must be efficient and scale to the analysis of realistic software projects. We will explore the application of our algorithms to inter-procedural Java bytecode analyses, though we expect performance bottlenecks in the initial design. To address these bottlenecks, third, our fixpoint algorithms also must be flexible, such that the analysis developer can choose how to trade-off precision for performance. To this end, we will explore how context-sensitivity and method summaries can be supported in big-step fixpoint algorithms. By designing efficient, sound, and flexible big-step fixpoint algorithms, this project will enable the development of big-step abstract interpreters that are easy to understand and scale well.

• DFG Programme: Research Grants