Improving the Robustness of Modern Software Systems #

Modern software systems fail in a variety of ways. We are developing systems for improving the reliability and robustness of these systems—including checks and guarantees before, during, and after their execution.

Systems and papers: RT (OSDI'26) is a new regular-language-based type system for inter-process communication. Sash (SOSP'26) statically analyzes shell program effects to find bugs before they cause irreversible damage. Towards expanding the reach of these analyses, Caruca mines specifications for the observable behavior of opaque components. During execution, the try subsystem (OSDI'26) controls the effects of opaque software components.

Several of the group’s projects deliver proofs of correctness for key properties. Our system, hS (OSDI'26) brings speculative out-of-order shell execution with a verified speculator component; Themis (ARES'22) analyzes the security properties of its decentralized service-interaction protocol suite; Harp (CCS'21) gives learning-and-regeneration guarantees aimed at preserving client-observable behavior while eliminating unwanted side-effects; and our PaSh ICFP'21 paper gives the formal core of PaSh’s parallelizing transformations and compiler.

Ongoing work: Our current work focuses on (1) correctness-preserving program and system transformations, (2) automated checking of key safety and behavioral invariants in production-like settings, (3) methods for reducing the gap between provable guarantees and practical deployment constraints, and (4) toolchains that combine formal reasoning with empirical validation.