CSE 231: Advanced Compilers

Reading Lists


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