Benjamin Lucien Kaminski
where else to find them
no profile links on file
what they talk about
where they keep going back
all 6 in the filters
on a stage with
all 17 in the filters
who talks about the same things
- Joost-Pieter Katoen14 talks
- Kevin Batz8 talks
- Christoph Matheja8 talks
- Gilles Barthe17 talks
- Joseph Tassarotti20 talks
- Alejandro Aguirre10 talks
| title | conference | date |
|---|---|---|
| A Taxonomy of Hoare-Like Logics | POPL 2025 | 2025-01-19 |
Classifies Hoare-like logics by giving a lattice of exact implications between transformers built from predicate transformers and a Kleene-algebra variant… | ||
| Partial Incorrectness Logic | TPSA 2025 | 2025-01-19 |
Defines "partial incorrectness" as an underapproximation of the strongest liberal postcondition that admits final states that are provably unreachable… | ||
| Hoare-Like Triples and Kleene Algebras with Top and Tests | Incorrectness 2024 | 2024-01-17 |
A taxonomy of program logics uses predicate transformers plus Kleene algebra with top and tests to show which Hoare-like triples are equationally definable… | ||
| Quantitative Weakest Hyper Pre | Incorrectness 2024 | 2024-01-17 |
A novel calculus defines a weakest hyper pre predicate transformer that predicts quantitative properties over initial sets or probability distributions for… | ||
| Belief Programming in Partially Observable Probabilistic Environments | LAFI 2024 | 2024-01-14 |
The work introduces P-BLIMP, a probabilistic belief-programming language with true/observe/infer statements that maintain belief states as probability… | ||
| 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… | ||
| 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… | ||
| Lower Bounds for Possibly Divergent Probabilistic Programs | OOPSLA 2023 | 2023-10-23 |
A proof rule called guard strengthening gives sound lower bounds for weakest preexpectations of possibly divergent probabilistic loops by replacing loop guards… | ||
| 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… | ||
| Quantitative strongest post: a calculus for reasoning about the flow of quantitative inform | OOPSLA 2022 | 2022-12-05 |
Presents a formal calculus that defines a quantitative strongest post and a strongest liberal post for nondeterministic programs with loops, where predicates… | ||
| 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… | ||
| A Pre-Expectation Calculus for Probabilistic Sensitivity | POPL 2021 | 2021-01-17 |
A relational pre-expectation calculus gives computable upper bounds on the Kantorovich lifting of output distributions, proved sound and (in cases) continuous… | ||
| 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 | ||