Thesis Projects

Sophisticated Numerical Analyses in Sturdy

Sturdy is a Haskell library that simplifies the development of sound static analyses. Static analyses are tools that provide information about programs by inspecting their source code, but without running them. They are used in integrated development environments (IDEs), continuous integration servers, and compilers. A challenge in the design of static analyses is to ensure that the analysis results are reliable (sound). Soundness means that these information are correct and users can trust the results. However, formally proving that a static analysis is sound is a difficult and laborious task. To this end, Sturdy uses techniques for structuring static analyses, such that their soundness proof becomes simpler. For more information about Sturdy, take a look at the Sturdy website.

Apron is a library for developing sophisticated numeric analyses. It supports several relational numeric abstractions, such as intervals, polyhedra, zonotopes, octagons, and grids. The library is implemented in C for performance reasons. We would like to support these abstractions in Sturdy. The goal of this project is to integrate the Apron library in Sturdy by writing foreign-function interface (FFI) bindings for Apron in Haskell. Furthermore, to evaluate the bindings, the project should develop a proof-of-concept analysis with one of the abstract domains.

The challenge is that Haskell is a purely functional programming language, which means that functions cannot have effects unless explicitly declared in the type. In contrast, C does not have this restriction and side effects can occur everywhere. This means, the FFI bindings for Haskell need to declare all implicit side effects of the C library functions.

Efficient Ordering Check for Complex Analysis Data

Static analyses are tools that provide information about programs by inspecting their source code, but without running them. They are used in integrated development environments (IDEs), continuous integration servers, and compilers. For example, a interval analysis may calculate the range of numbers of integer variables during the execution of the program.

Unfortunately, some programs are too complicate to be analyzed precisely. In these cases, an analysis may yield less precise information that only approximates the runtime behavior of the program. For example, an interval analysis may yield a larger interval that contains numbers that a variable may not have during the execution of the program. To indicate which analysis results approximate the program behavior are more precise than others, the results are ordered. For example, intervals are ordered by inclusion.

An analysis may perform these ordering checks millions of times for large programs. In some cases, the overhead of the ordering checks can dominate the total runtime of the analysis. Furthermore, depending on the complexity of the analysis information, even a single ordering check may be prohibitively expensive. For example, some numeric analyses describe the relationship between multiple variables with convex polyhedra, whose ordering check has quadratic runtime. The project is to reduce the overhead of the ordering check by using special hashing that gives information about the ordering of elements. If the hash is unequal, the elements are definitely not in an ordering relation to each other. If the hash is equal, the elements may be in an ordering relation. The idea of the project is inspired by cryptographic hashes, that can identify isomorphic structures efficiently.