~/talks

Joost-Pieter Katoen

what they talk about

where they keep going back

  • OOPSLA3 editions2022–2024
  • POPL3 editions2021–2024
  • LAFI2 editions2023–2026

all 5 in the filters

on a stage with

all 24 in the filters

who talks about the same things

titleconferencedate
Verifying Sampling Algorithms via Distributional InvariantsLAFI 20262026-01-11
Framework treats probabilistic programs as distribution transformers and proves that the Fast Dice Roller and Fast Loaded Dice Roller produce the intended…
Talk on
Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating FunctionsOOPSLA 20242024-10-20
Claims exact Bayesian posteriors for probabilistic programs with unbounded loops and conditioning by giving a denotational semantics based on extended…
Talk on
Caesar: A Verifier for Probabilistic ProgramsDafny 20242024-01-14
A deductive verifier called Caesar implements a probabilistic Boogie‑style pipeline: programs, specifications and proof rules are encoded in the quantitative…
Talk
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr...POPL 20242024-01-14
Shows a semi-automatic method that synthesizes memoryless deterministic (MD) strategies for probabilistic imperative programs by transforming guards via…
Talk on
A Deductive Verification Infrastructure for Probabilistic ProgramsOOPSLA 20232023-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…
Talk
Lower Bounds for Possibly Divergent Probabilistic ProgramsOOPSLA 20232023-10-23
A proof rule called guard strengthening gives sound lower bounds for weakest preexpectations of possibly divergent probabilistic loops by replacing loop guards…
Talk
Exact Probabilistic Inference Using Generating FunctionsLAFI 20232023-01-15
Generative-function semantics represent discrete program distributions as formal power series and use multiplicative inverses to get closed-form fractions…
Talk on
A Calculus for Amortized Expected RuntimesPOPL 20232023-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…
Talk
Weighted programming: a programming paradigm for specifying mathematical modelsOOPSLA 20222022-12-05
Defines an imperative language with nondeterministic branching and weighted traces parameterized by a semiring, and gives a denotational semantics via a…
Talk on
Gradient-Descent for Randomized Controllers under Partial ObservabilityVMCAI 20222022-01-16
Transforms partially observable controllers into a parametric Markov chain and computes exact derivatives by building a derived weighted automaton so gradients…
Talk on
Out of Control: Reducing Probabilistic Models by Control-State EliminationVMCAI 20222022-01-16
Title:[VMCAI'22] Out of Control: Reducing Probabilistic Models by Control-State Elimination Authors:Tobias Winkler, Johannes Lehmann, Joost-Pieter…
Talk
A Pre-Expectation Calculus for Probabilistic SensitivityPOPL 20212021-01-17
A relational pre-expectation calculus gives computable upper bounds on the Kantorovich lifting of output distributions, proved sound and (in cases) continuous…
Talk on
Relatively Complete Verification of Probabilistic ProgramsPOPL 20212021-01-17
Defines a compact grammar for non‑negative real‑valued assertions (rationals, addition, multiplication, truncated subtraction, guarded expectations, scaling…
Talk on
~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.