Skip to Content

Programming Systems

The Programming Systems Group in the Department of Computer Science and Engineering at the University of California, San Diego is interested in developing new languages, compilers, program analysis techniques and development environments for making software systems easier to build, maintain and understand.

People

Publications

Projects

Courses

People

Core Faculty

Affiliated Faculty

PhD Students

Recent alumni

News

(02/04/11) UCSD grad students and faculty on three PLDI 2011 papers. Awesome job everybody!
(12/02/10) Our JavaScript work, published at CCS 2010, is getting a fair bit of press coverage: Forbes, The Wall Street Journal, Associated Press, The BBC, The Register, PC World, The Telegraph, Network World, TechDirt, Technology Review, MediaPost, The Huffington Post, Slashdot, Jamie Zawinski’s blog, Boing Boing, and UCSD's own press release.
(02/12/10) UCSD has four papers accepted to PLDI 2010. Congrats to all!
(10/05/09) The UCSD Programming Systems group has two papers accepted to POPL 2010. Congrats to all!
(08/15/09) Macneil Shonle has graduated and will start as an Assistant Professor at UT San Antonio. Awesome job Macneil!
(08/01/09) Sudipta Kundu did a fantastic job at defending his thesis. He is going to join Synopsis. Congrats Sudipta!
(02/03/09) Ross Tate has received a Microsoft Research Fellowship. Congratulations Ross!
(01/27/09) The UCSD Programming Systems group has three papers accepted to PLDI 2009. Congrats to all!

Recent Publications

Generating Compiler Optimizations from Proofs, Ross Tate, Michael Stepp, and Sorin Lerner, POPL, (2010). PDF
Low-level Liquid Types, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, POPL, (2010). PDF
Enforcing Stateful Authorization and Information Flow Policies in Fine, Nikhil Swamy, Juan Chen, and Ravi Chugh, ESOP, (2010). PDF
Dsolve: Safety Verification Using Liquid Types, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, CAV, (2010). PDF
Type-preserving Compilation for End-to-end Verification of Security Enforcement, Juan Chen, Ravi Chugh, and Nikhil Swamy, PLDI, (2010). PDF
Bringing Extensibility to Verified Compilers, Zachary Tatlock, and Sorin Lerner, PLDI, (2010). PDF
Inferable Object-Oriented Typed Assembly Language, Ross Tate, Juan Chen, and Chris Hawblitzel, PLDI, (2010). PDF
Finding Latent Performance Bugs in Systems Implementations, Charles Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud, James Anderson, and Ranjit Jhala, FSE, (2010). PDF
An Empirical Study of Privacy-Violating Information Flows in JavaScript Web Applications, Dongseok Jang, Ranjit Jhala, Sorin Lerner, and Hovav Shacham, CCS, (2010). PDF
Verifying Reference Counting Implementations, Michael Emmi, Ranjit Jhala, Rupak Majumdar, and Eddie Kohler, TACAS, (2009). PDF
Equality Saturation: A New Approach to Optimization, Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner, POPL, (2009). PDF
Proving Optimizations Correct using Parameterized Program Equivalence, Zachary Tatlock, Sudipta Kundu, and Sorin Lerner, PLDI, (2009). PDF
Type-based Data Structure Verification, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, PLDI, (2009). PDF
Staged Information Flow for Javascript, Ravi Chugh, Jeff Meister, Ranjit Jhala, and Sorin Lerner, PLDI, (2009). PDF
Validating High Level Synthesis, Sudipta Kundu, Sorin Lerner, and Rajesh Gupta, CAV, (2008).

[Publications Archive]

Projects

Arccos

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, which consists of showing, for each translation that the HLS tool performs, that the output program produced by the tool has the same behavior as the original program. [read more...]
Arcum

Arcum

Arcum is an extension to the refactoring paradigm that provides for the modular maintenance of crosscutting design idioms, supporting both substitutability of design idiom implementations and the checking of essential constraints. [read more...]
Collider

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

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

Liquid Types

Liquid Types is a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties. [read more...]
Radar

Radar

The Radar project aims to automatically generate precise and scalable concurrent analyses from their sequential counterparts, thereby making concurrent analyses much easier to write, and allowing compiler writers and analysis writers to easily adapt current analyses to account for concurrency. [read more...]
Javascript Security

Javascript Security

The goal of this project is to use program analysis techniques to improve the reliability and security of Javascript code.

Courses

Annual Courses

The following core courses are regularly offered each academic year.

Topics Courses

Several topics courses are also offered on a less regular basis.



by Dr. Radut.