Thomas Reps
where else to find them
linkedin:thomas-reps-437b2a69
what they talk about
all 7 in the filters
where they keep going back
- OOPSLA4 editions2022–2025
- POPL3 editions2021–2026
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
on a stage with
all 25 in the filters
who talks about the same things
- Loris D'Antoni17 talks
- Zachary Kincaid9 talks
- Işıl Dillig21 talks
- Jinwoo Kim8 talks
- Benjamin Delaware18 talks
- Sharon Shoham13 talks
| title | conference | date |
|---|---|---|
| SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…) | PLDI 2026 | 2026-06-15 |
SAQR-QC combines quantum Hoare-style inequalities with quantum abstract interpretation to trade exactness for speed: each reasoning step touches only local… | ||
| Context-Free-Language Reachability for Almost-Commuting Transition Systems | POPL 2026 | 2026-01-11 |
Proves that the Parikh-image machinery extends to an almost-commuting monoid, giving a polynomial-time procedure that produces a Presburger formula describing… | ||
| Scalable Equivalence Checking and Verification of Shallow Quantum Circuits | OOPSLA 2025 | 2025-10-16 |
Projection-Based Equivalence Checking constructs a constraint representation of a shallow circuit’s output as a conjunction of local projections that act on… | ||
| Software Model Checking via Summary-Guided Search | OOPSLA 2025 | 2025-10-16 |
GPS presents a concrete algorithm that interleaves directed testing with summary-guided search: it queries an SMT solver for models, uses a summary oracle… | ||
| Polynomial Bounds of CFLOBDDs against BDDs | OOPSLA 2025 | 2025-10-16 |
Shows that, given the same variable ordering, a CFLOBDD for any Boolean function is at most polynomially larger than a BDD: groupings count = O(b log b)… | ||
| Semantics of Sets of Programs | OOPSLA 2025 | 2025-10-16 |
Claims that compositional verification of simple properties for infinite program sets with loops requires tracking behaviors across unbounded executions, and… | ||
| Verifying Solutions to Semantics-Guided Synthesis Problems | PLDI 2025 | 2025-06-16 |
Framework reduces SemGuS verification to reduction to µCLP and classifies problems into SMT-encodable, CHC-encodable, and µCLP-encodable cases, implements… | ||
| Newtonian Program Analysis of Probabilistic Programs | OOPSLA 2024 | 2024-10-20 |
Presents NPA-PMA, an interprocedural framework that generalizes Newtonian Program Analysis to probabilistic, nondeterministic, and conditional branching by… | ||
| Automating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…) | OOPSLA 2024 | 2024-10-20 |
Presents Wuldo, the first implementation of an Unrealizability Logic (UL) proof synthesizer that decouples a fixed proof skeleton from parametric nonterminal… | ||
| Weighted Context-Free-Language Ordered Binary Decision Diagrams | OOPSLA 2024 | 2024-10-20 |
Introduces WCFLOBDDs, a hierarchically structured, weighted BDD with a procedure-call mechanism that is canonical and supports polynomial-time operations… | ||
| Synthesizing Formal Semantics from Executable Interpreters | OOPSLA 2024 | 2024-10-20 |
Given a grammar and a closed-box interpreter the system Synantic synthesizes inductive, syntax-directed semantics as Constrained-Horn Clauses via a CEGIS loop… | ||
| Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…) | OOPSLA 2024 | 2024-10-20 |
Claims that monotonicity of concrete semantics lets an SMT solver automatically generate sound and often tight interval abstractions for top‑down enumerative… | ||
| CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams | PLDI 2024 | 2024-06-24 |
CFLOBDDs present a compressed Boolean-function representation that can be exponentially smaller than BDDs and, versus the decision tree, offer a… | ||
| Synthesizing Specifications | OOPSLA 2023 | 2023-10-23 |
Algorithm synthesizes all best L-properties that are sound, precise (no strictly more precise L-property exists), and complete (no further L-properties can… | ||
| Unrealizability Logic | POPL 2023 | 2023-01-15 |
A Hoare-style proof system called unrealizability logic gives checkable proofs that a synthesis search space has no solution, overapproximating infinite sets… | ||
| Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Pro... | POPL 2023 | 2023-01-15 |
Presents a single-source–single-target algorithm that summarizes all source→target paths as path expressions and reduces InterDyck reachability to a… | ||
| Synthesizing Abstract Transformers | OOPSLA 2022 | 2022-12-05 |
Method synthesizes an abstract transformer from (i) a concrete semantics for op, (ii) an abstract domain A, and (iii) a DSL L, producing an AMURTH output that… | ||
| On the Complexity of Bidirected Interleaved Dyck-Reachability | POPL 2021 | 2021-01-17 |
Shows that bidirected InterDyck reachability is decidable for D1 ⊙ D1 and gives a concrete polynomial-time algorithm that computes all pairs reachable by… | ||
| Semantics-Guided Synthesis | POPL 2021 | 2021-01-17 |
Framework that takes a grammar, a big‑step semantics expressed as Constrained Horn Clauses, and examples or formulas as specs, then reduces synthesis to CHC… | ||
| nothing matches | ||