54 citations · 255 across the 28 of their papers we have counts for
33 papers
Foundational Constraint Solving for Expressive Refinement Typing
Jam Kabeer Ali Khan, Petros Markopoulos, Nico Lehmann +1
SMT-based program verifiers are hamstrung by two problems: expressiveness, because predictable verification restricts to the boundaries of SMT decidability, and trust, because the…
Plainbook: Data Science, in Plain Language
Luca de Alfaro, Mathis Aubert, Ranjit Jhala +2
Jupyter Notebooks have become widely adopted in data science, as they allow the sharing of reproducible computational analysis. They are, however, accessible only to people who und…
Verifying the Rust Standard Library
Byron Cook, Remi Delmas, Zyad Hassan +9
Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic…
Complete first-order reasoning for functional programs
Adithya Murali, Lucas Peña, Ranjit Jhala +1
Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function…
Auditing Rust Crates Effectively
Lydia Zoghbi, David Thien, Ranjit Jhala +2
We introduce Cargo Scan, the first interactive program analysis tool designed to help developers audit third-party Rust code. Real systems written in Rust rely on thousands of tran…
Laurel: Unblocking Automated Verification with Large Language Models
Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala +2
Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of as…
Robust Constant-Time Cryptography
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi +4
The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory…
Mechanizing Refinement Types (extended)
Michael Borkowski, Niki Vazou, Ranjit Jhala
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verifica…
Flux: Liquid Types for Rust
Nico Lehmann, Adam Geller, Niki Vazou +1
We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manip…
Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version)
Anish Tondwalkar, Matthew Kolosick, Ranjit Jhala
Refinement types decorate types with assertions that enable automatic verification. Like assertions, refinements are limited to binders that are in scope, and hence, cannot express…
Isolation Without Taxation: Near Zero Cost Transitions for SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson +5
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to hard…
Solver-Aided Constant-Time Circuit Verification
Rami Gokhan Kici, Klaus v. Gleissenthall, Deian Stefan +1
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing t…
Refinement Types: A Tutorial
Ranjit Jhala, Niki Vazou
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable…
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus V. Gleissenthall +5
We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via specul…
Program Synthesis by Type-Guided Abstraction Refinement
Zheng Guo, Michael James, David Justo +4
We consider the problem of type-directed component based synthesis where, given a set of (typed) components and a query type, the goal is to synthesize a term that inhabits the que…
Iodine: Verifying Constant-Time Execution of Hardware
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan +1
To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing ch…
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury +4
We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the fu…
Learning to Blame: Localizing Novice Type Errors with Data-Driven Diagnosis
Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri +2
Localizing type errors is challenging in languages with global type inference, as the type checker must make assumptions about what the programmer intended to do. We introduce Nate…
Deriving Law-Abiding Instances
Ryan Scott, Vikraman Choudhury, Ryan Newton +2
Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. Bu…
Local Refinement Typing
Benjamin Cosman, Ranjit Jhala
We introduce the Fusion algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions…
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT)
Niki Vazou, Ranjit Jhala
Refinement Reflection turns your favorite programming language into a proof assistant by reflecting the code implementing a user-defined function into the function's (output) refin…
Dynamic Witnesses for Static Type Errors (or, Ill-Typed Programs Usually Go Wrong)
Eric L Seidel, Ranjit Jhala, Westley Weimer
Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample wi…
Refinement Types for TypeScript
Panagiotis Vekris, Benjamin Cosman, Ranjit Jhala
We present Refined TypeScript (RSC), a lightweight refinement type system for TypeScript, that enables static verification of higher-order, imperative programs. We develop a formal…
Bounded Refinement Types
Niki Vazou, Alexander Bakst, Ranjit Jhala
We present a notion of bounded quantification for refinement types and show how it expands the expressiveness of refinement typing by using it to develop typed combinators for: (1)…