Due Dates

Recent Updates


The purpose of the class project is to familiarize you with the state-of-the-art in compiler technology. There are four different types of projects you can choose:

Regardless of the project type you choose, by end of day Monday, October 5, create a private Piazza post to the instructors containing your proposed topic and group members. In addition, if you choose the research or implementation project, please schedule a brief meeting with Sorin on Friday, October 2 between 3-4 PM Monday, October 5 to propose your topic. Sign up for a time here.


Research Project

Your goal here is to perform original research. You may already have an idea you’ve been brainstorming, or perhaps you can gain inspiration from something in the reading project list.

You must schedule a meeting with Sorin for Friday, October 2 3-4 PM Monday, October 5 to propose your topic. Sign up for a time here.


Implementation Project

Your goal is to re-implement the ideas/algorithms described in an existing body of research. You can look to the reading project list for a ton of possibilities.

You must schedule a meeting with Sorin for Friday, October 2 3-4 PM Monday, October 5 to propose your topic. Sign up for a time here.


Reading Project

We have outlined five broad research areas that could be potential topics for your reading project. Pick one and perform an extensive literature survey of the area. A successful survey is expected to cover 10 papers per student (groups of 2 cover 20 papers, groups of 3 cover 30), so you will need to cover more than just the papers we have listed here. More specifically, each of these lists below is just a starting point. You are expected to follow references and locate other related papers, especially recent work, to fill out your survey.

Compiler Correctness

Automatically Proving the Correctness of Compiler Optimizations
Sorin Lerner, Todd Millstein, and Craig Chambers
PLDI 2003

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules
Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers
POPL 2005

Translation Validation
A. Pnueli , M. Siegel , F. Singerman
TACAS 1998

Translation validation for an optimizing compiler
George C. Necula
PLDI 2000

Proving Optimizations Correct using Parameterized Program Equivalence
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
PLDI 2009

Formal Certification Of A Compiler Back-End, Or: Programming A Compiler With A Proof Assistant
Xavier Leroy
POPL 2006

Bringing Extensibility to Verified Compilers
Zachary Tatlock, Sorin Lerner
PLDI 2010

Formal Verification Of Translation Validators: A Case Study On Instruction Scheduling Optimizations
Jean-Baptiste Tristan, Xavier Leroy
POPL 2008

Volatiles are miscompiled, and what to do about it
Eric Eide, John Regehr
EMSOFT 2008

Finding and Understanding Bugs in C Compilers
Xuejun Yang, Yang Chen, Eric Eide, John Regehr
PLDI 2011

Pointer Analysis

Points-To Analysis In Almost Linear Time
Bjarne Steensgaard
POPL 1996

Unification-Based Pointer Analysis With Directional Assignments
Manuvir Das
PLDI 2000

The Ant And The Grasshopper: Fast And Accurate Pointer Analysis For Millions Of Lines Of Code
Ben Hardekopf, Calvin Lin
PLDI 2007

Separation Logic And Abstraction
Matthew Parkinson, Gavin Bierman
POPL 2005

TVLA: A System for Implementing Static Analyses
Tal Lev-Ami, Shmuel Sagiv
SAS 2000

Ownership Types for Safe Region-Based Memory Management in Real-Time Java
Chandrasekhar Boyapati, Alexandru Salcianu, William Beebee, Jr., Martin Rinard
PLDI 2003

Parametric Shape Analysis Via 3-Valued Logic
Mooly Sagiv, Thomas Reps, Reinhard Wilhelm
POPL 1999

Ultra-fast aliasing analysis using CLA: a million lines of C code in a second
Nevin Heintze, Olivier Tardieu
PLDI 2001

Efficient context-sensitive pointer analysis for C programs
Robert P. Wilson, Monica Lam
PLDI 1995

Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams
John Whaley, Monica Lam
PLDI 2004

Error Detection and Safety Checking for C-level Languages

Checking System Rules Using System Specific, Programmer-Written Compiler Extensions
Dawson Engler, Benjamin Chelf, Andy Chou and Seth Hallem
OSDI 2000

