Ranjit Jhala

Orcid: 0000-0002-1802-9421

Affiliations:
  • University of California, San Diego, USA


According to our database1, Ranjit Jhala authored at least 118 papers between 2001 and 2024.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2021, "For contributions to software verification".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Mechanizing Refinement Types.
Proc. ACM Program. Lang., January, 2024

2023
Complete First-Order Reasoning for Properties of Functional Programs.
Proc. ACM Program. Lang., October, 2023

The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming.
Proc. ACM Program. Lang., August, 2023

Flux: Liquid Types for Rust.
Proc. ACM Program. Lang., 2023

Robust Constant-Time Cryptography.
CoRR, 2023

2022
Seq2Parse: neurosymbolic parse error repair.
Proc. ACM Program. Lang., 2022

Isolation without taxation: near-zero-cost transitions for WebAssembly and SFI.
Proc. ACM Program. Lang., 2022

Mechanizing Refinement Types (extended).
CoRR, 2022

Flux: Liquid Types for Rust.
CoRR, 2022

Embedded Domain Specific Verifiers.
Proceedings of the Principles of Systems Design, 2022

2021
Automatically eliminating speculative leaks from cryptographic code with blade.
Proc. ACM Program. Lang., 2021

Refinement Types: A Tutorial.
Found. Trends Program. Lang., 2021

mist: Refinements of Futures Past (Artifact).
Dagstuhl Artifacts Ser., 2021

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version).
CoRR, 2021

Isolation Without Taxation: Near Zero Cost Transitions for SFI.
CoRR, 2021

Solver-Aided Constant-Time Circuit Verification.
CoRR, 2021

RAPID: checking API usage for the cloud in the cloud.
Proceedings of the ESEC/FSE '21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2021

STORM: Refinement Types for Secure Web Applications.
Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 2021

Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types.
Proceedings of the 35th European Conference on Object-Oriented Programming, 2021

Solver-Aided Constant-Time Hardware Verification.
Proceedings of the CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15, 2021

2020
Digging for fold: synthesis-aided API discovery for Haskell.
Proc. ACM Program. Lang., 2020

Program synthesis by type-guided abstraction refinement.
Proc. ACM Program. Lang., 2020

Automatically Eliminating Speculative Leaks With Blade.
CoRR, 2020

Block public access: trust safety verification of access control policies.
Proceedings of the ESEC/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2020

PABLO: Helping Novices Debug Python Code Through Data-Driven Fault Localization.
Proceedings of the 51st ACM Technical Symposium on Computer Science Education, 2020

Type error feedback via analytic program repair.
Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2020

Stratified Abstraction of Access Control Policies.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019
Pretend synchrony: synchronous verification of asynchronous distributed programs.
Proc. ACM Program. Lang., 2019

IODINE: Verifying Constant-Time Execution of Hardware.
Proceedings of the 28th USENIX Security Symposium, 2019

Lazy counterfactual symbolic execution.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

FaCT: a DSL for timing-sensitive computation.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

InFix: Automatically Repairing Novice Program Inputs.
Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

2018
Predicate Abstraction for Program Verification.
Proceedings of the Handbook of Model Checking., 2018

Refinement reflection: complete verification with SMT.
Proc. ACM Program. Lang., 2018

Dynamic witnesses for static type errors (or, Ill-Typed Programs Usually Go Wrong).
J. Funct. Program., 2018

Towards Verified, Constant-time Floating Point Operations.
Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

2017
Learning to blame: localizing novice type errors with data-driven diagnosis.
Proc. ACM Program. Lang., 2017

Local refinement typing.
Proc. ACM Program. Lang., 2017

Verifying distributed programs via canonical sequentialization.
Proc. ACM Program. Lang., 2017

Deriving Law-Abiding Instances.
CoRR, 2017

Finding and Preventing Bugs in JavaScript Bindings.
Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017

FaCT: A Flexible, Constant-Time Programming Language.
Proceedings of the IEEE Cybersecurity Development, SecDev 2017, Cambridge, MA, USA, 2017

2016
Language Based Verification Tools for Functional Programs (Dagstuhl Seminar 16131).
Dagstuhl Reports, 2016

Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT).
CoRR, 2016

Dynamic Witnesses for Static Type Errors.
CoRR, 2016

Predicate Abstraction for Linked Data Structures.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Printing floating-point numbers: a faster, always correct method.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Refinement types for TypeScript.
Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2016

2015
NSF expedition on variability-aware software: Recent results and contributions.
it Inf. Technol., 2015

On Subnormal Floating Point and Abnormal Timing.
Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

Bounded refinement types.
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Type Targeted Testing.
Proceedings of the Programming Languages and Systems, 2015

