Ranjit Jhala

ORCID

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 56

Top Venues

CoRR

Proc. ACM Program. Lang.

PLDI

ICFP

Publications

Michael Borkowski, Niki Vazou, Ranjit Jhala
Mechanizing Refinement Types. Proc. ACM Program. Lang. 8 (POPL) (2024)
Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou
Laurel: Generating Dafny Assertions Using Large Language Models. CoRR (2024)
Nico Lehmann, Adam T. Geller, Niki Vazou, Ranjit Jhala
Flux: Liquid Types for Rust. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan
Robust Constant-Time Cryptography. CoRR (2023)
Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele Jr., Tim Sweeney
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming. Proc. ACM Program. Lang. 7 (ICFP) (2023)
Adithya Murali, Lucas Peña, Ranjit Jhala, P. Madhusudan
Complete First-Order Reasoning for Properties of Functional Programs. Proc. ACM Program. Lang. 7 (OOPSLA2) (2023)
Ranjit Jhala
Embedded Domain Specific Verifiers. Principles of Systems Design (2022)
Michael Borkowski, Niki Vazou, Ranjit Jhala
Mechanizing Refinement Types (extended). CoRR (2022)
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan
Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI. Proc. ACM Program. Lang. 6 (POPL) (2022)
Georgios Sakkas, Madeline Endres, Philip J. Guo, Westley Weimer, Ranjit Jhala
Seq2Parse: neurosymbolic parse error repair. Proc. ACM Program. Lang. 6 (OOPSLA2) (2022)
Nico Lehmann, Adam Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala
Flux: Liquid Types for Rust. CoRR (2022)
Ranjit Jhala, Niki Vazou
Refinement Types: A Tutorial. Found. Trends Program. Lang. 6 (3-4) (2021)
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types. ECOOP (2021)
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
mist: Refinements of Futures Past (Artifact). Dagstuhl Artifacts Ser. 7 (2) (2021)
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version). CoRR (2021)
Rami Gökhan Kici, Klaus von Gleissenthall, Deian Stefan, Ranjit Jhala
Solver-Aided Constant-Time Circuit Verification. CoRR (2021)
Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
Solver-Aided Constant-Time Hardware Verification. CCS (2021)
Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala
STORM: Refinement Types for Secure Web Applications. OSDI (2021)
Matthew Kolosick, Shravan Narayan, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan
Isolation Without Taxation: Near Zero Cost Transitions for SFI. CoRR (2021)
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Ranjit Jhala, Dean M. Tullsen, Deian Stefan
Automatically eliminating speculative leaks from cryptographic code with blade. Proc. ACM Program. Lang. 5 (POPL) (2021)
Michael Emmi, Liana Hadarean, Ranjit Jhala, Lee Pike, Nicolás Rosner, Martin Schäf, Aritra Sengupta, Willem Visser
RAPID: checking API usage for the cloud in the cloud. ESEC/SIGSOFT FSE (2021)
Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova
Digging for fold: synthesis-aided API discovery for Haskell. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
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
Stratified Abstraction of Access Control Policies. CAV (1) (2020)
Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, Ranjit Jhala
Type error feedback via analytic program repair. PLDI (2020)
Marco Vassena, Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
Automatically Eliminating Speculative Leaks With Blade. CoRR (2020)
Malik Bouchet, Byron Cook, Bryant Cutler, Anna Druzkina, Andrew Gacek, Liana Hadarean, Ranjit Jhala, Brad Marshall, Daniel Peebles, Neha Rungta, Cole Schlesinger, Chriss Stephens, Carsten Varming, Andy Warfield
Block public access: trust safety verification of access control policies. ESEC/SIGSOFT FSE (2020)
Ranjit Jhala, Niki Vazou
Refinement Types: A Tutorial. CoRR (2020)
Benjamin Cosman, Madeline Endres, Georgios Sakkas, Leon Medvinsky, Yao-Yuan Yang, Ranjit Jhala, Kamalika Chaudhuri, Westley Weimer
PABLO: Helping Novices Debug Python Code Through Data-Driven Fault Localization. SIGCSE (2020)
Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova
Program synthesis by type-guided abstraction refinement. Proc. ACM Program. Lang. 4 (POPL) (2020)
Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
IODINE: Verifying Constant-Time Execution of Hardware. USENIX Security Symposium (2019)
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
FaCT: a DSL for timing-sensitive computation. PLDI (2019)
William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, Ruzica Piskac
Lazy counterfactual symbolic execution. PLDI (2019)
Klaus von Gleissenthall, Rami Gökhan Kici, Alexander Bakst, Deian Stefan, Ranjit Jhala
Pretend synchrony: synchronous verification of asynchronous distributed programs. Proc. ACM Program. Lang. 3 (POPL) (2019)
Madeline Endres, Georgios Sakkas, Benjamin Cosman, Ranjit Jhala, Westley Weimer
InFix: Automatically Repairing Novice Program Inputs. ASE (2019)
Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
Iodine: Verifying Constant-Time Execution of Hardware. CoRR (2019)
Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova
Program Synthesis by Type-Guided Abstraction Refinement. CoRR (2019)
Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, Deian Stefan
Towards Verified, Constant-time Floating Point Operations. CCS (2018)
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang. 2 (POPL) (2018)
Eric L. Seidel, Ranjit Jhala, Westley Weimer
Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong). J. Funct. Program. 28 (2018)
Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan
FaCT: A Flexible, Constant-Time Programming Language. SecDev (2017)
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis. CoRR (2017)
Ryan G. Scott, Vikraman Choudhury, Ryan Newton, Niki Vazou, Ranjit Jhala
Deriving Law-Abiding Instances. CoRR (2017)
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
Learning to blame: localizing novice type errors with data-driven diagnosis. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
Fraser Brown, Shravan Narayan, Riad S. Wahby, Dawson R. Engler, Ranjit Jhala, Deian Stefan
Finding and Preventing Bugs in JavaScript Bindings. IEEE Symposium on Security and Privacy (2017)
Benjamin Cosman, Ranjit Jhala
Local Refinement Typing. CoRR (2017)
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
Refinement Reflection: Complete Verification with SMT. CoRR (2017)
Benjamin Cosman, Ranjit Jhala
Local refinement typing. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Alexander Bakst, Klaus von Gleissenthall, Rami Gökhan Kici, Ranjit Jhala
Verifying distributed programs via canonical sequentialization. Proc. ACM Program. Lang. 1 (OOPSLA) (2017)
Marc Andrysco, Ranjit Jhala, Sorin Lerner
Printing floating-point numbers: a faster, always correct method. POPL (2016)
Niki Vazou, Ranjit Jhala
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT). CoRR (2016)
Eric L. Seidel, Ranjit Jhala, Westley Weimer
Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong). ICFP (2016)
Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, Stephanie Weirich
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). Dagstuhl Reports 6 (3) (2016)
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
Refinement types for TypeScript. PLDI (2016)
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
Refinement Types for TypeScript. CoRR (2016)
Eric L. Seidel, Ranjit Jhala, Westley Weimer
Dynamic Witnesses for Static Type Errors. CoRR (2016)
Alexander Bakst, Ranjit Jhala
Predicate Abstraction for Linked Data Structures. VMCAI (2016)
Eric L. Seidel, Niki Vazou, Ranjit Jhala
Type Targeted Testing. ESOP (2015)
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
Trust, but Verify: Two-Phase Typing for Dynamic Languages. ECOOP (2015)
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
Trust, but Verify: Two-Phase Typing for Dynamic Languages. CoRR (2015)
Lucas Francisco Wanner, Liangzhen Lai, Abbas Rahimi, Mark Gottscho, Pietro Mercati, Chu-Hsiang Huang, Frederic Sala, Yuvraj Agarwal, Lara Dolecek, Nikil D. Dutt, Puneet Gupta, Rajesh K. Gupta, Ranjit Jhala, Rakesh Kumar, Sorin Lerner, Subhasish Mitra, Alexandru Nicolau, Tajana Simunic Rosing, Mani B. Srivastava, Steven Swanson, Dennis Sylvester, Yuanyuan Zhou
NSF expedition on variability-aware software: Recent results and contributions. it Inf. Technol. 57 (3) (2015)
Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, Hovav Shacham
On Subnormal Floating Point and Abnormal Timing. IEEE Symposium on Security and Privacy (2015)
Alexander Bakst, Ranjit Jhala
Predicate Abstraction for Linked Data Structures. CoRR (2015)
Niki Vazou, Alexander Bakst, Ranjit Jhala
Bounded Refinement Types. CoRR (2015)
Niki Vazou, Alexander Bakst, Ranjit Jhala
Bounded refinement types. ICFP (2015)
Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, Peter Thiemann
Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271). Dagstuhl Reports 4 (6) (2014)
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
Abstractions from proofs. ACM SIGPLAN Notices 49 (4S) (2014)
Niki Vazou, Eric L. Seidel, Ranjit Jhala
From Safety To Termination And Back: SMT-Based Verification For Lazy Languages. CoRR (2014)
Ranjit Jhala
Refinement types for Haskell. PLPV (2014)
Niki Vazou, Eric L. Seidel, Ranjit Jhala
LiquidHaskell: experience with refinement types in the real world. Haskell (2014)
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon L. Peyton Jones
Refinement types for Haskell. ICFP (2014)
Eric L. Seidel, Niki Vazou, Ranjit Jhala
Type Targeted Testing. CoRR (2014)
Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala
Abstract Refinement Types. ESOP (2013)
Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
Counterexample-guided Planning CoRR (2012)
Ravi Chugh, David Herman, Ranjit Jhala
Dependent types for JavaScript. OOPSLA (2012)
Ranjit Jhala
Software Verification with Liquid Types. VMCAI (2012)
Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala
CSolve: Verifying C with Liquid Types. CAV (2012)
Ming Kawaguchi, Patrick Maxim Rondon, Alexander Bakst, Ranjit Jhala
Deterministic parallelism via liquid effects. PLDI (2012)
Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala
Nested refinements: a logic for duck typing. POPL (2012)
Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner
Verifying GPU kernels by test amplification. PLDI (2012)
Panagiotis Vekris, Ranjit Jhala, Sorin Lerner, Yuvraj Agarwal
Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs. HotPower (2012)
Joel Coburn, Adrian M. Caulfield, Ameen Akel, Laura M. Grupp, Rajesh K. Gupta, Ranjit Jhala, Steven Swanson
NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories. ASPLOS (2011)
Ranjit Jhala
Software Verification with Liquid Types. APLAS (2011)
Ranjit Jhala
Using Types for Software Verification. CAV (2011)
Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala
System D: Dependent Dynamic Dictionaries CoRR (2011)
Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
HMC: Verifying Functional Programs Using Abstract Interpreters. CAV (2011)
Ravi Chugh, Ranjit Jhala
Dependent Types for JavaScript CoRR (2011)
Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala
Dsolve: Safety Verification via Liquid Types. CAV (2010)
Charles Edwin Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud, James W. Anderson, Ranjit Jhala
Finding latent performance bugs in systems implementations. SIGSOFT FSE (2010)
Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala
Low-level liquid types. POPL (2010)
Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
Refinement type inference via abstract interpretation CoRR (2010)
Dongseok Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham
An empirical study of privacy-violating information flows in JavaScript web applications. CCS (2010)
Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar
Verifying Reference Counting Implementations. TACAS (2009)
Ranjit Jhala, Rupak Majumdar
Software model checking. ACM Comput. Surv. 41 (4) (2009)
Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala
Type-based data structure verification. PLDI (2009)
Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner
Staged information flow for javascript. PLDI (2009)
Charles Edwin Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat
Building Distributed Systems Using Mace. Peer-to-Peer Computing (2009)
Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner
Dataflow analysis for concurrent programs using datarace detection. PLDI (2008)
Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala
Liquid types. PLDI (2008)
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
Deep typechecking and refactoring. OOPSLA (2008)
Ranjit Jhala, Kenneth L. McMillan
Interpolant-Based Transition Relation Approximation. Log. Methods Comput. Sci. 3 (4) (2007)

Ranjit Jhala.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Ranjit Jhala