Sorin Lerner

Computer Science and Engineering
University of California, San Diego
Office: EBU3B 3116
email: my last name at
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.

PB VeriDrone

Foundational Verification of Cyber-physical Systems

PB Polymorphic Blocks

Novel block-based UI for visualizing proofs and types

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]


Translation Validation for High-Level Synthesis

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

CodeSpells Code Spells

Learn how to program by crafting your own magic spells

Alex Sanchez-Stern (Ph. D. student, started 2016)

John Sarracino (Ph. D. student, started 2014)

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

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

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

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: A Faster, 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 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 ]