Ranjit Jhala
where else to find them
what they talk about
all 11 in the filters
where they keep going back
- OOPSLA4 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski4 editions2022–2026
- POPL3 editions2021–2024
all 9 in the filters
on a stage with
all 48 in the filters
who talks about the same things
- Niki Vazou23 talks
- Derek Dreyer35 talks
- Michael Sammler16 talks
- Peter Müller28 talks
- Neel Krishnaswami10 talks
- Deepak Garg18 talks
| title | conference | date |
|---|---|---|
| Counterexample-Guided Inference of Modular Specifications | PLDI 2026 | 2026-06-15 |
A counterexample-guided algorithm automatically infers missing callee specifications so a modular verifier can prove a client function, parameterized by a… | ||
| On the Impact of Formal Verification on Software Development | OOPSLA 2025 | 2025-10-16 |
Auto-active verifier Dafny is studied via 14 interviews using grounded theory and the paper reports concrete pain points: SMT queries balloon to 5 GB of SMT… | ||
| Laurel: Unblocking Automated Verification with Large Language Models | OOPSLA 2025 | 2025-10-16 |
Laurel is a tool that generates missing Dafny assertions with LLMs by (1) inserting an assertion placeholder at the SMT error location and (2) supplying… | ||
| Robust Constant-Time Cryptography | PLDI 2025 | 2025-06-16 |
Defines an operational semantics and a new property Robust Constant Time (RCT) that is parameterized by attacker models (read gadgets, speculative read… | ||
| Auditing Rust Crates Effectively | PriSC 2025 (with POPL 2025) | 2025-01-20 |
Cargo Scan is an interactive analysis tool that inspects Rust crates, models side-effecting APIs, and propagates color-checked propagation across call sites so… | ||
| Laurel: Unblocking Automated Verification with Large Language Models | Dafny 2025 | 2025-01-19 |
Laurel uses large language models to auto-generate missing Dafny assertions and reports a >56.6% success rate on a new DafnyGym benchmark of lemmas extracted… | ||
| Refinement Type Refutations | OOPSLA 2024 | 2024-10-20 |
Systematically turns bidirectional refinement type rules into refutations and defines must-instantiation as the concrete set of term inhabitants that prove a… | ||
| Mechanizing Refinement Types | POPL 2024 | 2024-01-14 |
Introduces λRF, a core calculus that actually combines semantic subtyping with parametric polymorphism and proves soundness; develops two mechanizations: one… | ||
| Complete First-Order Reasoning for Properties of Functional Programs | OOPSLA 2023 | 2023-10-23 |
The paper proves that the unfolding-then-SMT procedure (USMT heuristic) used by Liquid Haskell, Leon and Stainless is sound and complete for the combined… | ||
| The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programmi... | ICFP 2023 | 2023-09-04 |
A new core calculus (VC) gives a small-step rewrite semantics for a deterministic functional logic language and implements unification and logical variables as… | ||
| Flux: Liquid Types for Rust | PLDI 2023 | 2023-06-17 |
Flux implements a novel refined type system for Rust as a plug-in to the Rust compiler that indexes mutable locations, introduces strong references for precise… | ||
| Robust Constant-Time Cryptography | PriSC 2023 | 2023-01-21 |
Constant-time is insufficient: code that avoids secret-dependent branches still leaks when keys live in memory or the application misbehaves. The work defines… | ||
| RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code | PLDI 2022 | 2022-06-13 |
RustHornBelt gives a formal, mechanized bridge between RustHorn-style automatic specs and RustBelt’s unsafe-code semantics: a Coq model built on Iris… | ||
| Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFI | POPL 2022 | 2022-01-16 |
Paper claims that adding static invariants lets sandboxed code use simple function calls instead of heavyweight wrappers, and implements this end-to-end. A… | ||
| STORM: Refinement Types for Secure Web Applications | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
Storm is a web framework that enforces data-dependent security policies at compile time via a Security Typed ORM that refines MVC types with logical… | ||
| Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade | POPL 2021 | 2021-01-17 |
Blade automatically finds data-flow paths from memory reads that can speculatively carry secrets to cache-leaking sinks, models them with a transient vs stable… | ||
| Digging for Fold: Synthesis-Aided API Discovery for Haskell | OOPSLA 2020 | 2020-11-15 |
A synthesis-backed search called Hoogle Plus indexes popular Haskell libraries and synthesizes compositions that match either a provided type or inferred types… | ||
| LiquidHaskell Refinement Types for Haskell | LambdaConf 2015 | 2015-05-22 |
Haskell has many delightful features, perhaps the most beloved of which is its type system which allows developers to specify and verify a variety of program… | ||
| nothing matches | ||