Jinwoo Kim
where else to find them
no profile links on file
what they talk about
where they keep going back
all 4 in the filters
on a stage with
all 23 in the filters
who talks about the same things
- Loris D'Antoni17 talks
- Shaan Nagy3 talks
- Thomas Reps20 talks
- Roopsha Samanta10 talks
- Qinheping Hu3 talks
- Keith J.C. Johnson3 talks
| title | conference | date |
|---|---|---|
| Unleashing Zoned UFS: Cross-Layer Optimizations for Next-Generation Mobile Storage | FAST '26 | 2026-02-24 |
Zone UFS replaces page maps with zone-level mapping (zones are 1,056 MB, 16 KB pages) and implements a device-side GABM buffer manager, a driver/block-layer… | ||
| 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… | ||
| Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting | POPL 2025 | 2025-01-19 |
Archmage defines a memory model that uses lazy valuation for int→ptr casts so the integer keeps its value until a pointer interpretation is required, allowing… | ||
| 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… | ||
| Fair Operational Semantics | PLDI 2023 | 2023-06-17 |
Proposes FOS, an operational semantics that can encode arbitrary fairness notions and gives a concrete proof technique: a fairness counter that drops on bad… | ||
| 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… | ||
| 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 | ||