Emily First (Postdoc)
Brian Hempel (Postdoc)
Andrew Cheung (Ph. D. student, started 2024)
Raven Rothkopf (Ph. D. student, started 2024)
Saketh Kasibatla (Ph. D. student, started 2023)
Ilana Shapiro (Ph. D. student, started 2023)
Kyle Thompson (Ph. D. student, started 2023)
Ruanqianqian (Lisa) Huang (Ph. D. student, started 2020)
Yousef Alhessi (Ph. D. student, started 2018)

Kasra Ferdowsi (Ph. D. 2024)
Alex Sanchez-Stern (Ph. D. 2021)
John Sarracino (Ph. D. 2021)
Valentin Robert (Ph. D. 2018)   →   Galois
Dimitar Bounov (Ph. D. 2018)   →   ConsenSys
Alan Leung (Ph. D. 2017)   →   Microsoft
Daniel Ricketts (Ph. D. 2017)   →   Oracle
Stephen Foster (Ph. D. 2015, co-advised with Bill Griswold)   →   CEO of ThoughtStem
Samantha Wood (M. S. 2015, co-advised with Bill Griswold)
Zachary Tatlock (Ph. D. 2014)   →   Assistant Professor at University of Washington
Dongseok Jang (Ph. D. 2014)   →   Google
Ross Tate (Ph. D. 2012)   →   Assistant Professor at Cornell
Mike Stepp (Ph. D. 2011)   →   Google
Jeffrey A. Meister (M.S. 2011, co-advised with Ranjit Jhala)   →   MyLife
Sudipta Kundu (Ph. D. 2009, co-advised with Rajesh Gupta)   →   Synopsis
Macneil Shonle (Ph. D. 2009, co-advised with Bill Griswold)   →   The University of Texas at San Antonio, then Google
Jan Wen Voung (Ph. D. 2009, co-advised with Ranjit Jhala)   →   Google

Data-Driven Lemma Synthesis for Interactive Proofs (OOPSLA 2022)
    with Aishwarya Sivaraman, Alex Sanchez-Stern, Bretton Chen, Todd Millstein.

Investigating the Impact of Using a Live Programming Environment in a CS1 Course (SIGCSE 2022)
    with Ruanqianqian (Lisa) Huang, Kasra Ferdowsifard, Ana Selvaraj, and Adalbert Gerald Soosai Raj.

LooPy: Interactive Program Synthesis with Control Structures (OOPSLA 2021)
    with Kasra Ferdowsifard, Shraddha Barke, Hila Peleg and Nadia Polikarpova.

Synthesis of Web Layouts from Examples (FSE 2021)
    with John Sarracino, Dylan Lukes, Cora Coleman, Hila Peleg, and Nadia Polikarpova.

Scooter & Sidecar: A Domain-Specific Approach to Writing Secure Database Migrations (PLDI 2021)
    with John Renner, Alex Sanchez-Stern, Fraser Brown, and Deian Stefan.

Доверя́й, но проверя́й: SFI safety for native-compiled Wasm (NDSS 2021)
    with Evan Johnson, David Thien, Yousef Alhessi, Shravan Narayan, Fraser Brown, Tyler McMullen, Stefan Savage, and Deian Stefan.

A Computational Stack for Cross-Domain Acceleration (HPCA 2021)
    with Sean Kinzer, Joon Kyung Kim, Soroush Ghodrati, Brahmendra Yatham, Alric Althoff, Divya Mahajan, and Hadi Esmailzadeh

Focused Live Programming with Loop Seeds (UIST 2020)
    Sorin Lerner.

Gamification to Aid the Learning of Test Coverage Concepts (Conference on Software Engineering Education & Training 2020)
    with Eman Sherif, Andy Liu, Brian Nguyen and William G. Griswold.

Small-Step Live Programming by Example (UIST 2020)
    with Kasra Ferdowsifard, Allen Ordookhanians, Hila Peleg and Nadia Polikarpova.

Retrofitting Fine Grain Isolation in the Firefox Renderer (USENIX Security 2020)
    with Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Hovav Shacham, and Deian Stefan
    [arXiv | Site | UCSD Press release | Mozilla Blog Post ]

