Microarchitecture Verification by Compositional Model Checking. - Ranjit Jhala; Kenneth L. McMillan (CAV, 2001)

Compositional Methods for Probabilistic Systems. - Luca de Alfaro; Thomas A. Henzinger; Ranjit Jhala (CONCUR, 2001)

Temporal-Safety Proofs for Systems Code. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; George C. Necula; Grégoire Sutre; Westley Weimer (CAV, 2002)

Lazy abstraction. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Grégoire Sutre (POPL, 2002)

Extreme Model Checking. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Marco A. A. Sanvido (Verification: Theory and Practice, 2003)

Thread-Modular Abstraction Refinement. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Shaz Qadeer (CAV, 2003)

Counterexample-Guided Control. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (ICALP, 2003)

Software Verification with BLAST. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Grégoire Sutre (SPIN, 2003)

Generating Tests from Counterexamples. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (ICSE, 2004)

An Eclipse Plug-in for Model Checking. - Dirk Beyer 001; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (IWPC, 2004)

Invited talk: the blast query language for software verification. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (PEPM, 2004)

Race checking by context inference. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (PLDI, 2004)

The Blast Query Language for Software Verification.. - Dirk Beyer 001; Adam Chlipala; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (SAS, 2004)

Checking Memory Safety with Blast. - Dirk Beyer 001; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (FASE, 2005)

Path slicing. - Ranjit Jhala; Rupak Majumdar (PLDI, 2005)

Joining dataflow with predicates. - Jeffrey Fischer; Ranjit Jhala; Rupak Majumdar (ESEC/SIGSOFT FSE, 2005)

Permissive interfaces. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (ESEC/SIGSOFT FSE, 2005)

The BLAST Software Verification System. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (SPIN, 2005)

Counterexample-guided Planning. - Krishnendu Chatterjee; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (UAI, 2005)

Structural Invariants. - Ranjit Jhala; Rupak Majumdar; Ru-Gang Xu (SAS, 2006)

Bit level types for high level reasoning. - Ranjit Jhala; Rupak Majumdar (SIGSOFT FSE, 2006)

A Practical and Complete Approach to Predicate Refinement. - Ranjit Jhala; Kenneth L. McMillan (TACAS, 2006)

Array Abstractions from Proofs. - Ranjit Jhala; Kenneth L. McMillan (CAV, 2007)

Bounds Checking with Taint-Based Analysis. - Weihaw Chuang; Satish Narayanasamy; Brad Calder; Ranjit Jhala (HiPEAC, 2007)

OPIUM: Optimal Package Install/Uninstall Manager. - Chris Tucker; David Shuffelton; Ranjit Jhala; Sorin Lerner (ICSE, 2007)

Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (Awarded Best Paper). - Charles Killian; James W. Anderson; Ranjit Jhala; Amin Vahdat (NSDI, 2007)

Mace: language support for building distributed systems. - Charles Killian; James W. Anderson; Ryan Braud; Ranjit Jhala; Amin Vahdat (PLDI, 2007)

Lock allocation. - Michael Emmi; Jeffrey S. Fischer; Ranjit Jhala; Rupak Majumdar (POPL, 2007)

Interprocedural analysis of asynchronous programs. - Ranjit Jhala; Rupak Majumdar (POPL, 2007)

RELAY: static race detection on millions of lines of code. - Jan Wen Voung; Ranjit Jhala; Sorin Lerner (ESEC/SIGSOFT FSE, 2007)

State of the Union: Type Inference Via Craig Interpolation. - Ranjit Jhala; Rupak Majumdar; Ru-Gang Xu (TACAS, 2007)

Interpolant-Based Transition Relation Approximation. - Ranjit Jhala; Kenneth L. McMillan (Log. Methods Comput. Sci., 2007)

The software model checker Blast. - Dirk Beyer 001; Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar (Int. J. Softw. Tools Technol. Transf., 2007)

Deep typechecking and refactoring. - Zachary Tatlock; Chris Tucker; David Shuffelton; Ranjit Jhala; Sorin Lerner (OOPSLA, 2008)