Bugs as Deviant Behavior: A General Approach to Inferring Errors in Systems Code
Dawson Engler, David Yu Chen, Seth Hallem, Andy Chou, and Benjamin Chelf
SOSP 2001

Efficient Detection of All Pointer and Array Access Errors
Todd Austin, Scott Breach, Gurindar Sohi
PLDI 1994

Cyclone: A Safe Dialect of C
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang
USENIX 2002

Region-Based Memory Management in Cyclone
Trevor Jim, Greg Morrisett, Dan Grossman, Michael Hicks, James Cheney, Yanling Wang
PLDI 2002

CCured: Type-Safe Retrofitting of Legacy Code
George Necula, Scott McPeak, Westley Weimer
POPL 2002

Language Support for Regions
David Gay, Alex Aiken
PLDI 2001

Secure Execution Via Program Shepherding
Vladimir Kiriansky, Derek Bruening, Saman Amarasinghe
Usenix Security 2002

Static detection of dynamic memory errors
David Evans
PLDI 1996

Volatiles are miscompiled, and what to do about it
Eric Eide, John Regehr
EMSOFT 2008

A few billion lines of code later: using static analysis to find bugs in the real world
Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, Dawson Engler
CACM 2010

Concurrency: Races, Atomicity, and Error Detection

Eraser: A Dynamic Data Race Detector For Multi-Threaded Programs
Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, Thomas Anderson
SOSP 1997

RELAY: Static Race Detection On Millions Of Lines Of Code
Jan Wen Voung, Ranjit Jhala, Sorin Lerner
FSE 2007

Dataflow Analysis For Concurrent Programs Using Datarace Detection
Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner
PLDI 2008

Effective Static Race Detection For Java
Mayur Naik, Alex Aiken, John Whaley
PLDI 2006

Velodrome: A Sound and Complete Dynamic Atomicity Checker for Multithreaded Programs
Cormac Flanagan, Stephen N. Freund, Jaeheon Yi
PLDI 2008

Adversarial Memory for Detecting Destructive Races
Cormac Flanagan, Stephen N. Freund
PLDI 2010

AtomCaml: First-Class Atomicity Via Rollback
Michael F. Ringenburg, Dan Grossman
ICFP 2005

The Transactional Memory / Garbage Collection Analogy
Dan Grossman
OOPSLA 2007

CoreDet: A Compiler And Runtime System For Deterministic Multithreaded Execution
Tom Bergan, Owen Anderson, Joseph Devietti, Luis Ceze, Dan Grossman
ASPLOS 2010

Language Support for Lightweight Transactions
Tim Harris, Keir Fraser
OOPSLA 2003

Scalable Analysis Techniques

Points-To Analysis In Almost Linear Time
Bjarne Steensgaard
POPL 1996

Unification-Based Pointer Analysis With Directional Assignments
Manuvir Das
PLDI 2000

ESP: Path-Sensitive Program Verification In Polynomial Time
Manuvir Das, Sorin Lerner, Mark Seigle
PLDI 2002

Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary Decision Diagrams
John Whaley, Monica Lam
PLDI 2004

Saturn: A Scalable Framework For Error Detection Using Boolean Satisfiability
Yichen Xie, Alex Aiken
POPL 2005

Using Datalog with Binary Decision Diagrams for Program Analysis
John Whaley, Dzintars Avots, Michael Carbin, Monica S. Lam
APLAS 2005

Fast liveness checking for ssa-form programs
Benoit Boissinot, Sebastian Hack, Daniel Grund, Benoit Dupont, Fabri e Rastello
CGO 2008

RELAY: Static Race Detection On Millions Of Lines Of Code
Jan Wen Voung, Ranjit Jhala, Sorin Lerner
FSE 2007

Dataflow Analysis For Concurrent Programs Using Datarace Detection
Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner
PLDI 2008

Making Context-Sensitive Points-to Analysis with Heap Cloning Practical For The Real World
Chris Lattner, Andrew Lenharth, and Vikram Adve
PLDI 2007


Predefined Project

If none of the other options suit you, we also have a default project for you to work on.