Towards a verified range analysis for JavaScript JITs (PLDI 2020)
    with Fraser Brown, John Renner, Andres Nöetzli, Hovav Shacham, and Deian Stefan.

Generating Correctness Proofs with Neural Networks (MAPL 2020)
    with Alex Sanchez-Stern, Yousef Alhessi, and Lawrence Saul.

Projection Boxes: On-the-fly Reconfigurable Visualization for Live Programming (CHI 2020)
    Sorin Lerner.

REPLica: REPL Instrumentation for Coq Analysis (CPP 2020)
    with Talia Ringer, Alex Sanchez-Stern, and Dan Grossman.

Finding Root Causes of Floating Point Error (PLDI 2018)
    with Alex Sanchez-Stern, Pavel Panchekha, and Zachary Tatlock.

Inferring Loop Invariants through Gamification (CHI 2018)
    with Dimitar Bounov, Anthony DeRossi, Massimiliano Menarini, and William G. Griswold.

Safety verification using barrier certificates with application to double integrator with input saturation and zero-order hold (American Control Conference 2018)
    with A. Ghaffari, I. Abel, D. Ricketts, and M. Krstic.

Dead Store Elimination (Still) Considered Harmful (USENIX Security 2017)
    with Z. Yang, B. Johannesmeyer, A. T. Olesen, and K. Levchenko.

Parsimony: An IDE for Example-Guided Synthesis of Lexers and Parsers (ASE 2017)
    with Alan Leung.

User-Guided Synthesis of Interactive Diagrams (CHI 2017)
    with John Sarracino, Odaris Barrios-Arciga, Jasmine Zhu, Noah Marcus, and Ben Wiedermann.

Modular Deductive Verification of Sampled-Data Systems (EMSOFT 2016)
    with Daniel Ricketts and Gregory Malecha.
    [Veridrone Project]

Towards Foundational Verification of Cyber-physical Systems (SoSCYPS 2016)
    with Gregory Malecha, Daniel Ricketts and Mario M. Alvarez.

Protecting C++ Dynamic Dispatch Through VTable Interleaving (NDSS 2016)
    with Dimitar Bounov and Rami Gökhan Kici.

Formal Verification of Stability Properties of Cyber-physical Systems (CoqPL 2016)
    with Matthew Chan, Daniel Ricketts, and Gregory Malecha.
    [Veridrone Project]

Printing Floating-Point Numbers: An Always Correct Method (POPL 2016)
    with Marc Andrysco and Ranjit Jhala.

Towards Verification of Hybrid Systems in a Foundational Proof Assistant (MEMOCODE 2015)
    with Daniel Ricketts, Gregory Malecha, Mario Alvarez, and Vignesh Gowda.
    [Veridrone Project, Talk]

C-To-Verilog Translation Validation (MEMOCODE 2015)
    with Alan Leung and Dimitar Bounov.

Seamless Integration of Coding and Gameplay: Writing Code Without Knowing it (FDG 2015)
    with Stephen R. Foster and William G. Griswold.

Interactive Parser Synthesis by Example (PLDI 2015)
    with Alan Leung and John Sarracino.

On Subnormal Floating Point and Abnormal Timing (Oakland 2015)
    with Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, and Hovav Shacham.

Polymorphic Blocks: Formalism-Inspired UI for Structured Connectors (CHI 2015)
    with Stephen R. Foster and William G. Griswold.

Automating Formal Proofs for Reactive Systems (PLDI 2014)
    with Daniel Ricketts, Valentin Robert, Dongseok Jang and Zachary Tatlock
    [Project web site for Reflex, including videos of what we built, video of PLDI talk, source code, and working VM image ]

SafeDispatch: Securing C++ Virtual Calls from Memory Corruption Attacks (NDSS 2014)
    with Dongseok Jang and Zachary Tatlock

Establishing Browser Security Guarantees through Formal Shim Verification (USENIX Security 2012)
    with Dongseok Jang and Zachary Tatlock
    [Project web site for Quark browser, including videos of the browser, source code, and working VM image]

