Skip to Content

Programming Systems - Publications Archive

Export / Filter

2010

An Empirical Study of Privacy-Violating Information Flows in JavaScript Web Applications, Dongseok Jang, Ranjit Jhala, Sorin Lerner, and Hovav Shacham, CCS, (2010). PDF
Bringing Extensibility to Verified Compilers, Zachary Tatlock, and Sorin Lerner, PLDI, (2010). PDF
Dsolve: Safety Verification Using Liquid Types, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, CAV, (2010). PDF
Enforcing Stateful Authorization and Information Flow Policies in Fine, Nikhil Swamy, Juan Chen, and Ravi Chugh, ESOP, (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
Generating Compiler Optimizations from Proofs, Ross Tate, Michael Stepp, and Sorin Lerner, POPL, (2010). PDF
Inferable Object-Oriented Typed Assembly Language, Ross Tate, Juan Chen, and Chris Hawblitzel, PLDI, (2010). PDF
Low-level Liquid Types, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, POPL, (2010). PDF
Type-preserving Compilation for End-to-end Verification of Security Enforcement, Juan Chen, Ravi Chugh, and Nikhil Swamy, PLDI, (2010). PDF

2009

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
Staged Information Flow for Javascript, Ravi Chugh, Jeff Meister, Ranjit Jhala, and Sorin Lerner, PLDI, (2009). PDF
Type-based Data Structure Verification, Patrick Rondon, Ming Kawaguchi, and Ranjit Jhala, PLDI, (2009). PDF
Verifying Reference Counting Implementations, Michael Emmi, Ranjit Jhala, Rupak Majumdar, and Eddie Kohler, TACAS, (2009). PDF

2008

Addressing Common Crosscutting Problems with Arcum, Macneil Shonle, Sorin Lerner, and William Griswold, PASTE, (2008).
Dataflow Analysis For Concurrent Programs using Datarace Detection, Ravi Chugh, Jan Voung, Ranjit Jhala, and Sorin Lerner, PLDI, (2008). PDF
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). PDF
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). PDF
Automated Refinement Checking of Concurrent Systems, Sudipta Kundu, Sorin Lerner, and Rajesh Gupta, ICCAD, (2007). PDF
Automatic Inference of Optimizer Flow Functions from Semantic Meanings, Erika Rice, Sorin Lerner, and Craig Chambers, PLDI, (2007). PDF
Interprocedural Analysis of Asynchronous Programs, Ranjit Jhala, and Rupak Majumdar, POPL, (2007). PDF
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] PDF
Lock Allocation, Michael Emmi, Jeffrey Fischer, Ranjit Jhala, and Rupak Majumdar, POPL, (2007). PDF
Mace: Language Support for Building Distributed Systems, Charles Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, and Amin Vahdat, PLDI, (2007). PDF
OPIUM: Optimum Package Install/Uninstall Manager, Chris Tucker, David Shuffelton, Ranjit Jhala, and Sorin Lerner, ICSE, (2007). PDF
State of the Union: Type Inference via Craig Interpolation, Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu, TACAS, (2007). PDF

2006

A Practical and Complete Approach to Predicate Refinement, Ranjit Jhala, and Kenneth L. McMillan, TACAS, (2006). PDF
Bit-level Types for High-level Reasoning, Ranjit Jhala, and Rupak Majumdar, FSE, (2006). PDF
Structural Invariants, Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu, SAS, (2006). PDF

2005

Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules, Sorin Lerner, Todd Millstein, Erika Rice, and Craig Chambers, POPL, (2005).
application/pdf iconrhodium_popl_05.pdf
Automatically Inferring Sound Dataflow Functions from Dataflow Fact Schemas, Erika Rice, Sorin Lerner, and Craig Chambers, COCV, (2005).
application/pdf iconrhodium_cocv_05.pdf
Checking Memory Safety with Blast, Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, FASE, (2005).
Interpolant-based transition relation approximation, Ranjit Jhala, and Kenneth L. McMillan, CAV, (2005). PDF
Joining Dataflow with Predicates, Jeffrey Fischer, Ranjit Jhala, and Rupak Majumdar, FSE, (2005). PDF
Permissive Interfaces, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, FSE, (2005). PDF

2004

Abstractions from Proofs, T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan, POPL, (2004). PDF
Automatically Proving the Correctness of Compiler Transformations, Sorin Lerner, Todd Millstein, and Craig Chambers, PLDI, (2004). [Best paper]
application/pdf iconcobalt_pldi_03.pdf
Generating Tests from Counterexamples, Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, ICSE, (2004). PDF
Race Checking by Context Inference, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, PLDI, (2004). PDF
The Blast Query Language for Software Verification, Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar, SAS, (2004).

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). PDF

2002

Composing Dataflow Analyses and Transformations, Sorin Lerner, David Grove, and Craig Chambers, POPL, (2002).
application/pdf icondataflow_popl_02.pdf
ESP: Path-Sensitive Program Verification in Polynomial Time, Manuvir Das, Sorin Lerner, and Mark Seigle, PLDI, (2002).
application/pdf iconesp_pldi_02.pdf
Lazy abstraction, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre, POPL, (2002). PDF
Temporal-safety proofs for systems code, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George Necula, Gregoire Sutre, and Westley Weimer, CAV, (2002). PDF

2001

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


by Dr. Radut.