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.
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