Grand Challenge 3
How do we build computing systems that can be trusted to do exactly what we want them to do, every time?
From elections to energy grids, society depends on computers that must be safe, secure, and reliable: not just 90% or even 99% of the time, but every time.
That’s where verification comes in: using math to prove software always behaves as intended. In the lab, verification has been shown to produce applications that are dramatically safer and more reliable. But real-world code is so complex, most of it can’t be fully verified today, and the rise of unpredictable AI and “vibe coding” only raises the stakes. Allen School researchers are working to make verification practical across the stack — from chips and compilers, to cryptographic protocols and ML-powered apps.
Faculty Meeting the Challenge
Assistant Professor
Architecture & Parallel Computing; Operating & Distributed Systems; Security & Privacy
Associate Professor
Architecture & Parallel Computing; Computer Networking; Operating & Distributed Systems; Programming Languages
Professor
Computing Education Research; Formal Methods; Programming Languages; Security & Privacy; Software Engineering
Associate Professor
Cloud Computing; Computer Networking; Formal Methods; Operating & Distributed Systems
Professor
Augmented, Virtual & Mixed Reality; Human-Computer Interaction; Security & Privacy
Collaborators & Partner Institutions
Selected Projects
Avoiding Instruction-Centric Microarchitectural Timing Channels Via Binary-Code Transformations
Michael Flanders, Reshabh Sharma, Alexandra Michael, Dan Grossman…
Succinct Homomorphic MACs from Groups and Applications
Yuval Ishai, Hanjun Li, and Huijia Lin…
Mangrove: A Scalable Framework for Folding-based SNARKs
Wilson Nguyen, Trisha Datta, Binyi Chen, Nirvan Tyagi, Dan Boneh…