Tobias Grosser
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- OOPSLA3 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
all 6 in the filters
on a stage with
all 40 in the filters
who talks about the same things
- Arjun Pitchanathan3 talks
- Theodoros Theodoridis5 talks
- Jonathan Ragan-Kelley12 talks
- Adam Chlipala23 talks
- Amir Shaikhha15 talks
- Fredrik Kjolstad14 talks
| title | conference | date |
|---|---|---|
| Interactive Bit Vector Reasoning using Verified Bitblasting | OOPSLA 2025 | 2025-10-16 |
A verified bit-blasting pipeline called bv_decide tactic compiles Lean bitvector goals to AIGs, converts to CNF, calls an external SAT solver that emits… | ||
| Compressed and Parallelized Structured Tensor Algebra | OOPSLA 2025 | 2025-10-16 |
DASTAC generates compressed linear indexes from polyhedral structure using the Barvinok algorithm, emits affine code and parallel loops via MLIR, and adds… | ||
| Certified Decision Procedures for Width-Independent Bitvector Predicates | OOPSLA 2025 | 2025-10-16 |
Mechanized, executable decision procedures in Lean for width-independent bitvectors that formalize k-induction, automata reachability, emptiness checking and… | ||
| eqsat: An Equality Saturation Dialect for Non-destructive Rewriting | EGRAPHS 2025 | 2025-06-16 |
An MLIR-based e-graph representation called eqsat dialect encodes e-classes and e-nodes as MLIR ops and uses MLIR graph regions to express cycles so equality… | ||
| First-Class Verification Dialects for MLIR | PLDI 2025 | 2025-06-16 |
Adds semantics as first-class MLIR dialects and a pipeline that lowers compiler IRs through high-level memory and undefined-behavior dialects to an SMT… | ||
| Panel: Compilation Frameworks | Sparse 2024 | 2024-06-25 |
Discussion shows a concrete path for quantify over bitwidth proofs: Lean supports quantifying bitwidth but only offers high‑performance automation for fixed… | ||
| Design DSLs with xDSL | Sparse 2024 | 2024-06-25 |
xDSL is a Python reimplementation of MLIR that prioritizes approachability and textual IR interoperability, letting teams define ops and types in minutes and… | ||
| Falcon: A Scalable Analytical Cache Model | PLDI 2024 | 2024-06-24 |
Falcon builds a scalable analytical model for LRU cache miss rates using polyhedral dependence analysis and by splitting analysis to avoid blowup; it evaluates… | ||
| Guided Equality Saturation | POPL 2024 | 2024-01-14 |
Guided equality saturation splits a hard e-graph search into sequences of smaller equality-saturation runs guided by human-provided intermediate sketches… | ||
| Cross-Domain Compilation: Exploiting Synergies Across the CS Community | VMIL 2021 | 2021-10-17 |
Argues that MLIR turns many bespoke compilers into composable pieces and shows concrete work: a fast polyhedral math library for Presburger sets, a… | ||
| FPL: Fast Presburger Arithmetic through Transprecision | OOPSLA 2021 | 2021-10-17 |
A new C++ Presburger library lives inside MLIR and targets real polyhedral workloads: a benchmark of over 1,000,000 extracted Presburger cases shows… | ||
| Fast Linear Programming through Transprecision Computing on Small and Sparse Data | OOPSLA 2020 | 2020-11-15 |
Analyzes ~500,000 simplex tableaux from Polly PPCG and HayStack and finds >99% of coefficients <9 bits, medians of 18 columns and 84% sparsity, with rare… | ||
| nothing matches | ||