Sorin Lerner

Associate Professor
Computer Science and Engineering
University of California, San Diego
Office: EBU3B 3116
email: my last name at cs.ucsd.edu
phone: 858-534-8883


Here is a list of the projects I'm actively involved in. The common theme is that I like to develop Programming Language techniques and apply them to a wide range of interesting domains, for example program verification, hardware design, security/privacy, and teaching environments. I am always looking for great grad students and post-docs to join our group.

Quark Reflex

Automated verification of reactive systems in Coq [Quick links: Paper, Talk, Browser-video, SSH-video]

Quark Quark

A practical web browser that has been formally verified in Coq [Quick links: Paper, Quark-video, Another one]

Javascript Javascript

Program analysis for Javascript security [Quick links: History Sniffing Paper, Media Coverage]

TV-HLS TV-HLS

Translation Validation for High-Level Synthesis

Variability Variability

Handling the variability in future hardware platforms

CodeSpells Code Spells

Learn how to program by crafting your own magic spells


Collider Collider

Correct optimizations from high-level specifications

Radar Radar

Generate concurrent analyses from sequential counterparts

Quail Quail

Typechecking/Refactoring for the Java Persistence API

Arcum Arcum

Modular maintenance of crosscutting design idioms



Marc Andrysco (Ph. D. student, started 2013)

Valentin Robert (Ph. D. student, started 2012)

Samantha Wood (Ph. D. student, started 2011, co-advised with Bill Griswold)

Dimitar Bounov (Ph. D. student, started 2011)

Daniel Ricketts (Ph. D. student, started 2010)

Stephen Foster (Ph. D. student, started 2010, co-advised with Bill Griswold)

Alan Leung (Ph. D. student, started 2010)


Zachary Tatlock     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)     MyLife

Sudipta Kundu (Ph. D. 2009)     Synopsis

Macneil Shonle (Ph. D. 2009)     The University of Texas at San Antonio, then Google

Jan Wen Voung (Ph. D. 2009)     Google



CSE 130: Undergraduate Programming Languages
CSE 231: Graduate Compilers
CSE 291: Applied Automated Theorem Proving


CSE 291: Power and Programming Languages
CSE 291: Software Reliability Methods


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 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 ]