Ranjit Jhala
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
70
Venues
26
Active years
2001–2026
Best venue rank
A*
Where they publish
- A*PLDI13 papers
- A*CAV10 papers
- A*POPL7 papers
- AESOP3 papers
- A*ICSE3 papers
- A*CCS3 papers
- AICFP3 papers
- ATACAS3 papers
- A*SOSP2 papers
- AECOOP2 papers
- A*OSDI2 papers
- A*SP2 papers
- BVMCAI2 papers
- AOOPSLA2 papers
- BSAS2 papers
- ASIGCSE1 paper
- CHASKELL1 paper
- BAPLAS1 paper
- A*ASPLOS1 paper
- NationalNSDI1 paper
- BFASE1 paper
- AUAI1 paper
- CPEPM1 paper
- CPPDP1 paper
- A*ICALP1 paper
- BCONCUR1 paper
Papers
70 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | ESOP | Auditing Rust Crates Effectively. | Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford |
| 2025 | ICSE | Neurosymbolic Modular Refinement Type Inference. | Georgios Sakkas, Pratyush Sahu, Kyeling Ong, Ranjit Jhala |
| 2025 | SOSP | TickTock: Verified Isolation in a Production Embedded OS. | Vivien Rindisbacher, Evan Johnson, Nico Lehmann, Tyler Potyondy, Pat Pannuto, Stefan Savage, Deian Stefan, Ranjit Jhala |
| 2024 | SOSP | Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution. | Naomi Smith, Abhishek Sharma, John Renner, David Thien, Fraser Brown, Hovav Shacham, Ranjit Jhala, Deian Stefan |
| 2021 | CCS | Solver-Aided Constant-Time Hardware Verification. | Klaus von Gleissenthall, Rami Gkhan Kici, Deian Stefan, Ranjit Jhala |
| 2021 | ECOOP | Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types. | Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala |
| 2021 | OSDI | STORM: Refinement Types for Secure Web Applications. | Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala |
| 2020 | CAV | Stratified Abstraction of Access Control Policies. | John Backes, Ulises Berrueco, Tyler Bray, Daniel Brim, Byron Cook, Andrew Gacek, Ranjit Jhala, Kasper Se Luckow, Sean McLaughlin, Madhav Menon, Daniel Peebles, Ujjwal Pugalia, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan |
| 2020 | PLDI | Type error feedback via analytic program repair. | Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, Ranjit Jhala |
| 2020 | SIGCSE | PABLO: Helping Novices Debug Python Code Through Data-Driven Fault Localization. | Benjamin Cosman, Madeline Endres, Georgios Sakkas, Leon Medvinsky, Yao-Yuan Yang, Ranjit Jhala, Kamalika Chaudhuri, Westley Weimer |
| 2019 | PLDI | FaCT: a DSL for timing-sensitive computation. | Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grgoire, Gilles Barthe, Ranjit Jhala, Deian Stefan |
| 2019 | PLDI | Lazy counterfactual symbolic execution. | William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, Ruzica Piskac |
| 2018 | CCS | Towards Verified, Constant-time Floating Point Operations. | Marc Andrysco, Andres Ntzli, Fraser Brown, Ranjit Jhala, Deian Stefan |
| 2017 | SP | Finding and Preventing Bugs in JavaScript Bindings. | Fraser Brown, Shravan Narayan, Riad S. Wahby, Dawson R. Engler, Ranjit Jhala, Deian Stefan |
| 2016 | ICFP | Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong). | Eric L. Seidel, Ranjit Jhala, Westley Weimer |
| 2016 | PLDI | Refinement types for TypeScript. | Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala |
| 2016 | POPL | Printing floating-point numbers: a faster, always correct method. | Marc Andrysco, Ranjit Jhala, Sorin Lerner |
| 2016 | VMCAI | Predicate Abstraction for Linked Data Structures. | Alexander Bakst, Ranjit Jhala |
| 2015 | ECOOP | Trust, but Verify: Two-Phase Typing for Dynamic Languages. | Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala |
| 2015 | ESOP | Type Targeted Testing. | Eric L. Seidel, Niki Vazou, Ranjit Jhala |
| 2015 | ICFP | Bounded refinement types. | Niki Vazou, Alexander Bakst, Ranjit Jhala |
| 2015 | SP | On Subnormal Floating Point and Abnormal Timing. | Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, Hovav Shacham |
| 2014 | HASKELL | LiquidHaskell: experience with refinement types in the real world. | Niki Vazou, Eric L. Seidel, Ranjit Jhala |
| 2014 | ICFP | Refinement types for Haskell. | Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon L. Peyton Jones |
| 2013 | ESOP | Abstract Refinement Types. | Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala |
| 2012 | CAV | CSolve: Verifying C with Liquid Types. | Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala |
| 2012 | OOPSLA | Dependent types for JavaScript. | Ravi Chugh, David Herman, Ranjit Jhala |
| 2012 | OSDI | Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs. | Panagiotis Vekris, Ranjit Jhala, Sorin Lerner, Yuvraj Agarwal |
| 2012 | PLDI | Deterministic parallelism via liquid effects. | Ming Kawaguchi, Patrick Maxim Rondon, Alexander Bakst, Ranjit Jhala |
| 2012 | PLDI | Verifying GPU kernels by test amplification. | Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner |
| 2012 | POPL | Nested refinements: a logic for duck typing. | Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala |
| 2012 | VMCAI | Software Verification with Liquid Types. | Ranjit Jhala |
| 2011 | APLAS | Software Verification with Liquid Types. | Ranjit Jhala |
| 2011 | ASPLOS | NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories. | Joel Coburn, Adrian M. Caulfield, Ameen Akel, Laura M. Grupp, Rajesh K. Gupta, Ranjit Jhala, Steven Swanson |
| 2011 | CAV | Using Types for Software Verification. | Ranjit Jhala |
| 2011 | CAV | HMC: Verifying Functional Programs Using Abstract Interpreters. | Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko |
| 2010 | CAV | Dsolve: Safety Verification via Liquid Types. | Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala |
| 2010 | CCS | An empirical study of privacy-violating information flows in JavaScript web applications. | Dongseok Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham |
| 2010 | POPL | Low-level liquid types. | Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala |
| 2009 | PLDI | Staged information flow for javascript. | Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner |
| 2009 | PLDI | Type-based data structure verification. | Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala |
| 2009 | TACAS | Verifying Reference Counting Implementations. | Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar |
| 2008 | OOPSLA | Deep typechecking and refactoring. | Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner |
| 2008 | PLDI | Dataflow analysis for concurrent programs using datarace detection. | Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner |
| 2008 | PLDI | Liquid types. | Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala |
| 2007 | CAV | Array Abstractions from Proofs. | Ranjit Jhala, Kenneth L. McMillan |
| 2007 | ICSE | OPIUM: Optimal Package Install/Uninstall Manager. | Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner |
| 2007 | NSDI | Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (Awarded Best Paper). | Charles Killian, James W. Anderson, Ranjit Jhala, Amin Vahdat |
| 2007 | PLDI | Mace: language support for building distributed systems. | Charles Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat |
| 2007 | POPL | Lock allocation. | Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Rupak Majumdar |
| 2007 | POPL | Interprocedural analysis of asynchronous programs. | Ranjit Jhala, Rupak Majumdar |
| 2007 | TACAS | State of the Union: Type Inference Via Craig Interpolation. | Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu |
| 2006 | SAS | Structural Invariants. | Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu |
| 2006 | TACAS | A Practical and Complete Approach to Predicate Refinement. | Ranjit Jhala, Kenneth L. McMillan |
| 2005 | CAV | Interpolant-Based Transition Relation Approximation. | Ranjit Jhala, Kenneth L. McMillan |
| 2005 | FASE | Checking Memory Safety with Blast. | Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2005 | PLDI | Path slicing. | Ranjit Jhala, Rupak Majumdar |
| 2005 | UAI | Counterexample-guided Planning. | Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | ICSE | Generating Tests from Counterexamples. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | PEPM | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | PLDI | Race checking by context inference. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | POPL | Abstractions from proofs. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan |
| 2004 | PPDP | Invited talk: the blast query language for software verification. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2004 | SAS | The Blast Query Language for Software Verification.. | Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2003 | CAV | Thread-Modular Abstraction Refinement. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer |
| 2003 | ICALP | Counterexample-Guided Control. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar |
| 2002 | CAV | Temporal-Safety Proofs for Systems Code. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grgoire Sutre, Westley Weimer |
| 2002 | POPL | Lazy abstraction. | Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grgoire Sutre |
| 2001 | CAV | Microarchitecture Verification by Compositional Model Checking. | Ranjit Jhala, Kenneth L. McMillan |
| 2001 | CONCUR | Compositional Methods for Probabilistic Systems. | Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala |