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

LiquidHaskell

Liquid Types for Haskell

Code Analytics

Analyzing programs using models learned from interaction-traces

Canonical

Verifying Distributed Programs via Sequentialization

Browser Security

Binding bugs and Timing Channels

Past Projects

RefScript

Liquid Types for TypeScript

CSolve

DSolve

Relay

Mace/MC

Monographs

The following monographs are long introductions, suitable for a graduate class:

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.

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

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