Theses & Reports

Instructions for submitting a technical report or thesis.

You can find technical reports published prior to 1990 archived here.

Title

Authors

Year

Ph.D. Thesis 2026 Building Reliable Distributed Systems: Bridging Specifications and Implementations Ding, Ding Abstract | PDF

Title: Building Reliable Distributed Systems: Bridging Specifications and Implementations

Candidate: Ding, Ding

Advisor(s): Aurojit Panda, Jinyang Li

Abstract:

Distributed systems such as etcd and ZooKeeper implement protocols that have been formally specified and verified. Yet developers use the protocol only as a reference and write the implementation by hand, so the specification that was verified is never directly connected to the code that runs.

This leaves two gaps. The first is faithfulness: the manual translation from specification to code often introduces mistakes, especially where developers add optimizations such as concurrency, causing the implementation to diverge from what the specification permits. The second is coverage: specifications can omit certain runtime details, such as which in-memory protocol state a crash destroys, and thus fail to specify how the implementation must handle those details to maintain correctness. Because of these two gaps, implementations of verified protocols continue to ship with safety bugs.

This dissertation bridges both gaps to involve the specifications into building the systems to enhance the correctness of the implementations. Ellsberg checks at runtime whether a deployed implementation's messages comply with its specification, requiring no access to internal state and no changes to the system being checked; it detects ten protocol implementation bugs across etcd, ZooKeeper, and RedisRaft. PostMark extends the specification to model volatile state lost in crashes, synthesizes a crash-consistency policy from the extended specification, and enforces that policy in existing implementations; in our experiments, it reduces etcd's average read latency by 63%.
Ph.D. Thesis 2026 Surface Parametrization and Remeshing with Guarantees Zhu, Leyi Abstract | PDF