I am interested in Programming Languages and Software Engineering, more specifically, in techniques for building reliable computer systems. My work draws from, combines and contributes to methods the areas of Type Systems, Model Checking, Program Analysis and Automated Deduction.
Refinement types for Rust
Liquid Types for Haskell
Analyzing programs using models learned from interaction-traces
Verifying Distributed Programs via Sequentialization
Binding bugs and Timing Channels
Liquid Types for TypeScript
The following monographs are long introductions, suitable for a graduate class:
Refinement Types: A Tutorial
Ranjit Jhala and Niki Vazou
PDF, Code
Programming With Refinement Types
Ranjit Jhala, Eric Seidel and Niki Vazou
PDF, Online
Software Model Checking
Ranjit Jhala and Rupak Majumdar
ACM Computing Surveys, Volume 41 Issue 4, October 2009
PDF, ACM DL
Program Verification by Lazy Abstraction
Ranjit Jhala
Ph.D Dissertation, UC Berkeley, 2004
PDF
Formal Methods: Future Directions & Its Transition To Practice
Ranjit Jhala & Rupak Majumdar (Eds.)
Report compiled from NSF Workshop
Summary-PDF Full-PDF
Below is a list of papers I’ve written; also at Google Scholar, DBLP or ArXiv.
STORM: Refinement Types for Secure Web Applications
Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala
15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2021)
PDF
49Automatically Eliminating Speculative Leaks fromCryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthal, Sunjay Cauligi, Rami Gokhan, Ranjit Jhala, Dean Tullsen, Deian Stefan
48th ACM Symposium on Principles of Programming Languages (POPL 2021)
PDF
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
35th European Conference on Object Oriented Programming (ECOOP 2021)
PDF
XENON: Solver-Aided Constant Time Verification of Hardware
Klaus Gleissenthal, Rami Gokhan, Deian Stefan, Ranjit Jhala
ACM Conference on Computer Security (CCS 2021)
PDF
Type error feedback via analytic program repair
Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, Ranjit Jhala
42st ACM Conference on Programming Language Design and Implementation (PLDI 2020)
PDF
PABLO: Helping Novices Debug Python Code Through Data-Driven Fault Localization
Benjamin Cosman, Madeline Endres, Georgios Sakkas, Leon Medvinsky, Yao-Yuan Yang, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
51st ACM Technical Symposium on Computer Science Education (SIGCSE 2020)
PDF
Block Public Access: Trust Safety Verification of Access Control Policies
Malik Bouchet, Byron Cook, Bryant Cutler, Anna Druzkina, Andrew Gacek, Liana Hadarean, Ranjit Jhala, Brad Marshall, Dan Peebles, Neha Rungta, Cole Schlesinger, Chriss Stephens, Carsten Varming, Andy Warfield
Foundations of Software Engineering (FSE 2020)
PDF
Stratified Abstraction of Access Control Policies
John Backes, Ulises Berrueco, Tyler Bray, Daniel Brim, Byron Cook, Andrew Gacek, Ranjit Jhala, Kasper Søe Luckow, Sean McLaughlin, Madhav Menon, Daniel Peebles, Ujjwal Pugalia, Neha Rungta, Cole Schlesinger, Adam Schodde, Anvesh Tanuku, Carsten Varming, Deepa Viswanathan
32nd International Conference on Computer-Aided Verification (CAV 2020)
PDF
Digging for Fold: Synthesis-Aided API Discovery for Haskell
Michael James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova
39th ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2020)
PDF
Program Synthesis by Type-Guided Abstraction Refinement
Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova
47th ACM Symposium on Principles of Programming Languages (POPL 2020)
PDF
FACT: A DSL for Timing-Sensitive Computation
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Gregoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
41st ACM Conference on Programming Language Design and Implementation (PLDI 2019)
PDF
Lazy Counterfactual Symbolic Execution
William Hallahan, Anton Xue, Maxwell Bland, Ranjit Jhala, Ruzica Piskac
41st ACM Conference on Programming Language Design and Implementation (PLDI 2019)
PDF
InFix: Automatically Repairing Novice Program Inputs
Madeline Endres, Georgios Sakkas, Benjamin Cosman, Ranjit Jhala, Westley Weimer
Automated Software Engineering (ASE 2019)
PDF
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Klaus von Gleissenthal, Rami Gokhan, Alexander Bakst, Ranjit Jhala
46th ACM Symposium on Principles of Programming Languages (POPL 2019)
PDF
IODINE: Verifying Constant-Time Execution of Hardware
Klaus Gleissenthal, Rami Gokhan, Deian Stefan, Ranjit Jhala
28th USENIX Security Symposium (USENIX Security 2019)
PDF
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Chowdhury, Ryan Scott, Ryan Newton, Philip Wadler, Ranjit Jhala
ACM Symposium on Principles of Programming Languages (POPL 2018)
PDF
Towards Verified, Constant-time Floating Point Operations
Marc Andrysco, Andres Noetzli, Fraser Brown, Deian Stefan, Ranjit Jhala
ACM Conference on Computer Security (CCS 2018)
PDF
Finding and Preventing Bugs in JavaScript Bindings
Fraser Brown, Shravan Narayan, Riad S. Wahby, Dawson Engler, Ranjit Jhala, Deian Stefan
38th IEEE Symposium on Security and Privacy (Oakland S&P 2017)
PDF
Local Refinement Typing
Benjamin Cosman, Ranjit Jhala
22nd ACM International Conference on Functional Programming (ICFP 2017)
PDF
Verifying Distributed Programs via Canonical Sequentialization
Alexander Bakst, Klaus Gleissenthal, Rami Gokhan, Ranjit Jhala
36th ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2017)
PDF
Learning to Blame: Localizing Type Errors via Machine Learning
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
36th ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2017)
PDF
Printing Floating Point Numbers: A faster, always correct method
Marc Andrysco, Ranjit Jhala, Sorin Lerner
43rd ACM Symposium on Principles of Programming Languages (POPL 2016)
PDF
Dynamic Witnesses for Static Type Errors
Eric Seidel, Ranjit Jhala, Westley Weimer
21st ACM International Conference on Functional Programming (ICFP 2016)
PDF
Predicate Abstraction for Linked Data Structures
Alexander Bakst, Ranjit Jhala
16th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2016)
PDF
Refinement Types for Typescript
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
34th ACM Conference on Programming Languages Design and Implementation (PLDI 2016)
PDF
Bounded Refinement Types
Niki Vazou, Alexander Bakst, Ranjit Jhala
20th ACM International Conference on Functional Programming (ICFP 2015)
PDF
On Subnormal Floating Point and Abnormal Timing
Mark Andrysco, Keaton Mowery, David Kohlbrenner, Ranjit Jhala, Sorin Lerner, Hovav Shacham
36th IEEE Symposium on Security and Privacy (Oakland S&P 2015)
PDF
Trust but Verify: Two Phase Typing for Dynamic Languages
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
29th European Conference on Object Oriented Programming (ECOOP 2015)
PDF
Type Targeted Testing
Eric Seidel, Niki Vazou, Ranjit Jhala
24th European Symposium on Programming (ESOP 2015)
PDF
Refinement Types for Haskell
Niki Vazou, Eric Seidel, Ranjit Jhala, Dimitris Vytiniotis, Simon Peyton-Jones
19th ACM International Conference on Functional Programming (ICFP 2014)
PDF
LiquidHaskell: Experience With Refinement Types In The Real World
Niki Vazou, Eric Seidel, Ranjit Jhala
ACM Haskell Symposium (Haskell 2014)
PDF
Abstract Refinement Types
Niki Vazou, Patric Rondon, Ranjit Jhala
22nd European Symposium on Programming (ESOP 2013)
PDF
Nested Refinements: A Logic For Duck Typing
Ravi Chugh, Patrick Rondon, Ranjit Jhala
39th ACM Symposium on Principles of Programming Languages (POPL 2012)
PDF
Verifying GPU Kernels by Test Amplification
Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner
34th ACM Conference on Programming Language Design and Implementation (PLDI 2012)
PDF
Deterministic Parallelism via Liquid Effects
Ming Kawaguchi, Patrick Rondon, Alexander Bakst, Ranjit Jhala
34th ACM Conference on Programming Language Design and Implementation (PLDI 2012)
PDF
CSolve: Verifying C With Liquid Types
Patrick Rondon, Ming Kawaguchi, Alexander Bakst, Ranjit Jhala
24th International Conference on Computer-Aided Verification (CAV 2012)
PDF
Dependent Types for JavaScript
Ravi Chugh, David Herman, Ranjit Jhala
31st ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2012)
PDF
NV-Heaps: Making Persistent Objects Fast and Safe with Next-Generation, Non-Volatile Memories
Joel Coburn, Adrian Caulfield, Ameen Akel, Laura Grupp, Rajesh Gupta, Ranjit Jhala, Steven Swanson
16th ACM Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2011)
PDF
HMC: Verifying Functional Programs With Abstract Interpreters
Rupak Majumdar, Andrey Rybalchenko, Ranjit Jhala
23rd Conference on Computer-Aided Verification (CAV 2011)
PDF
Low-level Liquid Types
Patrick Rondon, Ming Kawaguchi, Ranjit Jhala
37th ACM Symposium on Principles of Programming Languages (POPL 2010)
PDF
Finding Latent Performance Bugs in Systems Implementations
Charles Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud, James W. Anderson, Ranjit Jhala
16th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2010)
PDF
Dsolve: Safety Verification with Liquid Types
Ming Kawaguchi, Patrick Rondon, Ranjit Jhala
22nd International Conference on Computer-Aided Verification (CAV 2010)
PDF
An Empirical Study of Privacy-Violating Information Flows in JavaScript Web Applications
Don Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham
17th ACM Conference on Computer and Communications Security (CCS 2010)
PDF
Verifying Reference Counting Implementations
Michael Emmi, Eddie Kohler, Ranjit Jhala, Rupak Majumdar
15th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009)
PDF
Staged Information Flow for JavaScript
Ravi Chugh, Jeff Meister, Ranjit Jhala, Sorin Lerner
31st ACM Conference on Programming Language Design and Implementation (PLDI 2009)
PDF
Type-based Data Structure Verification
Ming Kawaguchi, Patrick Rondon, Ranjit Jhala
31st ACM Conference on Programming Language Design and Implementation (PLDI 2009)
PDF
Dataflow Analysis for Concurrent Programs using Datarace Detection
Ravi Chugh, Jan Voung, Ranjit Jhala, Sorin Lerner
30th ACM Conference on Programming Language Design and Implementation (PLDI 2008)
PDF
Liquid Types
Patrick Rondon, Ming Kawaguchi, Ranjit Jhala
30th ACM Conference on Programming Language Design and Implementation (PLDI 2008)
PDF
Deep Typechecking and Refactoring
Zach Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
23rd ACM Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2008)
PDF
Interprocedural Analysis of Asynchronous Programs
Ranjit Jhala, Rupak Majumdar
34th ACM Symposium on Principles of Programming Languages (POPL 2007)
PDF
Lock Allocation
Michael Emmi, Jeff Fischer, Ranjit Jhala, Rupak Majumdar
34th ACM Symposium on Principles of Programming Languages (POPL 2007)
PDF
State of the Union: Type Inference via Craig Interpolation
Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu
13th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007)
PDF
OPIUM: Optimum Package Intall/Uninstall Management
Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
29th ACM/IEEE International Conference on Software Engineering (ICSE 2007)
PDF
Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code
Charles Killian, James Anderson, Ranjit Jhala, Amin Vahdat
4th USENIX Symposium on Networked Systems Design and Implementation [Best Paper] (NSDI 2007)
PDF
Mace: Language Support for Building Distributed Systems
Charles Killian, James Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat
29th ACM Conference on Programming Language Design and Implementation (PLDI 2007)
PDF
Array Abstractions from Proofs
Ranjit Jhala, Kenneth L. McMillan
19th Conference on Computer-Aided Verification (CAV 2007)
PDF
RELAY: Static Race Detection on Millions of Lines of Code
Jan Voung, Ranjit Jhala, Sorin Lerner
15th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2007)
PDF
A Practical and Complete Approach to Predicate Refinement
Ranjit Jhala, Kenneth L. McMillan
12th Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2006)
PDF
Structural Invariants
Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu
13th International Static Analysis Symposium (SAS 2006)
PDF
Bit-Level Types for High-Level Reasoning
Ranjit Jhala, Rupak Majumdar
14th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2006)
PDF
Path Slicing
Ranjit Jhala, Rupak Majumdar
27th ACM Conference on Programming Language Design and Implementation (PLDI 2005)
PDF
Interpolant-based Transition Relation Approximation
Ranjit Jhala, Kenneth L. McMillan
17th International Conference on Computer-Aided Verification (CAV 2005)
PDF
Counterexample-Guided Planning
Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
21st Conference on Uncertainty in Artificial Intelligence (UAI 2005)
PDF
Joining Dataflow with Predicates
Jeffrey Fischer, Ranjit Jhala, Rupak Majumdar
13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2005)
PDF
Permissive Interfaces
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE 2005)
PDF
Abstractions from Proofs
Thomas A. Henzinger, Rupak Majumdar, Ranjit Jhala, Kenneth L. McMillan
31st ACM Symposium on Principles of Programming Languages (POPL 2004)
PDF
Generating Tests from Counterexamples
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
26th ACM/IEEE International Conference on Software Engineering (ICSE 2004)
PDF
Race Checking by Context Inference
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
26th ACM Conference on Programming Language Design and Implementation (PLDI 2004)
PDF
Software Verification with BLAST
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre
10th International Workshop on Model Checking Software (SPIN 2003)
PDF
Extreme Model Checking
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco Sanvido
International Symposium on Verification: Theory and Practice (Invited 2003)
PDF
Counterexample-Guided Control
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
30th International Colloquium on Automata, Languages and Programming (ICALP 2003)
PDF
Thread-Modular Abstraction Refinement
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer
15th International Conference on Computer-Aided Verification (CAV 2003)
PDF
Temporal-safety Proofs for Systems Code
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George Necula, Westley Weimer, Gregoire Sutre
14th International Conference on Computer-Aided Verification (CAV 2002)
PDF
Lazy Abstraction
Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Gregoire Sutre
ACM Symposium on Principles of Programming Languages (POPL 2002)
PDF
Microarchitecture Verification by Compositional Model Checking
Ranjit Jhala, Kenneth L. McMillan
13th Conference on Computer-Aided Verification (CAV 2001)
PDF
Compositional Methods for Probabilistic Systems
Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala
12th Conference on Concurrency Theory (CONCUR 2001)
PDF