Noam Zilberstein
where else to find them
what they talk about
where they keep going back
all 4 in the filters
on a stage with
all 10 in the filters
who talks about the same things
- Alexandra Silva14 talks
- Joseph Tassarotti20 talks
- Alejandro Aguirre10 talks
- Simon Oddershede Gregersen9 talks
- John M. Li4 talks
- Sharon Shoham13 talks
| title | conference | date |
|---|---|---|
| Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…) | POPL 2026 | 2026-01-11 |
Introduces Probabilistic Concurrent Outcome Logic (pcOL) that composes concurrent separation logic, probabilistic separation logic, and Outcome Logic to prove… | ||
| Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching | TPSA 2025 | 2025-01-19 |
Presents Total Outcome Logic, a single logic that models program runs as maps from states to semiring-weighted outcomes and adds an explicit divergence outcome… | ||
| A Demonic Outcome Logic for Randomized Nondeterminism | POPL 2025 | 2025-01-19 |
Introduces Demonic Outcome Logic that models randomized programs with adversarial nondeterminism using the convex power set semantics, proving a distributive… | ||
| Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…) | OOPSLA 2024 | 2024-10-20 |
Outcome Separation Logic gives a single formalism that proves both correctness and incorrectness for programs with effects by making postconditions talk about… | ||
| Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasonin... | OOPSLA 2023 | 2023-10-23 |
Outcome Logic (OL) replaces a single postcondition with outcome-indexed assertions over sets of states, adds an outcome conjunction that composes reachable… | ||
| Applying Formal Verification to Microkernel IPC at Meta | CPP 2022 | 2022-01-17 |
Project uses Iris in Coq to verify the microkernel IPC algorithms (not the full C), proving correctness of two queues verified implemented as non‑blocking… | ||
| nothing matches | ||