P. Madhusudan
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- OOPSLA3 editions2021–2025
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2026
on a stage with
all 18 in the filters
who talks about the same things
- Paul Krogmeier5 talks
- Adithya Murali6 talks
- Sharon Shoham13 talks
- Loris D'Antoni17 talks
- Thomas Reps20 talks
- Lucas Peña3 talks
| title | conference | date |
|---|---|---|
| Verification Modulo Tested Library Contracts | PLDI 2026 | 2026-06-15 |
Proposes a concrete pipeline that synthesizes method contracts and loop invariants by looping a generalizing CHC solver (ICE learners, decision trees, optional… | ||
| Synthesizing DSLs for Few-Shot Learning | OOPSLA 2025 | 2025-10-16 |
Constructs a precise formulation: given a base language L, a complexity measure (parse tree depth), and a metagrammar of candidate DSLs, decides whether a… | ||
| FO-Complete Program Verification for Heap Logics | OOPSLA 2025 | 2025-10-16 |
Claims a practical verification pipeline that achieves FO-Complete reasoning for heap logics by designing two logics — frame logic (FL) and SL-FL — with… | ||
| Predictable Verification using Intrinsic Definitions | PLDI 2024 | 2024-06-24 |
Proposes that defining heap structures with intrinsic definitions — auxiliary monadic maps plus local constraints — makes verification decidable and therefore… | ||
| Perception Contracts for Safety of ML-Enabled Systems | OOPSLA 2023 | 2023-10-23 |
Proposes Perception contracts — symbolic formulas that bound error between ground truth and perception estimates so a controller keeps a safety invariant — and… | ||
| Languages with Decidable Learning: A Meta-theorem | OOPSLA 2023 | 2023-10-23 |
Proves a concrete meta-theorem: if a symbolic language admits a facet interpreter whose extra memory is bounded by the fixed structure (independent of… | ||
| Complete First-Order Reasoning for Properties of Functional Programs | OOPSLA 2023 | 2023-10-23 |
The paper proves that the unfolding-then-SMT procedure (USMT heuristic) used by Liquid Haskell, Leon and Stainless is sound and complete for the combined… | ||
| Learning Formulas in Finite Variable Logics | POPL 2022 | 2022-01-16 |
Decision procedures synthesize separating sentences, query formulas, and terms over finite structures for finite-variable logics (FO^k), FO^k with nested or… | ||
| Synthesizing Contracts Correct Modulo a Test Generator | OOPSLA 2021 | 2021-10-17 |
Approach synthesizes tight contracts as decision trees and integrates a SyGuS-based learner (CVC4Sy) with the Pex test generator to get guarantees modulo a… | ||
| nothing matches | ||