Programming Systems Publications
     
 
Programming Systems Publications
│ 2014 │ 2013 │ 2012 │ 2011 │ 2010 │ 2009 │ 2008 │ 2007 │ 2006 │ 2005 │ 2004 │ 2003 │ 2002 │ 2001 │ 
 
     
 

2014

Automating Formal Proofs for Reactive Systems, Daniel Ricketts, Valentin Robert, Donseok Jang, Zachary Tatlock, and Sorin Lerner, PLDI, 2014.

SafeDispatch: Securing C++ Virtual Calls from Memory Corruption, Dongseok Jang, Zachary Tatlock, and Sorin Lerner, NDSS, 2014.

 
     
 

2013

Abstract Refinement Types, Niki Vazou, Patrick Rondon, and Ranjit Jhala, ESOP, 2013.

 
     
 

2012

Dependent Types For JavaScript, Ravi Chugh, David Herman, and Ranjit Jhala, OOPSLA, 2012.

CSolve: Verifying C With Liquid Types, Patrick Rondon, Ming Kawaguchi, Alexander Bakst, and Ranjit Jhala, CAV, 2012.

Deterministic Parallelism via Liquid Effects, Patrick Rondon, Ming Kawaguchi, Alexander Bakst, and Ranjit Jhala, PLDI, 2012.

Verifying GPU Kernels By Test Amplification, Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, and Sorin Lerner, PLDI, 2012.

Nested Refinements: A Logic For Duck Typing, Ravi Chugh, Patrick Rondon, and Ranjit Jhala, POPL, 2012.

WitchDoctor: IDE support for real-time auto-completion of refactorings, Stephen Foster, William Griswold, and Sorin Lerner, ICSE, 2012.

Establishing Browser Security Guarantees through Formal Shim Verification, Donseok Jang, Zachary Tatlock, and Sorin Lerner, USENIX Security, 2012.

 
     
 

2011

HMC: Verifying Functional Programs With Abstract Interpreters, Ranjit Jhala, Rupak Majumdar, and Andrey Rybalchenko, CAV, 2011.

NV-Heaps: Making Persistent Objects Fast and Safe with Next-Generation, Non-Volatile Memories , Joel Coburn, Adrian Caulfield, Ameen Akel, Laura Grupp, Ranjit Jhala, Rajesh Gupta, and Steven Swanson, ASPLOS, 2011.

Equality-Based Translation Validator for LLVM, Michael Stepp, Ross Tate, and Sorin Lerner, CAV, 2011.

Taming Wildcards in Java's Type System, Ross Tate, Alan Leung, and Sorin Lerner, PLDI, 2011.

 
     
 

2010

Latent Variable Models for Predicting File Dependencies in Large-Scale Software Development, Diane Hu, Laurens van der Maaten, Youngmin Cho, Lawrence K. Saul, and Sorin Lerner, NIPS, 2010.

An Empirical Study of Privacy-Violating Information Flows in JavaScript Web Applications, Dongseok Jang, Ranjit Jhala, Sorin Lerner, and Hovav Shacham, CCS, 2010.

Finding Latent Performance Bugs in Systems Implementations, Charles Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud, James Anderson, and Ranjit Jhala, FSE, 2010.

Software Data Spreading: Leveraging Distributed Caches in Multicore Systems to Improve Single Thread Performance, Md Kamruzzaman, Steve Swanson, and Dean Tullsen, PLDI, 2010.

Inferable Object-Oriented Typed Assembly Language, Ross Tate, Juan Chen, and Chris Hawblitzel, PLDI, 2010.

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

Type-preserving Compilation for End-to-end Verification of Security Enforcement, Juan Chen, Ravi Chugh, and Nikhil Swamy, PLDI, 2010.

Dsolve: Safety Verification Using Liquid Types, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, CAV, 2010.

Enforcing Stateful Authorization and Information Flow Policies in Fine, Nikhil Swamy, Juan Chen, and Ravi Chugh, ESOP, 2010.

Low-level Liquid Types, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, POPL, 2010.

Generating Compiler Optimizations from Proofs, Ross Tate, Michael Stepp, and Sorin Lerner, POPL, 2010.

 
     
 

2009

