Gradual Abstract Interpretation

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

Static analysis of source code plays a crucial role in generating programmer feedback, validating correctness and security properties of programs, and enabling compiler optimizations. A static analysis derives properties about a program without considering concrete input values and without executing the program. Instead, a static analysis predicts the possible results and effects of running the program for all possible inputs. Unfortunately, static analysis of practical programming languages is undecidable due to Rice's theorem and static analyses therefore must trade-off precision, recall, and performance. Prior work showed that combining static analysis with dynamic analysis into a hybrid analysis can improve analysis results significantly. While a static analysis must be conservative (losing precision) or risk unsoundness, a hybrid analysis can be optimistic (retaining precision) and delegate soundness checks to the dynamic analysis at run-time. Unfortunately, most past approaches for constructing hybrid analyses are ad-hoc: the static and dynamic analysis must be implemented individually, they collaborate by convention but not by design, and there are no correctness guarantees. Recently, PI Tanter and colleagues proposed gradual program analysis as a novel theory for constructing hybrid analyses by gradualizing a static analysis, based on the prolific line of research on gradual typing, which has seen great adoption in industry. Initial work on gradual program analysis showed how the theory can be instantiated to develop a simple gradual null-pointer analysis. While promising, it is unclear how to scale this approach to more expressive and advanced analyses. In this project, we will deepen the theory of gradual program analysis into a general approach for developing gradual analyses that is easy to use, supports sophisticated programming languages and program properties, and yields implementations of gradual analyses that scale to real-world code bases. In doing so, we must find answers to fundamental questions such as: how to gradualize abstract domains of infinite height, how to reason about effectful computations gradually, and how to derive a dynamic program analysis systematically? We will not only explore these questions theoretically, but also study how to realize gradual program analyses modularly as gradual definitional abstract interpreters in PI Erdweg's analysis framework Sturdy, which is being used for the static analysis of real-world WebAssembly programs. We will extend Sturdy to provide the first practical framework for gradual program analysis.

• DFG Programme: Research Grants
• International Connection: Chile
• Partner Organisation: Agencia Nacional de Investigación y Desarrollo (ANID)
• Cooperation Partners: Professor Dr. Éric Tanter; Professor Dr. Matías Toro Ipinza