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