일시: 2025. 10. 22. (수요일), 오전 11시 ~ 오후 12시
장소: 제4공학관 D504

Speaker:Ji-Yong Shin, Ph.D. (Assistant Professor at the Khoury College of Computer Sciences at Northeastern University)

Title:How Formal Verification Leads to a New System Design: An Example from Reconfiguration Protocols for Distributed Consensus Algorithms

Abstract:

Despite recent advances, guaranteeing the correctness of large-scale distributed systems through formal verification remains a challenge. The atomic distributed object (ADO) was proposed in prior work to simplify the modeling and verification of strongly consistent distributed systems.

This talk demonstrates how the ADO model is extended to verify reconfiguration protocols for Raft and how verification insights inspired the design of ReCraft, a new reconfiguration protocol for Raft. The verification process revealed that quorum overlap is the key safety property for reconfiguration, leading to ReCraft's design that supports split, merge, and membership change operations—capabilities that did not exist or were less efficient in standard Raft. Through this work, we show how formal verification not only validates correctness but also drives the design of novel distributed protocols.

Bio:

Ji-Yong Shin is an Assistant Professor at the Khoury College of Computer Sciences at Northeastern University. He received his Ph.D. from Cornell University and was an Associate Research Scientist at Yale University. His research interests are designing systems, including distributed systems, cloud storage systems, and operating systems, and ensuring their correctness through formal verification.