Verifying GPU Kernels By Test Amplification (PLDI 2012)
    with Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta and Ranjit Jhala

WitchDoctor: IDE support for real-time auto-completion of refactorings (ICSE 2012)
    with Stephen R. Foster and William G. Griswold

Equality-Based Translation Validator for LLVM (CAV 2011)
    with Michael Stepp and Ross Tate

Taming Wildcards in Java's Type System (PLDI 2011)
    with Ross Tate and Alan Leung

Latent Variable Models for Predicting File Dependencies in Large-Scale Software Development (NIPS 2010)
    with Diane Hu, Laurens van der Maaten, Youngmin Cho, and Lawrence K. Saul

An Empirical Study of Privacy-Violating Information Flows in JavaScript Web Applications (CCS 2010)
    with Dongseok Jang, Ranjit Jhala, and Hovav Shacham

Bringing Extensibility to Verified Compilers (PLDI 2010)
    with Zachary Tatlock

Generating Compiler Optimizations from Proofs (POPL 2010)
    with Ross Tate, and Michael Stepp

Proving Optimizations Correct using Parameterized Program Equivalence (PLDI 2009)
    with Sudipta Kundu, and Zachary Tatlock

Staged Information Flow for JavaScript (PLDI 2009)
    with Ravi Chugh, Jeffrey A. Meister, and Ranjit Jhala

Equality Saturation: a New Approach to Optimization (POPL 2009)
    with Ross Tate, Michael Stepp, and Zachary Tatlock

Addressing Common Crosscutting Problems with Arcum (PASTE 2008)
    with Macneil Shonle and William G. Griswold

When Refactoring Acts like Modularity: Keeping Options Open with Persistent Condition Checking (WRT 2008)
    with Macneil Shonle and William G. Griswold

Deep Typechecking and Refactoring (OOPSLA 2008)
    with Zachary Tatlock, Chris Tucker, David Shuffelton, and Ranjit Jhala

Validating High Level Synthesis (CAV 2008)
    with Sudipta Kundu and Rajesh Gupta

Dataflow Analysis for Concurrent Programs using Datarace Detection (PLDI 2008)
    with Ravi Chugh, Jan Voung, and Ranjit Jhala

Automated Refinement Checking of Concurrent Systems (ICCAD 2007)
    with Sudipta Kundu and Rajesh Gupta

Beyond Refactoring: A Framework for Modular Maintenance of Crosscutting Design Idioms (ESEC/FSE 2007)
    with Macneil Shonle and William G. Griswold

RELAY: Static Race Detection on Millions of Lines of Code (ESEC/FSE 2007)
    with Jan Voung and Ranjit Jhala

Automatic Inference of Optimizer Flow Functions from Semantic Meanings (PLDI 2007)
    with Erika Rice Scherpelz and Craig Chambers

OPIUM: Optimal Package Install/Uninstall Management (ICSE 2007)
    with Chris Tucker, David Shuffelton, and Ranjit Jhala
    Our OPIUM work is being incorporated into Eclipse
    [ announcement 1 | annoucement 2 | more details ]

Automatically Proving the Correctness of Program Analyses and Transformations (PhD dissertation, 2006)
    University of Washington

Automatically Inferring Sound Dataflow Functions from Dataflow Fact Schemas (COCV 2005)
    with Erika Rice and Craig Chambers

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules (POPL 2005)
    with Todd Millstein, Erika Rice, and Craig Chambers
    [ Slides | Tech Report ]

Automatically Proving the Correctness of Compiler Optimizations (PLDI 2003, Best Paper Award)
    with Todd Millstein, and Craig Chambers
    [ Slides | Tech Report ]

Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis (SAS 2002)
    with Stephen Adams, Thomas Ball, Manuvir Das,
    Sriram K. Rajamani, Mark Seigle, and Westley Weimer

ESP: Path-Sensitive Program Verification in Polynomial Time (PLDI 2002)
    with Manuvir Das and Mark Seigle

Combining Dataflow Analyses and Transformations (POPL 2002)
    with David Grove and Craig Chambers
    [ Slides | Tech Report ]