Dataflow analysis for concurrent programs using datarace detection. - Ravi Chugh; Jan Wen Voung; Ranjit Jhala; Sorin Lerner (PLDI, 2008)

Liquid types. - Patrick Maxim Rondon; Ming Kawaguchi; Ranjit Jhala (PLDI, 2008)

Building Distributed Systems Using Mace. - Charles Killian; James W. Anderson; Ryan Braud; Ranjit Jhala; Amin Vahdat (Peer-to-Peer Computing, 2009)

Staged information flow for javascript. - Ravi Chugh; Jeffrey A. Meister; Ranjit Jhala; Sorin Lerner (PLDI, 2009)

Type-based data structure verification. - Ming Kawaguchi; Patrick Maxim Rondon; Ranjit Jhala (PLDI, 2009)

Verifying Reference Counting Implementations. - Michael Emmi; Ranjit Jhala; Eddie Kohler; Rupak Majumdar (TACAS, 2009)

Software model checking. - Ranjit Jhala; Rupak Majumdar (ACM Comput. Surv., 2009)

Dsolve: Safety Verification via Liquid Types. - Ming Kawaguchi; Patrick Maxim Rondon; Ranjit Jhala (CAV, 2010)

An empirical study of privacy-violating information flows in JavaScript web applications. - Dongseok Jang; Ranjit Jhala; Sorin Lerner; Hovav Shacham (CCS, 2010)

Low-level liquid types. - Patrick Maxim Rondon; Ming Kawaguchi; Ranjit Jhala (POPL, 2010)

Finding latent performance bugs in systems implementations. - Charles Killian; Karthik Nagaraj; Salman Pervez; Ryan Braud; James W. Anderson; Ranjit Jhala (SIGSOFT FSE, 2010)

Refinement type inference via abstract interpretation - Ranjit Jhala; Rupak Majumdar; Andrey Rybalchenko (CoRR, 2010)

Software Verification with Liquid Types. - Ranjit Jhala (APLAS, 2011)

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 001; Ranjit Jhala; Steven Swanson (ASPLOS, 2011)

Using Types for Software Verification. - Ranjit Jhala (CAV, 2011)

HMC: Verifying Functional Programs Using Abstract Interpreters. - Ranjit Jhala; Rupak Majumdar; Andrey Rybalchenko (CAV, 2011)

System D: Dependent Dynamic Dictionaries - Ravi Chugh; Patrick Maxim Rondon; Ranjit Jhala (CoRR, 2011)

Dependent Types for JavaScript - Ravi Chugh; Ranjit Jhala (CoRR, 2011)

CSolve: Verifying C with Liquid Types. - Patrick Maxim Rondon; Alexander Bakst; Ming Kawaguchi; Ranjit Jhala (CAV, 2012)

Dependent types for JavaScript. - Ravi Chugh; David Herman; Ranjit Jhala (OOPSLA, 2012)

Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs. - Panagiotis Vekris; Ranjit Jhala; Sorin Lerner; Yuvraj Agarwal (HotPower, 2012)

Deterministic parallelism via liquid effects. - Ming Kawaguchi; Patrick Maxim Rondon; Alexander Bakst; Ranjit Jhala (PLDI, 2012)

Verifying GPU kernels by test amplification. - Alan Leung; Manish Gupta 010; Yuvraj Agarwal; Rajesh Gupta 001; Ranjit Jhala; Sorin Lerner (PLDI, 2012)

Nested refinements: a logic for duck typing. - Ravi Chugh; Patrick Maxim Rondon; Ranjit Jhala (POPL, 2012)

Abstract Refinement Types. - Niki Vazou; Patrick Maxim Rondon; Ranjit Jhala (ESOP, 2013)

LiquidHaskell: experience with refinement types in the real world. - Niki Vazou; Eric L. Seidel; Ranjit Jhala (Haskell, 2014)

