Chung-Kil Hur
where else to find them
no profile links on file
what they talk about
where they keep going back
- POPL3 editions2023–2026
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2026
all 5 in the filters
on a stage with
all 26 in the filters
who talks about the same things
- Minki Cho6 talks
- Dongjae Lee5 talks
- Youngju Song6 talks
- Taeyoung Yoon3 talks
- Michael Sammler16 talks
- Janggun Lee7 talks
| title | conference | date |
|---|---|---|
| CRIS: The Power of Imagination in Hybrid Verification | PLDI 2026 | 2026-06-15 |
Introduces CRIS, a framework that extends CCR with imaginary specifications—specs that intermix executable code and separation-logic assertions—to prove… | ||
| Coco: Corecursion with Compositional Heterogeneous Productivity | POPL 2026 | 2026-01-11 |
CHP claims it computes Compositional Heterogeneous Productivity relations that quantify how many outputs a component produces given input-level requirements… | ||
| Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness | OOPSLA 2025 | 2025-10-16 |
Lilo is a higher-order concurrent separation logic that adds a promise mechanism to reason about liveness: threads record a promise list and must consume… | ||
| CRIS: The power of imagination in specification and verification | CPP 2025 | 2025-01-20 |
CRIS introduces imaginary nondeterminism to let specifications include angelic choices and mix operational steps with separation logic, implemented on top of… | ||
| 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… | ||
| VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems | POPL 2025 | 2025-01-19 |
VeriRT provides an end-to-end framework that links abstract timed specs to assembly by (1) embedding low-level timing assumptions into operational semantics… | ||
| In-order execution nails every weak memory behavior | The Future of Weak Memory 2024 | 2024-01-15 |
Claims that an in-order, view-based model (an operational V‑IC1 semantics) captures all weak‑memory behaviors typically attributed to out‑of‑order models and… | ||
| 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… | ||
| Putting Weak Memory in Order via a Promising Intermediate Representation | PLDI 2023 | 2023-06-17 |
Claims an in-order source semantics for C/C++ that preserves all common compiler optimizations for non-atomics by compiling to an out-of-order IR with… | ||
| Conditional Contextual Refinement | POPL 2023 | 2023-01-15 |
A new refinement notion, Conditional Contextual Refinement (CCR), combines separation-logic pre/post conditions with transitive contextual refinement by… | ||
| nothing matches | ||