Research

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.

Current Projects

Flux

Refinement types for Rust

  • [Code][code-flux]
  • Papers: PLDI 23

LiquidHaskell

Liquid Types for Haskell

Code Analytics

Analyzing programs using models learned from interaction-traces

Pretend Synch.

Verifying Distributed Programs via Sequentialization

Browser Security

Binding bugs and Timing Channels

Past Projects

RefScript

Liquid Types for TypeScript

CSolve

DSolve

Relay

Mace/MC

Blast

Monographs

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

Papers

Below is a list of papers I’ve written; also at Google Scholar, DBLP or ArXiv.

2021

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

2020

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

2019

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

2018

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

2017

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

2016

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

2015

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

2014

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

2013

Abstract Refinement Types
Niki Vazou, Patric Rondon, Ranjit Jhala
22nd European Symposium on Programming (ESOP 2013)
PDF

2012

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

2011

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

2010

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

2009

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

2008

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

2007

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

2006

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

2005

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

2004

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

2003

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

2002

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

2001

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