Kevin Batz
where else to find them
what they talk about
where they keep going back
all 5 in the filters
on a stage with
all 14 in the filters
who talks about the same things
- Joost-Pieter Katoen14 talks
- Benjamin Lucien Kaminski14 talks
- Christoph Matheja8 talks
- Gilles Barthe17 talks
- Joseph Tassarotti20 talks
- Rupak Majumdar21 talks
| title | conference | date |
|---|---|---|
| Weighted NetKAT: A Programming Language For Quantitative Network Verification | PLDI 2026 | 2026-06-15 |
Weighted NetKAT extends NetKAT to be parametric on a semiring and provides both denotational and operational semantics plus a compiler that turns programs into… | ||
| Verifying Sampling Algorithms via Distributional Invariants | LAFI 2026 | 2026-01-11 |
Framework treats probabilistic programs as distribution transformers and proves that the Fast Dice Roller and Fast Loaded Dice Roller produce the intended… | ||
| Caesar: A Verifier for Probabilistic Programs | Dafny 2024 | 2024-01-14 |
A deductive verifier called Caesar implements a probabilistic Boogie‑style pipeline: programs, specifications and proof rules are encoded in the quantitative… | ||
| Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr... | POPL 2024 | 2024-01-14 |
Shows a semi-automatic method that synthesizes memoryless deterministic (MD) strategies for probabilistic imperative programs by transforming guards via… | ||
| A Deductive Verification Infrastructure for Probabilistic Programs | OOPSLA 2023 | 2023-10-23 |
A deductive verification infrastructure implements an IVL (HAV/Halo) and a real-valued logic that encodes expectation-based specs, encodings for 12 loop proof… | ||
| A Calculus for Amortized Expected Runtimes | POPL 2023 | 2023-01-15 |
Develops a weakest-precondition-style aert calculus that composes the potential method with an extended ert for dynamic memory using runtime separation logic… | ||
| Weighted programming: a programming paradigm for specifying mathematical models | OOPSLA 2022 | 2022-12-05 |
Defines an imperative language with nondeterministic branching and weighted traces parameterized by a semiring, and gives a denotational semantics via a… | ||
| Relatively Complete Verification of Probabilistic Programs | POPL 2021 | 2021-01-17 |
Defines a compact grammar for non‑negative real‑valued assertions (rationals, addition, multiplication, truncated subtraction, guarded expectations, scaling… | ||
| nothing matches | ||