Thesis Projects¶

The following projects are open for thesis students. Most of them build on VeIR, our compiler infrastructure written in Lean that combines an MLIR-style imperative design with (optional) interactive-theorem-prover-level verification.

SSA-Based Register Allocation for VeIR¶

Register allocation maps a program's unbounded set of values to the few registers of a real machine, and makes up about a third of the LLVM backend. Work at Saarland University showed that for programs in SSA form the interference graph is chordal: it can be colored optimally in polynomial time, and spilling, coloring, and coalescing become separate, simpler problems. In this project, you will implement an SSA-based register allocator for VeIR and prove it correct in Lean, i.e., that the allocated program computes the same result as the original. This cleaner structure makes a verified register allocator within reach and would bring formal guarantees to a large, bug-prone part of the compiler backend.

NVIDIA's TileIR for VeIR¶

CUDA Tile IR is NVIDIA's recently open-sourced, MLIR-based intermediate representation for GPU kernels, built around tile-based computations that target tensor cores. In this project, you will implement Tile IR as a dialect in VeIR, covering its operations and types, so that VeIR can read, process, and emit Tile IR programs. This will be the first project to enable GPU compute in Lean. Building on this, you can give Tile IR a precise semantics in Lean, enabling interpreters and verified rewrites for modern GPU code.

Formally Verified InstCombine for VeIR¶

InstCombine is LLVM's workhorse peephole optimizer: thousands of small rewrites that simplify instructions, and a well-known source of miscompilation bugs. In this project, you will implement InstCombine rewrites in VeIR and prove them correct in Lean, using automation such as Lean's bitvector decision procedure bv_decide to keep proofs push-button where possible. The result will be a verified subset of InstCombine that runs as part of a real compiler.

A Formally Verified MLIR Parser using Triparsers¶

VeIR connects to the MLIR ecosystem through MLIR's textual format, which makes its parser a critical, trusted component. In this project, you will build a parser for MLIR in VeIR using triparsers, and prove it correct in Lean, e.g., that printing and re-parsing a program yields the same program. A verified parser closes a gap in VeIR's trusted code base and makes the verification guarantees of VeIR hold end-to-end.

Fast Floating-Point Arithmetic in Lean¶

Floating-point arithmetic is at the heart of scientific computing and machine learning, but reasoning about it formally is notoriously hard. Our library fp.lean mechanizes IEEE 754 semantics in Lean and proves floating-point properties automatically by bit-blasting them to SAT with Lean's bv_decide, using circuits inspired by symfpu. In this project, you will develop new ideas for floating-point bit-blasting that go beyond what fp.lean offers today, so that proofs scale from small formats to the 16-, 32-, and 64-bit floats used in practice. One promising tool is bit heaps, which the hardware community uses to generate efficient arithmetic circuits: a bit heap represents a sum of many weighted bits, e.g., the partial products of a mantissa multiplication, and compresses them jointly instead of chaining individual adders. Applying this idea to bit-blasting could yield much smaller SAT encodings for floating-point multiplication and fused operations, while keeping the encoding verified in Lean.

Contact¶

Interested? Email Tobias Grosser.