Ji-Yong Shin
where else to find them
no profile links on file
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
- OOPSLA2 editions2021–2024
on a stage with
all 6 in the filters
who talks about the same things
- Longfei Qiu5 talks
- Wolf Honore4 talks
- Jieung Kim4 talks
- Yoonseung Kim3 talks
- Jingqi Xiao2 talks
- Zhong Shao19 talks
| title | conference | date |
|---|---|---|
| SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…) | PLDI 2026 | 2026-06-15 |
SureDistrib defines probabilistic IO automata in the Rocq proof assistant and proves composition lemmas that let an abstract underlay be replaced by an… | ||
| LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols | PLDI 2025 | 2025-06-16 |
LiDO-DAG gives an abstract concurrent-object model and a refinement proof showing DAG protocols simulate leader-based consensus, implemented in Coq and… | ||
| AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects | OOPSLA 2024 | 2024-10-20 |
Claims a single abstraction, AdoB abstraction, unifies benign and Byzantine consensus and lets proofs be done by refinement; implements it in Coq with… | ||
| LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs | PLDI 2024 | 2024-06-24 |
LiDO is a refinement-ready model that adds an explicit pacemaker state so liveness of partially synchronous Byzantine SMR reduces to a few safety invariants… | ||
| Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D | OOPSLA 2021 | 2021-10-17 |
Presents a fault-aware ADO model that exposes partial failures (uncommitted but visible updates) while hiding protocol internals, and a verification stack… | ||
| nothing matches | ||