Publications

All Operating Systems Programming Languages Quantum Computing Theory

Quantum Virtual Machines

Runzhou Tao, Hongzheng Zhu, Jason Nieh, Jianan Yao, Ronghui Gu

OSDI 2025

paper
A Case for Synthesis of Recursive Quantum Unitary Programs

Haowei Deng, Runzhou Tao, Yuxiang Peng, Xiaodi Wu

POPL 2024

arXiv code
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh

POPL 2024
A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm

Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, Xiaodi Wu

PNAS 120.21 (2023): e2218775120

arXiv
Solving SDP Faster: A Robust IPM Framework and Efficient Implementation

Baihe Huang, Shunhua Jiang, Zhao Song, Runzhou Tao, Ruizhe Zhang

FOCS 2022

arXiv
Symmetric Sparse Boolean Matrix Factorization and Applications

Sitan Chen, Zhao Song, Runzhou Tao, Ruizhe Zhang

ITCS 2022

arXiv video
DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh

OSDI 2022

paper
Giallar: Push-button Verification for the Qiskit Quantum Compiler

Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu

PLDI 2022

arXiv code video
Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware

Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, Ronghui Gu

SOSP 2021

paper code video
DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols Jay Lepreau Best Paper Award

Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, Gabriel Ryan

OSDI 2021

paper code video
Gleipnir: Toward Practical Error Analysis for Quantum Programs

Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, Ronghui Gu

PLDI 2021

arXiv paper code video
Edge-Weighted Online Bipartite Matching Best Paper Award

Matthew Fahrbach, Zhiyi Huang, Runzhou Tao, Morteza Zadimoghaddam

FOCS 2020

arXiv paper video
Streaming Hardness of Unique Games

Venkatesan Guruswami, Runzhou Tao

APPROX 2019

arXiv
Tight Competitive Ratios of Classic Matching Algorithms in the Fully Online Model

Zhiyi Huang, Binghui Peng, Zhihao Gavin Tang, Runzhou Tao, Xiaowei Wu, Yuhao Zhang

SODA 2019

arXiv

Quantum Virtual Machines

A Case for Synthesis of Recursive Quantum Unitary Programs

Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions

A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm

Solving SDP Faster: A Robust IPM Framework and Efficient Implementation

Symmetric Sparse Boolean Matrix Factorization and Applications

DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols

Giallar: Push-button Verification for the Qiskit Quantum Compiler

Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware

DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols Jay Lepreau Best Paper Award

Gleipnir: Toward Practical Error Analysis for Quantum Programs

Edge-Weighted Online Bipartite Matching Best Paper Award

Streaming Hardness of Unique Games

Tight Competitive Ratios of Classic Matching Algorithms in the Fully Online Model