HTTP/2 200 server: GitHub.com content-type: text/html; charset=utf-8 last-modified: Sat, 09 Mar 2024 22:59:16 GMT access-control-allow-origin: * strict-transport-security: max-age=31556952 etag: W/"65ece9c4-1c75" expires: Sat, 17 Jan 2026 22:40:32 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: ADBE:25AD8:170086:1AF992:696C0D88 accept-ranges: bytes age: 0 date: Sat, 17 Jan 2026 22:30:32 GMT via: 1.1 varnish x-served-by: cache-bom-vanm7210072-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1768689032.481668,VS0,VE217 vary: Accept-Encoding x-fastly-request-id: 9029c1443aecc71cd0c19b47efd8e693a113c003 content-length: 2862

Yun-Sheng Chang

yschang@mit.edu

I’m a Ph.D. student in the PDOS group at MIT CSAIL. My advisors are Frans Kaashoek and Nickolai Zeldovich. I’m interested in formally verifying sophisticated software components; in particular, crash recovery, concurrency control, and distributed consensus. I believe program proofs are more than evidence of correctness—they should also help us understand why the program works. Better understanding then leads to clean abstractions, simpler code, optimization opportunities, and a happier life in general.

Before coming to MIT in 2021, I was a research assistant at Academia Sinica, Taiwan, where I worked with Yu-Fang Chen and Hsiang-Shang Ko.

I graduated in 2019 from National Tsing Hua University, Taiwan, where I got my B.S. and M.S. degrees in Electrical Engineering. My advisor was Ren-Shuo Liu.

Publications

• Verifying vMVCC, a high-performance transaction library using multi-version concurrency control.
  Yun-Sheng Chang, Ralf Jung, Upamanyu Sharma, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich.
  OSDI 2023
  paper / slides / code / proof

• Weakly durable high-performance transactions.
  Yun-Sheng Chang, Yu-Fang Chen, and Hsiang-Shang Ko.
  Preprint on arXiv
  paper

• Don’t look back, look into the future: Prescient data partitioning and migration for deterministic database systems.
  Yu-Shan Lin, Ching Tsai, Tz-Yu Lin, Yun-Sheng Chang, and Shan-Hung Wu.
  SIGMOD 2021
  paper

• Determinizing crash behavior with a verified snapshot-consistent flash translation layer.
  Yun-Sheng Chang, Yao Hsiao, Tzu-Chi Lin, Che-Wei Tsao, Chun-Feng Wu, Yuan-Hao Chang, Hsiang-Shang Ko, and Yu-Fang Chen.
  OSDI 2020
  paper / slides / code + proof

• OPTR: Order-preserving translation and recovery methods for SSDs with a standard block device interface.
  Yun-Sheng Chang and Ren-Shuo Liu.
  USENIX ATC 2019
  paper / slides / code

• VST: A virtual stress testing framework for discovering bugs in SSD flash-translation layers.
  Ren-Shuo Liu, Yun-Sheng Chang, and Chih-Wen Hung.
  ICCAD 2017
  paper / slides