Staged Information Flow for Javascript, Ravi Chugh, Jeff Meister, Ranjit Jhala, and Sorin Lerner, PLDI, 2009.

Type-based Data Structure Verification, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, PLDI, 2009.

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

Equality Saturation: A New Approach to Optimization, Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner, POPL, 2009.

Verifying Reference Counting Implementations, Michael Emmi, Ranjit Jhala, Rupak Majumdar, and Eddie Kohler, TACAS, 2009.

 
     
 

2008

Addressing Common Crosscutting Problems with Arcum, Macneil Shonle, Sorin Lerner, and William Griswold, PASTE, 2008.

Deep Typechecking and Refactoring, Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, and Sorin Lerner, OOPSLA, 2008.

Liquid Types, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, PLDI, 2008.

Dataflow Analysis For Concurrent Programs using Datarace Detection, Ravi Chugh, Jan Voung, Ranjit Jhala, and Sorin Lerner, PLDI, 2008.

Validating High Level Synthesis, Sudipta Kundu, Sorin Lerner, and Rajesh Gupta, CAV, 2008.

 
     
 

2007

Array Abstractions from Proofs, Ranjit Jhala and Kenneth L. McMillan, CAV, 2007.

Lock Allocation, Michael Emmi, Jeffrey Fischer, Ranjit Jhala, and Rupak Majumdar, POPL, 2007.

Interprocedural Analysis of Asynchronous Programs, Ranjit Jhala and Rupak Majumdar, POPL, 2007.

State of the Union: Type Inference via Craig Interpolation, Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu, TACAS, 2007.

Automatic Inference of Optimizer Flow Functions from Semantic Meanings, Erika Rice, Sorin Lerner, and Craig Chambers, PLDI, 2007.

Mace: Language Support for Building Distributed Systems, Charles Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, and Amin Vahdat, PLDI, 2007.

Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code, Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat, NSDI, 2007. (Best paper).

OPIUM: Optimum Package Install/Uninstall Manager, Chris Tucker, David Shuffelton, Ranjit Jhala, and Sorin Lerner, ICSE, 2007.

Automated Refinement Checking of Concurrent Systems, Sudipta Kundu, Sorin Lerner, and Rajesh Gupta, ICCAD, 2007.

 
     
 

2006

A Practical and Complete Approach to Predicate Refinement, Ranjit Jhala and Kenneth L. McMillan, TACAS, 2006.

Bit-level Types for High-level Reasoning, Ranjit Jhala and Rupak Majumdar, FSE, 2006.

Structural Invariants, Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu, SAS, 2006.

 
     
 

2005

Interpolant-based transition relation approximation, Ranjit Jhala and Kenneth L. McMillan, CAV, 2005.

Automatically Inferring Sound Dataflow Functions from Dataflow Fact Schemas, Erika Rice, Sorin Lerner, and Craig Chambers, COCV, 2005.

Joining Dataflow with Predicates, Jeffrey Fischer, Ranjit Jhala, and Rupak Majumdar, FSE, 2005.

Checking Memory Safety with Blast, Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, FASE, 2005.

Permissive Interfaces, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, FSE, 2005.

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

 
     
 

2004

Abstractions from Proofs, T.A. Henzinger, R. Jhala, R. Majumdar, and K.L. McMillan, POPL, 2004.

Race Checking by Context Inference, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, PLDI, 2004.

Generating Tests from Counterexamples, Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, ICSE, 2004.

The Blast Query Language for Software Verification, Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, SAS, 2004.

Automatically Proving the Correctness of Compiler Transformations, Sorin Lerner, Todd Millstein, and Craig Chambers, PLDI, 2004. (Best paper).

 
     
 

2003

Software Verification with BLAST, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Grégoire Sutre, SPIN, 2003.

Thread-modular abstraction refinement, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer, CAV, 2003.

 
     
 

2002

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

Lazy abstraction, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre, POPL, 2002.

Composing Dataflow Analyses and Transformations, Sorin Lerner, David Grove, and Craig Chambers, POPL, 2002.

Temporal-safety proofs for systems code, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George Necula, Gregoire Sutre, and Westley Weimer, CAV, 2002.

 
     
 

2001

Microarchitecture Verification by Compositional Model Checking, Ranjit Jhala and Kenneth L. McMillan, CAV, 2001.