cache_ext is a framework to customize Linux page cache eviction policies using BPF. Appeared in SOSP 2025.

Research prototype tool for modular formal verification of C, Rust and Java programs

Verifying the Rust standard library

Experiment with BPF_MAP_TYPE_HASH_OF_MAPS

A LLVM-based static analysis framework.

A PROMELA model for FreeRTOS

FreeRTOS kernel files only, submoduled into https://github.com/FreeRTOS/FreeRTOS and various other repos.

Awkernel: realtime operating system written in Rust

Concurrency permutation testing tool for Rust.

Interference-aware CPU scheduling that enables performance isolation and high CPU utilization for datacenter servers

RD-Gen (random DAG generator considering multi-rate applications for reproducible scheduling evaluation) is a tool for researchers targeting DAGs.

An rclcpp-compatible true zero-copy IPC middleware that supports all ROS message types, including message structs already generated by rosidl.

A minimal Linux kernel module written in rust.

HEFT, randomHEFT and IPEFT algorithms for static list DAG Scheduling

Explicit state logic model checking tool -- 2002 winner of the ACM System Software Award.

Linux running inside a PDF file via a RISC-V emulator

LLTZ: Compiler from MLIR to Michelson

Homebrew Taps for my favorite scientific software

Production-grade client-side tracing, profiling, and analysis for complex software systems.

The FlexFringe tool for flexible learning of state machines (deterministic automata) from traces. See the paper at https://arxiv.org/abs/2203.16331

Linux v6.11 Kernel Module for Print VMA

A machine learning toolkit for log parsing [ICSE'19, DSN'16]

Tamarin models for state continuity of SGX enclave programs

A minimal Linux scheduler with sched-ext written in C