Trust, but Verify: Two-Phase Typing for Dynamic Languages.
Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014
Abstractions from proofs.
ACM SIGPLAN Notices, 2014

Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271).
Dagstuhl Reports, 2014

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages.
CoRR, 2014

Refinement types for Haskell.
Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, 2014

Refinement types for Haskell.
Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

LiquidHaskell: experience with refinement types in the real world.
Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

2013
Abstract Refinement Types.
Proceedings of the Programming Languages and Systems, 2013

2012
Nested refinements: a logic for duck typing.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

Verifying GPU kernels by test amplification.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Deterministic parallelism via liquid effects.
Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2012

Towards Verifying Android Apps for the Absence of No-Sleep Energy Bugs.
Proceedings of the 2012 Workshop on Power-Aware Computing Systems, HotPower'12, 2012

Dependent types for JavaScript.
Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2012

CSolve: Verifying C with Liquid Types.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Dependent Types for JavaScript
CoRR, 2011

System D: Dependent Dynamic Dictionaries
CoRR, 2011

HMC: Verifying Functional Programs Using Abstract Interpreters.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

Using Types for Software Verification.
Proceedings of the Computer Aided Verification - 23rd International Conference, 2011

NV-Heaps: making persistent objects fast and safe with next-generation, non-volatile memories.
Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, 2011

Software Verification with Liquid Types.
Proceedings of the Programming Languages and Systems - 9th Asian Symposium, 2011

2010
Refinement type inference via abstract interpretation
CoRR, 2010

Finding latent performance bugs in systems implementations.
Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

Low-level liquid types.
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

An empirical study of privacy-violating information flows in JavaScript web applications.
Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

Dsolve: Safety Verification via Liquid Types.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

2009
Software model checking.
ACM Comput. Surv., 2009

Verifying Reference Counting Implementations.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Type-based data structure verification.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Staged information flow for javascript.
Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2009

Building Distributed Systems Using Mace.
Proceedings of the Proceedings P2P 2009, 2009

2008
Liquid types.
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

Dataflow analysis for concurrent programs using datarace detection.
Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, 2008

Deep typechecking and refactoring.
Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, 2008

2007
The software model checker Blast.
Int. J. Softw. Tools Technol. Transf., 2007

Interpolant-Based Transition Relation Approximation.
Log. Methods Comput. Sci., 2007

State of the Union: Type Inference Via Craig Interpolation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

RELAY: static race detection on millions of lines of code.
Proceedings of the 6th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2007

Interprocedural analysis of asynchronous programs.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Lock allocation.
Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2007

Mace: language support for building distributed systems.
Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, 2007

Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (Awarded Best Paper).
Proceedings of the 4th Symposium on Networked Systems Design and Implementation (NSDI 2007), 2007

OPIUM: Optimal Package Install/Uninstall Manager.
Proceedings of the 29th International Conference on Software Engineering (ICSE 2007), 2007

Bounds Checking with Taint-Based Analysis.
Proceedings of the High Performance Embedded Architectures and Compilers, 2007

Array Abstractions from Proofs.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
A Practical and Complete Approach to Predicate Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Bit level types for high level reasoning.
Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006

Structural Invariants.
Proceedings of the Static Analysis, 13th International Symposium, 2006

2005
Counterexample-guided Planning.
Proceedings of the UAI '05, 2005

The BLAST Software Verification System.
Proceedings of the Model Checking Software, 2005

Permissive interfaces.
Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005

Joining dataflow with predicates.
Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005

Path slicing.
Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, 2005

Checking Memory Safety with Blast.
Proceedings of the Fundamental Approaches to Software Engineering, 2005

2004
The Blast Query Language for Software Verification..
Proceedings of the Static Analysis, 11th International Symposium, 2004

Race checking by context inference.
Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation 2004, 2004

Invited talk: the blast query language for software verification.
Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-based Program Manipulation, 2004

An Eclipse Plug-in for Model Checking.
Proceedings of the 12th International Workshop on Program Comprehension (IWPC 2004), 2004

Generating Tests from Counterexamples.
Proceedings of the 26th International Conference on Software Engineering (ICSE 2004), 2004

2003
Software Verification with BLAST.
Proceedings of the Model Checking Software, 2003

Counterexample-Guided Control.
Proceedings of the Automata, Languages and Programming, 30th International Colloquium, 2003

Thread-Modular Abstraction Refinement.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

Extreme Model Checking.
Proceedings of the Verification: Theory and Practice, 2003

2002
Lazy abstraction.
Proceedings of the Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002

Temporal-Safety Proofs for Systems Code.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
Compositional Methods for Probabilistic Systems.
Proceedings of the CONCUR 2001, 2001

Microarchitecture Verification by Compositional Model Checking.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001


  Loading...