Refinement types for Haskell. - Niki Vazou; Eric L. Seidel; Ranjit Jhala; Dimitrios Vytiniotis; Simon L. Peyton Jones (ICFP, 2014)

Refinement types for Haskell. - Ranjit Jhala (PLPV, 2014)

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages. - Niki Vazou; Eric L. Seidel; Ranjit Jhala (CoRR, 2014)

Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271). - Fritz Henglein; Ranjit Jhala; Shriram Krishnamurthi; Peter Thiemann 001 (Dagstuhl Reports, 2014)

Abstractions from proofs. - Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar; Kenneth L. McMillan (ACM SIGPLAN Notices, 2014)

Trust, but Verify: Two-Phase Typing for Dynamic Languages. - Panagiotis Vekris; Benjamin Cosman; Ranjit Jhala (ECOOP, 2015)

Type Targeted Testing. - Eric L. Seidel; Niki Vazou; Ranjit Jhala (ESOP, 2015)

Bounded refinement types. - Niki Vazou; Alexander Bakst; Ranjit Jhala (ICFP, 2015)

On Subnormal Floating Point and Abnormal Timing. - Marc Andrysco; David Kohlbrenner; Keaton Mowery; Ranjit Jhala; Sorin Lerner; Hovav Shacham (IEEE Symposium on Security and Privacy, 2015)

NSF expedition on variability-aware software: Recent results and contributions. - 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 001; Rajesh K. Gupta 001; et al. (it Inf. Technol., 2015)

Refinement types for TypeScript. - Panagiotis Vekris; Benjamin Cosman; Ranjit Jhala (PLDI, 2016)

Printing floating-point numbers: a faster, always correct method. - Marc Andrysco; Ranjit Jhala; Sorin Lerner (POPL, 2016)

Predicate Abstraction for Linked Data Structures. - Alexander Bakst; Ranjit Jhala (VMCAI, 2016)

Dynamic Witnesses for Static Type Errors. - Eric L. Seidel; Ranjit Jhala; Westley Weimer (CoRR, 2016)

Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT). - Niki Vazou; Ranjit Jhala (CoRR, 2016)

Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131). - Marco Gaboardi; Suresh Jagannathan; Ranjit Jhala; Stephanie Weirich (Dagstuhl Reports, 2016)

FaCT: A Flexible, Constant-Time Programming Language. - Sunjay Cauligi; Gary Soeller; Fraser Brown; Brian Johannesmeyer; Yunlu Huang; Ranjit Jhala; Deian Stefan (SecDev, 2017)

Finding and Preventing Bugs in JavaScript Bindings. - Fraser Brown; Shravan Narayan; Riad S. Wahby; Dawson R. Engler; Ranjit Jhala; Deian Stefan (IEEE Symposium on Security and Privacy, 2017)

Deriving Law-Abiding Instances. - Ryan G. Scott; Vikraman Choudhury; Ryan Newton; Niki Vazou; Ranjit Jhala (CoRR, 2017)

Verifying distributed programs via canonical sequentialization. - Alexander Bakst; Klaus von Gleissenthall; Rami Gökhan Kici; Ranjit Jhala (Proc. ACM Program. Lang., 2017)

Local refinement typing. - Benjamin Cosman; Ranjit Jhala (Proc. ACM Program. Lang., 2017)

Learning to blame: localizing novice type errors with data-driven diagnosis. - Eric L. Seidel; Huma Sibghat; Kamalika Chaudhuri; Westley Weimer; Ranjit Jhala (Proc. ACM Program. Lang., 2017)

Towards Verified, Constant-time Floating Point Operations. - Marc Andrysco; Andres Nötzli; Fraser Brown; Ranjit Jhala; Deian Stefan (CCS, 2018)

Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong). - Eric L. Seidel; Ranjit Jhala; Westley Weimer (J. Funct. Program., 2018)

Refinement reflection: complete verification with SMT. - Niki Vazou; Anish Tondwalkar; Vikraman Choudhury; Ryan G. Scott; Ryan R. Newton; Philip Wadler; Ranjit Jhala (Proc. ACM Program. Lang., 2018)

