Sorin Lerner

Assistant Professor
Department of Computer Science and Engineering
University of California, San Diego
9500 Gilman Drive, Mail Code 0404, La Jolla, CA 92093-0404

Office: EBU3B 3116
email: my last name at cs.ucsd.edu
phone: 858-534-8883

My research interests lie in programming language and analysis techniques for making software systems easier to write, maintain and understand, including static program analysis, domain specific languages, compilation, formal methods and automated theorem proving. I am a member of the UCSD Programming Systems Group.

Teaching

Fall 2009: CSE 231 Advanced Compilers
Spring 2009: CSE 291 Seminar on Power and Programming Languages
Winter 2009: CSE 130 Programming Languages
Previous quarters

Research

	Collider The Collider project investigates techniques for automatically generating efficient, scalable, correct, and precise dataflow analyzers and optimizers from a very high-level specification. [read more...]
	Radar The Radar project aims to automatically generate precise and scalable concurrent analyses from their sequential counterparts. [read more...]
	Quail The goal of the Quail project is to develop techniques for deep typechecking and refactoring for systems that combine Java code with a database back-end using the Java Persistence API. [read more...]
	Arccos The goal of this project is to provide strong guarantees about the High-Level Sythesis process (HLS). As a starting point, we are exploring the idea of performing translation validation for HLS. [read more...]
	Arcum Arcum is an extension to the refactoring paradigm that provides for the modular maintenance of crosscutting design idioms. [read more...]

Publications

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 ]

Students

Students who have graduated

Sudipta Kundu (Ph. D. 2009) → Synopsis
Macneil Shonle (Ph. D. 2009) → The University of Texas at San Antonio