ATLAS Group

We build systems that lift the capabilities of programmers dealing with the vast complexity of modern software systems. Our systems automate away inessential complexity and automate in desired features — for example, securing programs that use hundreds of software dependencies, bolting distribution onto existing applications, and parallelizing large-scale pipelines built out of multi-language components. We characterize the behavior of the systems we build using real workloads seen in practice, often paired with mathematical models and proofs of key properties of interest.

News #

Jul'26: Sash, a new ahead-of-time analysis of shell program effects, to appear at SOSP'26—see you in Prague!

Jul'26: At OSDI'26, try received both a Jay Lepreau Best Paper Award and a Best Artifact Award, and rt was a Best Paper runner-up!

May'26: Four OSDI'26 papers on bolt-on incrementalization with Incr, on opaque-component effect control with try, on speculative execution for shell and Python programs with hs, and on a regex-based type system for the Unix shell—see you in Seattle!

Apr'26: Extensions to the Koala benchmarks invited to ACM TOCS, following a recommendation by the USENIX ATC'25 chairs.

Apr'26: New approaches on securing agentic environments, internally (at EuroMLSys'26) and externally (Sc.M. thesis)!

Mar'26: Apply to attend the 2026 Brown Systems Week in beautiful Providence, RI!

Feb'26: Jiayi Wu and Kaitlyn Cheng join the group as UTRAs!

Jan'26: Two new pre-prints on LLM-assisted specification mining for opaque components and secure program regeneration.

Jan'26: We are organizing a tutorial on Analyzing Shell Scripts at POPL'26—join us in Rennes, France!

Sep'25: Early ideas on LLM guardrails, hybrid scheduling, and verifiable kernel extensions at SOSP'25 workshops!

See all news

Research #

Automating Protections Against Software Supply-Chain Threats
Modern software incorporates thousands of dependencies as a means of accelerating development and reducing cost—risking safety and security for both developers and end-users. We have built a series of systems targeting the JavaScript ecosystem—the largest such ecosystem out there—automating the analysis, transformation, and synthesis of JavaScript dependencies across a variety of threat models. Examples: OSDI'26, AsiaCCS'23, CCS'21, CCS'21.

Automating Acceleration and Scale-out of Software Systems
Language-agnostic programming environments hinder automated parallelization and distribution, often forcing developers to manually rewrite programs and their components in languages that support these features. We have built a series of systems that accelerate, parallelize, distribute, and scale out computations fully automatically—while maintaining key correctness and security guarantees. Our systems target widely used environments—e.g., JavaScript, Python, the Shell—and are offered by open-source consortia such as the Linux Foundation. Examples: OSDI'26, OSDI'26, NSDI'23, OSDI'22, EuroSys'21.

Automating Software Correctness
Programming correctness in modern software systems is hard to maintain as applications scale across dependencies, languages, and distributed environments. We build systems that automatically enforce, validate, and preserve correctness properties while remaining practical for real workloads. Examples: SOSP'26, OSDI'26, OSDI'26, HotOS'25, ICFP'21, HotOS'23, ARES'22, CCS'21.