Sorin Lerner

Professor and Chair, CSE @ UCSD Office: EBU3B 3116
I develop Programming Language techniques and apply them to various domains, including program verification, security/privacy, and HCI. I am always looking for great grad students and post-docs to join our group.

Current Work

CSE Pixel Art Competition: Inaugural CSE Department Pixel Art Competition!
Projection Boxes: Visualization for Live Programming
Browser and Web Security: Making web platforms safe
Proverbot: Finding Proofs with Machine Learning
Polymorphic Blocks: Block-based UI for proofs/types
Proof Games: Crowdsourcing proofs via gamification
Attending GHC: UCSD presence at Grace Hopper

Previous Work

While the projects below are mostly wrapped up, they give you a flavor for the kind of research I'm interested in.

Collider Collider: Correct opts from high-level specifications
Radar Radar: Concurrent analyses from sequential ones
Quail Quail: Deep Typechecking & Refactoring
Arcum Arcum: Crosscutting design idioms, made modular
CodeSpells Code Spells: Game that teaches coding
Reflex Reflex: Verification of reactive systems in Coq
Quark Quark: Practical web browser verified in Coq
Javascript Javascript: Analysis for Javascript security
TV-HLS TV-HLS: Verification for High-Level Synthesis
Parsimony Parsimony: Construct parsers by example
Parsimony Eddie: Synthesize interactive diagrams
VD VeriDrone: Verification of Cyber-physical Systems


Kasra Ferdowsi (Ph. D. student, started 2021)
Ruanqianqian (Lisa) Huang (Ph. D. student, started 2020)
David Thien (Ph. D. student, co-advised with Deian Stefan, started 2019)
Yousef Alhessi (Ph. D. student, started 2018)

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


CSE 8A: Introduction to Programming
CSE 130: Undergraduate Programming Languages
CSE 231: Graduate Compilers
CSE 230: Graduate Programming Languages

CSE 291: Applied Automated Theorem Proving
CSE 291: Power and Programming Languages
CSE 291: Software Reliability Methods


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 ]