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