Loris D'Antoni
where else to find them
github:lorisdanto
bluesky:lorisdanto.bsky.social
what they talk about
all 6 in the filters
where they keep going back
all 5 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Jinwoo Kim8 talks
- Thomas Reps20 talks
- Shaan Nagy3 talks
- Keith J.C. Johnson3 talks
- Nadia Polikarpova24 talks
- Roopsha Samanta10 talks
| title | conference | date |
|---|---|---|
| ChopChop: A Programmable Framework for Semantically Constraining the Output of Language(…) | POPL 2026 | 2026-01-11 |
ChopChop constructs constrained decoders that decide whether a token prefix has a completion satisfying a semantic spec by building prefix spaces and solving a… | ||
| Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers | POPL 2026 | 2026-01-11 |
Automates generation of MLIR integer abstract transformers by synthesizing small SSA programs (cut-style MCMC search) and composing them with… | ||
| LOUD: Synthesizing Strongest and Weakest Specifications | OOPSLA 2025 | 2025-10-16 |
The paper presents LOUD, a logic and algorithm that synthesizes strongest L-consequences (over-approximations) and weakest L-implicants (under-approximations)… | ||
| 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… | ||
| Invited Talk: Finding Good Programs by Avoiding Bad Ones | POPL 2025 | 2025-01-19 |
Shows that proving unrealizability — certifying that an entire grammar-derived search space contains no correct program — gives a practical pruning primitive… | ||
| Automatically Reducing Privilege for Access Control Policies | OOPSLA 2024 | 2024-10-20 |
Tool named IAM-PolicyRefiner synthesizes tighter AWS IAM policies from three months of real access logs, removing on average 77% of allowed actions and 88% of… | ||
| 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… | ||
| 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… | ||
| 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… | ||
| Verifying Infinitely Many Programs at Once | SAS 2023 | 2023-10-22 |
Proposes proving unrealizability for entire program search spaces by reducing synthesis-to-verification and by designing a Hoare-like logic that reasons about… | ||
| 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… | ||
| 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… | ||
| 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… | ||
| Automatic Repair of Regular Expressions | DLS 2019 | 2019-10-20 |
Tool enumerates AST templates with holes and uses automata-based and regex-based SMT encodings plus three pruning tests (Sigma/Top/Bottom) to synthesize… | ||
| nothing matches | ||