Sorin Lerner

Professor and Vice-Chair, CSE @ UCSD Office: EBU3B 3116
email: lerner@cs.ucsd.edu
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

VD
VeriDrone: Verification of Cyber-physical Systems
PB
Polymorphic Blocks: Block-based UI for proofs/types
PB
Proof Games: Crowdsourcing proofs via gamification
PB
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

Students

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


Teaching

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


Papers

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

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