Gowtham Kaki
where else to find them
bluesky:gowthamkaki.bsky.social
x:GowthamK
what they talk about
all 4 in the filters
where they keep going back
- OOPSLA3 editions2018–2025
on a stage with
all 8 in the filters
who talks about the same things
- Kartik Nagar6 talks
- Bor-Yuh Evan Chang11 talks
- Aseem Rastogi7 talks
- Constantin Enea14 talks
- Suresh Jagannathan16 talks
- Benjamin Delaware18 talks
| title | conference | date |
|---|---|---|
| Ravencheck: Effectively-Propositional Reasoning for Rust | SOAP 2026 | 2026-06-16 |
Ravencheck encodes a purely functional subset of Rust into EEPR with relational abstraction and calls SMT solvers (cvc5 or Z3) to get decidable, fast… | ||
| Bolt-On Strong Consistency: Specification, Implementation, and Verification | OOPSLA 2025 | 2025-10-16 |
Shows how consensus safety can be proved from local properties by implementing strong replication atop a causal weak store and verifying at the single-node… | ||
| Cyclic Message Histories for Automated Safety Verification of Distributed Algorithms | TPSA 2025 | 2025-01-19 |
Claims an automated verifier that uses a separation logic augmented with message histories and a goal-directed abstract interpretation to soundly… | ||
| Historia: Refuting Callback Reachability with Message-History Logics | OOPSLA 2023 | 2023-10-23 |
Defines message histories (sequences of boundary call-ins/callbacks) and a temporal message-history logic, implements a prototype verifier called Historia that… | ||
| Verifying Indistinguishability of Privacy-Preserving Protocols | OOPSLA 2023 | 2023-10-23 |
Library Waldo implements a middle ground between symbolic and computational models in F by modeling messages as bitstrings, using a tape to factor out… | ||
| Safe Replication through Bounded Concurrency Verification | OOPSLA 2018 | 2018-11-07 |
Automatic bounded verification explores executions under an unrestricted consistency model but with a finite concurrency bound and discovers concrete… | ||
| nothing matches | ||