Ranjit Jhala

154 papers A* 45A 14B 10C 3Misc 1Journal 60Unranked 19
YearRankTypeTitle / Venue / Authors
2026 — conf
Auditing Rust Crates Effectively.
ESOP (2)
Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford
2026 J jnl
Auditing Rust Crates Effectively.
CoRR
Lydia Zoghbi, David Thien, Ranjit Jhala, Deian Stefan, Caleb Stanford
2025 J jnl
Counterexample-Guided Inference of Modular Specifications.
Proc. ACM Program. Lang.
William T. Hallahan, Ranjit Jhala, Ruzica Piskac
2025 J jnl
Generic Refinement Types.
Proc. ACM Program. Lang.
Nico Lehmann, Cole Kurashige, Nikhil Akiti, Niroop Krishnakumar, Ranjit Jhala
2025 J jnl
Laurel: Unblocking Automated Verification with Large Language Models.
Proc. ACM Program. Lang.
Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, Yuanyuan Zhou
2025 A* conf
Neurosymbolic Modular Refinement Type Inference.
ICSE
Georgios Sakkas, Pratyush Sahu, Kyeling Ong, Ranjit Jhala
2025 J jnl
On the Impact of Formal Verification on Software Development.
Proc. ACM Program. Lang.
Eric Mugnier, Yuanyuan Zhou, Ranjit Jhala, Michael Coblenz
2025 J jnl
Robust Constant-Time Cryptography.
Proc. ACM Program. Lang.
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan
2025 A* conf
TickTock: Verified Isolation in a Production Embedded OS.
SOSP
Vivien Rindisbacher, Evan Johnson, Nico Lehmann, Tyler Potyondy, Pat Pannuto, Stefan Savage, Deian Stefan, Ranjit Jhala
2024 J jnl
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs.
Proc. ACM Program. Lang.
Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova
2024 A* conf
Icarus: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution.
SOSP
Naomi Smith, Abhishek Sharma, John Renner, David Thien, Fraser Brown, Hovav Shacham, Ranjit Jhala, Deian Stefan
2024 J jnl
Laurel: Generating Dafny Assertions Using Large Language Models.
CoRR
Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou
2024 J jnl
Mechanizing Refinement Types.
Proc. ACM Program. Lang.
Michael Borkowski, Niki Vazou, Ranjit Jhala
2024 J jnl
Refinement Type Refutations.
Proc. ACM Program. Lang.
Robin Webbers, Klaus von Gleissenthall, Ranjit Jhala
2023 J jnl
Complete First-Order Reasoning for Properties of Functional Programs.
Proc. ACM Program. Lang.
Adithya Murali, Lucas Peña, Ranjit Jhala, P. Madhusudan
2023 J jnl
Flux: Liquid Types for Rust.
Proc. ACM Program. Lang.
Nico Lehmann, Adam T. Geller, Niki Vazou, Ranjit Jhala
2023 J jnl
Robust Constant-Time Cryptography.
CoRR
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, Deian Stefan
2023 J jnl
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming.
Proc. ACM Program. Lang.
Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele Jr., Tim Sweeney
2022 — conf
Embedded Domain Specific Verifiers.
Principles of Systems Design
Ranjit Jhala
2022 J jnl
Flux: Liquid Types for Rust.
CoRR
Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala
2022 J jnl
Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI.
Proc. ACM Program. Lang.
Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan
2022 J jnl
Mechanizing Refinement Types (extended).
CoRR
Michael Borkowski, Niki Vazou, Ranjit Jhala
2022 A* ed.
PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022
PLDI
Ranjit Jhala, Isil Dillig
2022 J jnl
Seq2Parse: neurosymbolic parse error repair.
Proc. ACM Program. Lang.
Georgios Sakkas, Madeline Endres, Philip J. Guo, Westley Weimer, Ranjit Jhala
2021 J jnl
Automatically eliminating speculative leaks from cryptographic code with blade.
Proc. ACM Program. Lang.
Marco Vassena, Craig Disselkoen, Klaus von Gleissenthall, Sunjay Cauligi, Rami Gökhan Kici, Ranjit Jhala, Dean M. Tullsen, Deian Stefan
2021 J jnl
Isolation Without Taxation: Near Zero Cost Transitions for SFI.
CoRR
Matthew Kolosick, Shravan Narayan, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan
2021 — conf
RAPID: checking API usage for the cloud in the cloud.
ESEC/SIGSOFT FSE
Michael Emmi, Liana Hadarean, Ranjit Jhala, Lee Pike, Nicolás Rosner, Martin Schäf, Aritra Sengupta, Willem Visser
2021 J jnl
Refinement Types: A Tutorial.
Found. Trends Program. Lang.
Ranjit Jhala, Niki Vazou
2021 J jnl
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version).
CoRR
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
2021 A conf
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types.
ECOOP
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
2021 A* conf
STORM: Refinement Types for Secure Web Applications.
OSDI
Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala
2021 J jnl
Solver-Aided Constant-Time Circuit Verification.
CoRR
Rami Gökhan Kici, Klaus von Gleissenthall, Deian Stefan, Ranjit Jhala
2021 A* conf
Solver-Aided Constant-Time Hardware Verification.
CCS
Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
2021 J jnl
mist: Refinements of Futures Past (Artifact).
Dagstuhl Artifacts Ser.
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
2020 J jnl
Automatically Eliminating Speculative Leaks With Blade.
CoRR
Marco Vassena, Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
2020 — conf
Block public access: trust safety verification of access control policies.
ESEC/SIGSOFT FSE
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
2020 J jnl
Digging for fold: synthesis-aided API discovery for Haskell.
Proc. ACM Program. Lang.
Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, Nadia Polikarpova
2020 A conf
PABLO: Helping Novices Debug Python Code Through Data-Driven Fault Localization.
SIGCSE
Benjamin Cosman, Madeline Endres, Georgios Sakkas, Leon Medvinsky, Yao-Yuan Yang, Ranjit Jhala, Kamalika Chaudhuri, Westley Weimer
2020 J jnl
Program synthesis by type-guided abstraction refinement.
Proc. ACM Program. Lang.
Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova
2020 J jnl
Refinement Types: A Tutorial.
CoRR
Ranjit Jhala, Niki Vazou
2020 — conf
Stratified Abstraction of Access Control Policies.
CAV (1)
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
2020 A* conf
Type error feedback via analytic program repair.
PLDI
Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, Ranjit Jhala
2019 A* conf
FaCT: a DSL for timing-sensitive computation.
PLDI
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
2019 A* conf
IODINE: Verifying Constant-Time Execution of Hardware.
USENIX Security Symposium
Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
2019 A* conf
InFix: Automatically Repairing Novice Program Inputs.
ASE
Madeline Endres, Georgios Sakkas, Benjamin Cosman, Ranjit Jhala, Westley Weimer
2019 J jnl
Iodine: Verifying Constant-Time Execution of Hardware.
CoRR
Klaus von Gleissenthall, Rami Gökhan Kici, Deian Stefan, Ranjit Jhala
2019 A* conf
Lazy counterfactual symbolic execution.
PLDI
William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, Ruzica Piskac
2019 J jnl
Pretend synchrony: synchronous verification of asynchronous distributed programs.
Proc. ACM Program. Lang.
Klaus von Gleissenthall, Rami Gökhan Kici, Alexander Bakst, Deian Stefan, Ranjit Jhala
2019 J jnl
Program Synthesis by Type-Guided Abstraction Refinement.
CoRR
Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, Nadia Polikarpova
2018 J jnl
Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong).
J. Funct. Program.
Eric L. Seidel, Ranjit Jhala, Westley Weimer
2018 — ch.
Predicate Abstraction for Program Verification.
Handbook of Model Checking
Ranjit Jhala, Andreas Podelski, Andrey Rybalchenko
2018 J jnl
Refinement reflection: complete verification with SMT.
Proc. ACM Program. Lang.
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
2018 A* conf
Towards Verified, Constant-time Floating Point Operations.
CCS
Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, Deian Stefan
2017 J jnl
Deriving Law-Abiding Instances.
CoRR
Ryan G. Scott, Vikraman Choudhury, Ryan Newton, Niki Vazou, Ranjit Jhala
2017 — conf
FaCT: A Flexible, Constant-Time Programming Language.
SecDev
Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, Deian Stefan
2017 A* conf
Finding and Preventing Bugs in JavaScript Bindings.
IEEE Symposium on Security and Privacy
Fraser Brown, Shravan Narayan, Riad S. Wahby, Dawson R. Engler, Ranjit Jhala, Deian Stefan
2017 J jnl
Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis.
CoRR
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
2017 J jnl
Learning to blame: localizing novice type errors with data-driven diagnosis.
Proc. ACM Program. Lang.
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
2017 J jnl
Local Refinement Typing.
CoRR
Benjamin Cosman, Ranjit Jhala
2017 J jnl
Local refinement typing.
Proc. ACM Program. Lang.
Benjamin Cosman, Ranjit Jhala
2017 J jnl
Refinement Reflection: Complete Verification with SMT.
CoRR
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
2017 J jnl
Verifying distributed programs via canonical sequentialization.
Proc. ACM Program. Lang.
Alexander Bakst, Klaus von Gleissenthall, Rami Gökhan Kici, Ranjit Jhala
2016 J jnl
Dynamic Witnesses for Static Type Errors.
CoRR
Eric L. Seidel, Ranjit Jhala, Westley Weimer
2016 A conf
Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong).
ICFP
Eric L. Seidel, Ranjit Jhala, Westley Weimer
2016 J jnl
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131).
Dagstuhl Reports
Marco Gaboardi, Suresh Jagannathan, Ranjit Jhala, Stephanie Weirich
2016 B conf
Predicate Abstraction for Linked Data Structures.
VMCAI
Alexander Bakst, Ranjit Jhala
2016 A* conf
Printing floating-point numbers: a faster, always correct method.
POPL
Marc Andrysco, Ranjit Jhala, Sorin Lerner
2016 J jnl
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT).
CoRR
Niki Vazou, Ranjit Jhala
2016 J jnl
Refinement Types for TypeScript.
CoRR
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
2016 A* conf
Refinement types for TypeScript.
PLDI
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
2015 J jnl
Bounded Refinement Types.
CoRR
Niki Vazou, Alexander Bakst, Ranjit Jhala
2015 A conf
Bounded refinement types.
ICFP
Niki Vazou, Alexander Bakst, Ranjit Jhala
2015 J jnl
NSF expedition on variability-aware software: Recent results and contributions.
it Inf. Technol.
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
2015 A* conf
On Subnormal Floating Point and Abnormal Timing.
IEEE Symposium on Security and Privacy
Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, Hovav Shacham
2015 J jnl
Predicate Abstraction for Linked Data Structures.
CoRR
Alexander Bakst, Ranjit Jhala
2015 A conf
Trust, but Verify: Two-Phase Typing for Dynamic Languages.
ECOOP
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
2015 J jnl
Trust, but Verify: Two-Phase Typing for Dynamic Languages.
CoRR
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
2015 A conf
Type Targeted Testing.
ESOP
Eric L. Seidel, Niki Vazou, Ranjit Jhala
2014 J jnl
Abstractions from proofs.
ACM SIGPLAN Notices
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
2014 J jnl
From Safety To Termination And Back: SMT-Based Verification For Lazy Languages.
CoRR
Niki Vazou, Eric L. Seidel, Ranjit Jhala
2014 C conf
LiquidHaskell: experience with refinement types in the real world.
Haskell
Niki Vazou, Eric L. Seidel, Ranjit Jhala
2014 A conf
Refinement types for Haskell.
ICFP
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon L. Peyton Jones
2014 — conf
Refinement types for Haskell.
PLPV
Ranjit Jhala
2014 J jnl
Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271).
Dagstuhl Reports
Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, Peter Thiemann
2014 J jnl
Type Targeted Testing.
CoRR
Eric L. Seidel, Niki Vazou, Ranjit Jhala
2013 A conf
Abstract Refinement Types.
ESOP
Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala
2013 B ed.
Compiler Construction - 22nd International Conference, CC 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings
CC
Ranjit Jhala, Koen De Bosschere
2012 A* conf
CSolve: Verifying C with Liquid Types.
CAV
Patrick Maxim Rondon, Alexander Bakst, Ming Kawaguchi, Ranjit Jhala
2012 J jnl
Counterexample-guided Planning
CoRR
Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2012 A conf
Dependent types for JavaScript.
OOPSLA
Ravi Chugh, David Herman, Ranjit Jhala
2012 A* conf
Deterministic parallelism via liquid effects.
PLDI
Ming Kawaguchi, Patrick Maxim Rondon, Alexander Bakst, Ranjit Jhala
2012 A* conf
Nested refinements: a logic for duck typing.
POPL
Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala
2012 B ed.
Programming Languages and Systems - 10th Asian Symposium, APLAS 2012, Kyoto, Japan, December 11-13, 2012. Proceedings
APLAS
Ranjit Jhala, Atsushi Igarashi
2012 B conf
Software Verification with Liquid Types.
VMCAI
Ranjit Jhala
2012 — conf
Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs.
HotPower
Panagiotis Vekris, Ranjit Jhala, Sorin Lerner, Yuvraj Agarwal
2012 A* conf
Verifying GPU kernels by test amplification.
PLDI
Alan Leung, Manish Gupta, Yuvraj Agarwal, Rajesh Gupta, Ranjit Jhala, Sorin Lerner
2011 J jnl
Dependent Types for JavaScript
CoRR
Ravi Chugh, Ranjit Jhala
2011 A* conf
HMC: Verifying Functional Programs Using Abstract Interpreters.
CAV
Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
2011 A* conf
NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories.
ASPLOS
Joel Coburn, Adrian M. Caulfield, Ameen Akel, Laura M. Grupp, Rajesh K. Gupta, Ranjit Jhala, Steven Swanson
2011 — ed.
Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011
PLPV
Ranjit Jhala, Wouter Swierstra
2011 B conf
Software Verification with Liquid Types.
APLAS
Ranjit Jhala
2011 J jnl
System D: Dependent Dynamic Dictionaries
CoRR
Ravi Chugh, Patrick Maxim Rondon, Ranjit Jhala
2011 A* conf
Using Types for Software Verification.
CAV
Ranjit Jhala
2011 B ed.
Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings
VMCAI
Ranjit Jhala, David A. Schmidt
2010 A* conf
An empirical study of privacy-violating information flows in JavaScript web applications.
CCS
Dongseok Jang, Ranjit Jhala, Sorin Lerner, Hovav Shacham
2010 A* conf
Dsolve: Safety Verification via Liquid Types.
CAV
Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala
2010 — conf
Finding latent performance bugs in systems implementations.
SIGSOFT FSE
Charles Killian, Karthik Nagaraj, Salman Pervez, Ryan Braud, James W. Anderson, Ranjit Jhala
2010 A* conf
Low-level liquid types.
POPL
Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala
2010 J jnl
Refinement type inference via abstract interpretation
CoRR
Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko
2009 — conf
Building Distributed Systems Using Mace.
Peer-to-Peer Computing
Charles Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat
2009 J jnl
Software model checking.
ACM Comput. Surv.
Ranjit Jhala, Rupak Majumdar
2009 A* conf
Staged information flow for javascript.
PLDI
Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, Sorin Lerner
2009 A* conf
Type-based data structure verification.
PLDI
Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala
2009 A conf
Verifying Reference Counting Implementations.
TACAS
Michael Emmi, Ranjit Jhala, Eddie Kohler, Rupak Majumdar
2008 A* conf
Dataflow analysis for concurrent programs using datarace detection.
PLDI
Ravi Chugh, Jan Wen Voung, Ranjit Jhala, Sorin Lerner
2008 A conf
Deep typechecking and refactoring.
OOPSLA
Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
2008 A* conf
Liquid types.
PLDI
Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala
2007 A* conf
Array Abstractions from Proofs.
CAV
Ranjit Jhala, Kenneth L. McMillan
2007 — conf
Bounds Checking with Taint-Based Analysis.
HiPEAC
Weihaw Chuang, Satish Narayanasamy, Brad Calder, Ranjit Jhala
2007 J jnl
Interpolant-Based Transition Relation Approximation
CoRR
Ranjit Jhala, Kenneth L. McMillan
2007 J jnl
Interpolant-Based Transition Relation Approximation.
Log. Methods Comput. Sci.
Ranjit Jhala, Kenneth L. McMillan
2007 A* conf
Interprocedural analysis of asynchronous programs.
POPL
Ranjit Jhala, Rupak Majumdar
2007 Misc conf
Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (Awarded Best Paper).
NSDI
Charles Killian, James W. Anderson, Ranjit Jhala, Amin Vahdat
2007 A* conf
Lock allocation.
POPL
Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, Rupak Majumdar
2007 A* conf
Mace: language support for building distributed systems.
PLDI
Charles Killian, James W. Anderson, Ryan Braud, Ranjit Jhala, Amin Vahdat
2007 A* conf
OPIUM: Optimal Package Install/Uninstall Manager.
ICSE
Chris Tucker, David Shuffelton, Ranjit Jhala, Sorin Lerner
2007 — conf
RELAY: static race detection on millions of lines of code.
ESEC/SIGSOFT FSE
Jan Wen Voung, Ranjit Jhala, Sorin Lerner
2007 A conf
State of the Union: Type Inference Via Craig Interpolation.
TACAS
Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu
2007 J jnl
The software model checker Blast.
Int. J. Softw. Tools Technol. Transf.
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2006 A conf
A Practical and Complete Approach to Predicate Refinement.
TACAS
Ranjit Jhala, Kenneth L. McMillan
2006 — conf
Bit level types for high level reasoning.
SIGSOFT FSE
Ranjit Jhala, Rupak Majumdar
2006 B conf
Structural Invariants.
SAS
Ranjit Jhala, Rupak Majumdar, Ru-Gang Xu
2005 B conf
Checking Memory Safety with Blast.
FASE
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2005 A conf
Counterexample-guided Planning.
UAI
Krishnendu Chatterjee, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2005 A* conf
Interpolant-Based Transition Relation Approximation.
CAV
Ranjit Jhala, Kenneth L. McMillan
2005 — conf
Joining dataflow with predicates.
ESEC/SIGSOFT FSE
Jeffrey Fischer, Ranjit Jhala, Rupak Majumdar
2005 A* conf
Path slicing.
PLDI
Ranjit Jhala, Rupak Majumdar
2005 — conf
Permissive interfaces.
ESEC/SIGSOFT FSE
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2005 — conf
The BLAST Software Verification System.
SPIN
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004 A* conf
Abstractions from proofs.
POPL
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan
2004 — conf
An Eclipse Plug-in for Model Checking.
IWPC
Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004 A* conf
Generating Tests from Counterexamples.
ICSE
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004 C conf
Invited talk: the blast query language for software verification.
PEPM
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004 C conf
Invited talk: the blast query language for software verification.
PPDP
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004 A* conf
Race checking by context inference.
PLDI
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2004 B conf
The Blast Query Language for Software Verification..
SAS
Dirk Beyer, Adam Chlipala, Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2003 A* conf
Counterexample-Guided Control.
ICALP
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
2003 — conf
Extreme Model Checking.
Verification: Theory and Practice
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido
2003 — conf
Software Verification with BLAST.
SPIN
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre
2003 A* conf
Thread-Modular Abstraction Refinement.
CAV
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer
2002 A* conf
Lazy abstraction.
POPL
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Grégoire Sutre
2002 A* conf
Temporal-Safety Proofs for Systems Code.
CAV
Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer
2001 B conf
Compositional Methods for Probabilistic Systems.
CONCUR
Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala
2001 A* conf
Microarchitecture Verification by Compositional Model Checking.
CAV
Ranjit Jhala, Kenneth L. McMillan