Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 15-minute conference presentation from OOPSLA 2025 that introduces TraceLinking, a novel methodology for detecting deviations between formally verified distributed system designs and their implementations. Learn how researchers Finn Hackett and Ivan Beschastnikh from the University of British Columbia developed TraceLink to bridge the critical correctness gap that exists when compiling verified designs into actual running code. Discover how this automated approach maps execution traces to formal designs using TLA+ specifications, eliminating the manual effort required by previous trace validation methods. Examine the implementation of TraceLink for PGo, a compiler that transforms Modular PlusCal specifications into both TLA+ and Go code, and understand the formal semantics developed for interpreting execution traces as TLA+. Investigate the innovative templatization strategy that minimizes TLA+ tracing specification size and the novel "sidestep" trace path validation technique that accelerates bug detection with minimal overhead. Review evaluation results demonstrating TraceLink's effectiveness in finding 9 previously undetected bugs across various distributed systems, including a Raft key-value store implementation, with discoveries ranging from compiler bugs to deployment environment issues.
