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 sytems—including checks and guarantees before, during, and after their execution.

Systems and papers: Our HotOS'25 paper, From Ahead-of- to Just-in-Time and Back Again, pushes this line toward static analysis for real shell programs. Towards expanding the reach of these analyses, Caruca mines specifications for the observable behavior of opaque components, and Try complements this direction with a lightweight frontend for inspecting a command’s effects before it touches a live system.

Our PaSh ICFP'21 paper, An order-aware dataflow model for parallel Unix pipelines, gives the formal core of PaSh’s parallelizing transformations and compiler.

Several of the group’s projects deliver proofs of correctness for key properties. Our system, hS (HotOS'23) 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; and Harp (CCS'21) gives learning-and-regeneration guarantees aimed at preserving client-observable behavior while eliminating unwanted side-effects.

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.