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 #
See all news
Team #
Atharv Chowdhary
B.Sc. Student
Eric Zhao
Ph.D. Student
Ethan Lavi
Ph.D. Student
Evangelos Lamprou
Ph.D. Student
George Kapetanakis
Visiting Student
Grigorios Ntousakis
Ph.D. Student
Jerry Xia
B.Sc. Student
Jiayi Wu
B.Sc. Student
Kaitlyn Cheng
B.Sc. Student
Ken Mahattanadul
M.Sc. Student
Lukas Lazarek
Postdoc
Maria Lazou
Visiting Student
Megan Zheng
B.Sc. student
Nikos Vasilakis
Faculty
Oğuzhan Çölkesen
Ph.D. Student
Yasmin Kadyrova
M.Sc. Student
Yizheng Xie
Ph.D. Student
Yuchen Lu
Ph.D. Student
Zekai Li
M.Sc. Student
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:
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:
NSDI'23,
OSDI'22,
EuroSys'21.
Automated Transformation Towards Secure Scalable Computing Paradigms
Recent trends are pushing developers towards new paradigms of secure and scalable computing—e.g., confidential computing, microservices, serverless computing, and edge computing. Transforming a conventional program to leverage these paradigms is a laborious manual process that can lead to suboptimal performance and in many cases even break the program. We are developing systems that support this kind of decomposition and leveraging special hardware capabilities when these are available in the network. Examples:
ARES'22,
PLDI'19,
ATC'19.
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:
HotOS'25,
ICFP'21,
HotOS'23,
ARES'22,
CCS'21.