Skip to content Search
Search our website:

Static Analysis of Termination and Time Complexity for Rust Programs

Static Analysis of Termination and Time Complexity for Rust Programs

Principal supervisor: Dr Carsten Fuhs

Systems programming languages like C or C++ are notorious for security leaks due to programming mistakes, yet they continue to be in widespread use due to the efficiency of the generated machine code. On the other end of the spectrum, there are programming languages with built-in memory safety, such as Java, Python, ... The price paid in these languages is that at runtime, execution of the program is periodically interrupted for garbage collection, and the programmer does not get low-level memory access at all.

In 2010, the Rust programming language was introduced to enable writing system programs that are both highly efficient and memory-safe by default. Instead of costly memory management via garbage collection, an elaborate ownership-based type system prevents unsafe memory accesses at compile time. At the same time, potentially unsafe low-level memory access can still be performed in specifically marked sections of the source code. In recent years, Rust has seen a significant uptake in a number of open-source and industrial settings.

Although the safety measures on language level are already very useful for preventing bugs in Rust programs, additional tool support to help Rust developers write bug-free code is highly desirable. This is currently a topic of intensive research. However, what is missing are dedicated tools for analysis of termination and for automatic inference of time complexity bounds. Here termination is the property that a program's execution will finish in finite time for all inputs, and non-termination usually indicates a bug. Inference of time complexity bounds is a refinement of the termination question: whereas termination asks "Does the program finish at all?", complexity asks "How quickly is the program guaranteed to finish for an input of size n?", which is possibly of even higher practical importance.

While these properties are famously undecidable, corresponding static analysis tools (like Microsoft's T2 tool with its termination analysis, Facebook's Infer tool with its complexity analysis, or the AProVE tool co-developed by the principal supervisor) exist for several programming languages (e.g., Java, C, Haskell, Prolog). However, the specifics of the Rust language, in particular its type system, have not yet been addressed.

The goal of this PhD project is to develop techniques for automated analysis of termination and runtime complexity properties of Rust programs and to implement and empirically evaluate these techniques in a prototype software tool.

Candidate Requirements:

This PhD project involves both theoretical and practical components. On the theoretical side, the program analysis steps to be described on formal level, and correctness of the pursued approach will need to be proved. Thus, the PhD candidate should have an affinity to logic and formal settings. On the practical side, feasibility of the approach is shown by developing and experimentally evaluating a software tool that performs the proposed analysis automatically. Thus, the PhD candidate student should also have a good programming background.

Key References:

[1] Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann: Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 58(1): 3-31 (2017) (Preprint)

[2] Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs, Jürgen Giesl: Analyzing Runtime and Size Complexity of Integer Programs. ACM Trans. Program. Lang. Syst. 38(4): 13:1-13:50 (2016) (Preprint)

Further details about the project may be obtained from:

Principal supervisor: Dr Carsten Fuhs

Further information about PhDs at CSIS is available via this link.