Projects
Over the years, the group's work has come to center on a few long-running projects — a trust stack for reasoning about low-level software, and operating systems, compilers, and runtimes for heterogeneous-ISA hardware. Alongside these, the group works on improving the security and reliability of existing software, safely modernizing legacy code, reasoning about concurrent programs, and developing new program-analysis and machine-learning techniques for reasoning about security properties at scale — drawing on the group’s roots in concurrency, distributed systems, operating systems, and real-time computing.
LLRM — Low-Level Reasoning Machine
A foundation for verifying security and correctness properties of binaries: formalized ISA semantics, verified lifting, program logics, and prover-assisted reasoning over stripped, position-independent code.
FoxDec — Formally verified x86-64 decompilation
Verifiably correct lifting of x86-64 binaries to an IR that is recompilable, patchable, and validatable, with the soundness of each phase formalized in Isabelle/HOL. Recompiled binaries are shown observationally equivalent to the original.
libLISA
Automated discovery and analysis of x86-64 instruction semantics — a validated foundation for reasoning about machine code.
MESA
Program analysis cast as mathematical optimization, including scalable floating-point satisfiability via staged optimization.
Popcorn Linux
A replicated-kernel operating system and compiler toolchain for executing and migrating a single application across machines with different instruction sets (x86, Arm, RISC-V) and across CPUs, FPGAs, and SmartNICs.
LibrettOS
A multiserver / library operating system combining the isolation of a microkernel with the performance of a library OS, with POSIX and legacy driver support.
Several further projects are under active development. See the publications for the results behind these systems.