Christoph Matheja
where else to find them
what they talk about
all 4 in the filters
where they keep going back
all 4 in the filters
on a stage with
all 14 in the filters
who talks about the same things
- Benjamin Lucien Kaminski14 talks
- Joost-Pieter Katoen14 talks
- Kevin Batz8 talks
- Alexander J. Summers13 talks
- Derek Dreyer35 talks
- Peter Müller28 talks
| title | conference | date |
|---|---|---|
| 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… | ||
| 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… | ||
| Modular Specification and Verification of Closures in Rust | SPLASH 2022 | 2022-12-05 |
Presents a concrete method to specify and verify Rust closures by encoding higher‑order concerns into a first-order encoding that SMT solvers (via Viper and… | ||
| Modular Specification and Verification of Closures in Rust | OOPSLA 2021 | 2021-10-17 |
A Prusti extension encodes higher-order Rust closures into first-order Viper logic and discharges verification conditions to Z3, claiming modular verification… | ||
| 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… | ||
| How Do Programmers Use Unsafe Rust? | OOPSLA 2020 | 2020-11-15 |
Paper analyzes unsafe Rust across the ecosystem using the Qrates framework and a modified compiler to compile and extract MIR from almost 29k compiled crates… | ||
| nothing matches | ||