Alexander J. Summers
where else to find them
no profile links on file
what they talk about
where they keep going back
- OOPSLA4 editions2020–2025
all 5 in the filters
on a stage with
all 18 in the filters
who talks about the same things
- Peter Müller28 talks
- Christoph Matheja8 talks
- Aurel Bílý5 talks
- Derek Dreyer35 talks
- Ralf Jung18 talks
- Michael Sammler16 talks
| title | conference | date |
|---|---|---|
| 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… | ||
| 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… | ||
| 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… | ||
| 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… | ||
| 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… | ||
| 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 | ||