Predicate Abstraction for Program Verification. - Ranjit Jhala; Andreas Podelski; Andrey Rybalchenko (Handbook of Model Checking, 2018)

InFix: Automatically Repairing Novice Program Inputs. - Madeline Endres; Georgios Sakkas; Benjamin Cosman; Ranjit Jhala; Westley Weimer (ASE, 2019)

FaCT: a DSL for timing-sensitive computation. - Sunjay Cauligi; Gary Soeller; Brian Johannesmeyer; Fraser Brown; Riad S. Wahby; John Renner; Benjamin Grégoire; Gilles Barthe; Ranjit Jhala; Deian Stefan (PLDI, 2019)

Lazy counterfactual symbolic execution. - William T. Hallahan; Anton Xue; Maxwell Troy Bland; Ranjit Jhala; Ruzica Piskac (PLDI, 2019)

IODINE: Verifying Constant-Time Execution of Hardware. - Klaus von Gleissenthall; Rami Gökhan Kici; Deian Stefan; Ranjit Jhala (USENIX Security Symposium, 2019)

Pretend synchrony: synchronous verification of asynchronous distributed programs. - Klaus von Gleissenthall; Rami Gökhan Kici; Alexander Bakst; Deian Stefan; Ranjit Jhala (Proc. ACM Program. Lang., 2019)

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; et al. (CAV (1), 2020)

Type error feedback via analytic program repair. - Georgios Sakkas; Madeline Endres; Benjamin Cosman; Westley Weimer; Ranjit Jhala (PLDI, 2020)

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 (SIGCSE, 2020)

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; Daniel Peebles; Neha Rungta; Cole Schlesinger; Chriss Stephens; et al. (ESEC/SIGSOFT FSE, 2020)

Automatically Eliminating Speculative Leaks With Blade. - Marco Vassena; Klaus von Gleissenthall; Rami Gökhan Kici; Deian Stefan; Ranjit Jhala (CoRR, 2020)

Program synthesis by type-guided abstraction refinement. - Zheng Guo 003; Michael James 003; David Justo; Jiaxiao Zhou; Ziteng Wang; Ranjit Jhala; Nadia Polikarpova (Proc. ACM Program. Lang., 2020)

Digging for fold: synthesis-aided API discovery for Haskell. - Michael B. James; Zheng Guo 003; Ziteng Wang; Shivani Doshi; Hila Peleg; Ranjit Jhala; Nadia Polikarpova (Proc. ACM Program. Lang., 2020)

Solver-Aided Constant-Time Hardware Verification. - Klaus von Gleissenthall; Rami Gökhan Kici; Deian Stefan; Ranjit Jhala (CCS, 2021)

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types. - Anish Tondwalkar; Matthew Kolosick; Ranjit Jhala (ECOOP, 2021)

STORM: Refinement Types for Secure Web Applications. - Nico Lehmann; Rose Kunkel; Jordan Brown; Jean Yang 001; Niki Vazou; Nadia Polikarpova; Deian Stefan; Ranjit Jhala (OSDI, 2021)

RAPID: checking API usage for the cloud in the cloud. - Michael Emmi; Liana Hadarean; Ranjit Jhala; Lee Pike; Nicolás Rosner; Martin Schäf; Aritra Sengupta; Willem Visser (ESEC/SIGSOFT FSE, 2021)

Solver-Aided Constant-Time Circuit Verification. - Rami Gökhan Kici; Klaus von Gleissenthall; Deian Stefan; Ranjit Jhala (CoRR, 2021)

Isolation Without Taxation: Near Zero Cost Transitions for SFI. - Matthew Kolosick; Shravan Narayan; Conrad Watt; Michael LeMay; Deepak Garg 001; Ranjit Jhala; Deian Stefan (CoRR, 2021)

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version). - Anish Tondwalkar; Matthew Kolosick; Ranjit Jhala (CoRR, 2021)

