Tej Chajed
where else to find them
what they talk about
where they keep going back
- CoqPL2 editions2020–2021
all 6 in the filters
on a stage with
all 20 in the filters
who talks about the same things
nobody close enough yet
| title | conference | date |
|---|---|---|
| Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols | OSDI '25 | 2025-07-07 |
Basilisk is a Daphne compiler extension that automatically derives inductive invariants for distributed protocols using Provenance Invariants and an analysis… | ||
| Anvil: Verifying Liveness of Cluster Management Controllers | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
Anvil presents eventually stable reconciliation as a concise temporal liveness spec and provides a Rust framework that verifies controllers against it using… | ||
| Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline... | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
Claim: Kondo auto-generates and proves the network-level lemmas that make host-level invariants inductive, so developers only prove the synchronous proof about… | ||
| Verifying a concurrent file system with sequential reasoning | Dafny 2024 | 2024-01-14 |
A verified concurrent NFS server called DaisyNFS implements linearizability and crash durability by building file-system logic as atomic transactions atop a… | ||
| GoJournal: a verified, concurrent, crash-safe journaling system | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
GoJournal implements a verified, concurrent, crash-safe journaling API in Go and proves it in Coq with Perennial 2.0, using the Goose translator to model Go… | ||
| Record Updates in Coq | CoqPL 2021 | 2021-01-19 |
Library coq-record-update implements record setters by generating per-field setters with Ltac and plugging that Ltac into type class resolution so Coq runs the… | ||
| Record Updates in Coq | POPL 2021 | 2021-01-17 |
Implements record updates in Coq by generating setters via type class resolution and Ltac: a Ltac procedure solve_setter extracts an ada_expansion (eval hnf)… | ||
| Verifying Concurrent Go Code in Coq with Goose | CoqPL 2020 | 2020-01-25 |
A pipeline imports a practical subset of Go into Coq: a 2.5k‑line Go translator produces GooseLang programs that plug into Iris’s weakest‑precondition… | ||
| nothing matches | ||