Peter Müller
where else to find them
what they talk about
all 10 in the filters
where they keep going back
- OOPSLA6 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski4 editions2023–2026
all 8 in the filters
on a stage with
all 38 in the filters
who talks about the same things
- Thibault Dardinier9 talks
- Michael Sammler16 talks
- Derek Dreyer35 talks
- Alexander J. Summers13 talks
- Ranjit Jhala19 talks
- Lennard Gäher7 talks
| title | conference | date |
|---|---|---|
| Hyper Separation Logic | PLDI 2026 | 2026-06-15 |
Introduces a logic that supports hyperproperties with arbitrary quantifier alternation over heap programs, proves soundness in Isabelle/HOL, and ships reusable… | ||
| Modular Reasoning about Global Variables and Their Initialization | OOPSLA 2025 | 2025-10-16 |
Presents a verification method that lets clients assume global state only when three concrete conditions hold: module invariants are established… | ||
| Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing(…) | OOPSLA 2025 | 2025-10-16 |
Place Capability Graphs (PCG) present a concretely computable model of Rust ownership that is extracted from the compiler’s MIR and borrow-checker facts and… | ||
| A Refinement Methodology for Distributed Programs in Rust | OOPSLA 2025 | 2025-10-16 |
Presents a bottom-up refinement method that pairs guarded transition systems with a novel locally inductive invariants proof rule, implemented as a Rust… | ||
| Destabilizing Iris | PLDI 2025 | 2025-06-16 |
Adds Daenerys to Iris: a reworked resource layer that introduces unstable resources and an explicit frame modality, plus an unstable points-to and a… | ||
| Formal Foundations for Translational Separation Logic Verifiers | POPL 2025 | 2025-01-19 |
Provides a formal, mechanized framework that proves soundness of translational separation-logic verifiers by defining a core IVL with both operational and… | ||
| Hypra: A Deductive Program Verifier for Hyper Hoare Logic | OOPSLA 2024 | 2024-10-20 |
Claims the first automated deductive technique for arbitrary hyperproperties by encoding sets of program states explicitly into an intermediate language and… | ||
| Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…) | PLDI 2024 | 2024-06-24 |
Adds a per-run Isabelle certificate generator to an existing Viper→Boogie translation, proving that whenever the generated Boogie program has no failing… | ||
| Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties | PLDI 2024 | 2024-06-24 |
Logic lifts pre/postconditions to properties of arbitrary sets of states and claims to capture exactly the class of hyperproperties over terminating… | ||
| Compositional Reasoning about Advanced Iterator Patterns in Rust | IWACO 2023 | 2023-10-24 |
Methodology specifies and verifies Rust iterator chains that include closures with side effects, claiming precise modular reasoning about composition and… | ||
| Verification-Preserving Inlining in Automatic Separation Logic Verifiers | OOPSLA 2023 | 2023-10-23 |
Presents a provable criterion that makes bounded inlining safe for automatic separation-logic verifiers: a semantic condition (formalized in Isabelle/HOL) that… | ||
| Leveraging Rust Types for Program Synthesis | PLDI 2023 | 2023-06-17 |
First deductive synthesizer for safe Rust that uses Rust types to both shrink specifications and prune search, extracting programs from proofs and guaranteeing… | ||
| CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…) | PLDI 2023 | 2023-06-17 |
Claims a verification method that proves non‑interference for concurrent programs without any timing assumptions by requiring commutativity of updates only on… | ||
| 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… | ||
| Fractional Resources in Unbounded Separation Logic | OOPSLA 2022 | 2022-12-05 |
Defines a new semantics where assertions may temporarily use unbounded states that allow more-than-one permission during evaluation, then reimpose 0–1… | ||
| 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… | ||
| Rich Specifications for Ethereum Smart Contract Verification | OOPSLA 2021 | 2021-10-17 |
Defines a specification style that proves concrete guarantees: sound reasoning under arbitrary re-entrancy, modular verification of collaborating contracts… | ||
| Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verifica | OOPSLA 2020 | 2020-11-15 |
A methodology that links compositional refinement to separation-logic code verification and is fully formalized in Isabelle/HOL, yielding end-to-end trace… | ||
| 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… | ||
| High Performance Web Fonts | CSS-Minsk-JS 2018 | 2018-09-21 |
Self-host Google Fonts (or use Google Webfonts Helper) and add link rel=preload plus the CSS Font Loading API to force earlier downloads; that combination cuts… | ||
| High Performance Web Fonts | JSUnconf 2018 | 2018-04-21 |
Demo shows a concrete tool called subfont that pulls Google Fonts local, preloads them and applies font-display: swap, cutting the slow-path cost so first… | ||
| Check your links with hyperlink | JSUnconf 2018 | 2018-04-21 |
A small crawler called hyperlink walks a site recursively and reports actual failures not vague examples it flags broken links and permanent redirects verifies… | ||
| The Effect of Richer Visualizations on Code Comprehension | CHI 2016 | 2016-05-07 |
Compared standard syntax highlighting to two enriched presentations: medium: outlines and alternating background colors and high: icons replacing keywords plus… | ||
| nothing matches | ||