mist: Refinements of Futures Past (Artifact). - Anish Tondwalkar; Matthew Kolosick; Ranjit Jhala (Dagstuhl Artifacts Ser., 2021)

Refinement Types: A Tutorial. - Ranjit Jhala; Niki Vazou (Found. Trends Program. Lang., 2021)

Automatically eliminating speculative leaks from cryptographic code with blade. - Marco Vassena; Craig Disselkoen; Klaus von Gleissenthall; Sunjay Cauligi; Rami Gökhan Kici; Ranjit Jhala; Dean M. Tullsen; Deian Stefan (Proc. ACM Program. Lang., 2021)

Embedded Domain Specific Verifiers. - Ranjit Jhala (Principles of Systems Design, 2022)

Flux: Liquid Types for Rust. - Nico Lehmann; Adam T. Geller; Gilles Barthe; Niki Vazou; Ranjit Jhala (CoRR, 2022)

Mechanizing Refinement Types (extended). - Michael Borkowski; Niki Vazou; Ranjit Jhala (CoRR, 2022)

Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI. - Matthew Kolosick; Shravan Narayan; Evan Johnson 001; Conrad Watt; Michael LeMay; Deepak Garg 001; Ranjit Jhala; Deian Stefan (Proc. ACM Program. Lang., 2022)

Seq2Parse: neurosymbolic parse error repair. - Georgios Sakkas; Madeline Endres; Philip J. Guo; Westley Weimer; Ranjit Jhala (Proc. ACM Program. Lang., 2022)

Flux: Liquid Types for Rust. - Nico Lehmann; Adam T. Geller; Niki Vazou; Ranjit Jhala (Proc. ACM Program. Lang., 2023)

The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming. - Lennart Augustsson; Joachim Breitner; Koen Claessen; Ranjit Jhala; Simon Peyton Jones; Olin Shivers; Guy L. Steele Jr.; Tim Sweeney (Proc. ACM Program. Lang., 2023)

Complete First-Order Reasoning for Properties of Functional Programs. - Adithya Murali; Lucas Peña; Ranjit Jhala; P. Madhusudan (Proc. ACM Program. Lang., 2023)

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 (SOSP, 2024)

Laurel: Generating Dafny Assertions Using Large Language Models. - Eric Mugnier; Emmanuel Anaya Gonzalez; Ranjit Jhala; Nadia Polikarpova; Yuanyuan Zhou 001 (CoRR, 2024)

CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. - Cole Kurashige; Ruyi Ji; Aditya Giridharan; Mark Barbone; Daniel Noor; Shachar Itzhaky; Ranjit Jhala; Nadia Polikarpova (Proc. ACM Program. Lang., 2024)

Refinement Type Refutations. - Robin Webbers; Klaus von Gleissenthall; Ranjit Jhala (Proc. ACM Program. Lang., 2024)

Mechanizing Refinement Types. - Michael Borkowski; Niki Vazou; Ranjit Jhala (Proc. ACM Program. Lang., 2024)

Neurosymbolic Modular Refinement Type Inference. - Georgios Sakkas; Pratyush Sahu; Kyeling Ong; Ranjit Jhala (ICSE, 2025)

Counterexample-Guided Inference of Modular Specifications. - William T. Hallahan; Ranjit Jhala; Ruzica Piskac (Proc. ACM Program. Lang., 2025)

Robust Constant-Time Cryptography. - Matthew Kolosick; Basavesh Ammanaghatta Shivakumar; Sunjay Cauligi; Marco Patrignani; Marco Vassena; Ranjit Jhala; Deian Stefan (Proc. ACM Program. Lang., 2025)

Generic Refinement Types. - Nico Lehmann; Cole Kurashige; Nikhil Akiti; Niroop Krishnakumar; Ranjit Jhala (Proc. ACM Program. Lang., 2025)

Laurel: Unblocking Automated Verification with Large Language Models. - Eric Mugnier; Emmanuel Anaya Gonzalez; Nadia Polikarpova; Ranjit Jhala; Yuanyuan Zhou 001 (Proc. ACM Program. Lang., 2025)