Runzhou's Publications

(The authors of papers in theoretical computer science are listed by alphabetical order, whereas in other papers the authors are in contribution order.)

• A Case for Synthesis of Recursive Quantum Unitary Programs
  Haowei Deng*, Runzhou Tao*, Yuxiang Peng and Xiaodi Wu
  The 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), to appear

  
  

• Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
  Jianan Yao, Runzhou Tao, Ronghui Gu and Jason Nieh
  The 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), to appear

  
  

• A Formally Certified End-to-End Implementation of Shor’s Factorization Algorithm -
  Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks and Xiaodi Wu
  Proceedings of the National Academy of Sciences (PNAS) 120.21 (2023): e2218775120
  [arXiv]

  
  

• Solving SDP Faster: A Robust IPM Framework and Efficient Implementation
  Baihe Huang, Shunhua Jiang, Zhao Song, Runzhou Tao and Ruizhe Zhang
  The 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS 2022)
  [arXiv]

  
  

• DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols
  Jianan Yao, Runzhou Tao, Ronghui Gu and Jason Nieh
  The 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022)

  
  

• 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 and Ronghui Gu
  The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022)
  [arXiv] [code] [video]

  
  

• Symmetric Sparse Boolean Matrix Factorization and Applications
  Sitan Chen, Zhao Song, Runzhou Tao and Ruizhe Zhang
  The 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)
  [arXiv] [video]

  
  

• Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware -
  Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh and Ronghui Gu
  The 28th ACM Symposium on Operating Systems Principles (SOSP 2021)
  [paper] [code] [video]

  
  

• DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
  Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana and Gabriel Ryan
  The 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2021)
  Jay Lepreau Best Paper Award
  [paper] [code] [video]

  
  

• Gleipnir: Toward Practical Error Analysis for Quantum Programs
  Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong and Ronghui Gu
  The 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021)
  [arXiv] [paper] [code] [video]

  
  

• Edge-Weighted Online Bipartite Matching
  Matthew Fahrbach, Zhiyi Huang, Runzhou Tao and Morteza Zadimoghaddam
  The 61st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2020)
  Best Paper Award
  [arXiv] [paper] [video]

  
  

• Streaming Hardness of Unique Games
  Venkatesan Guruswami and Runzhou Tao
  The 22nd International Conference on Approximation Algorithms for Combinatorial Optimization Problems (APPROX 2019)
  [arXiv] [paper]

  
  

• Tight Competitive Ratios of Classic Matching Algorithms The Fully Online Model
  Zhiyi Huang, Binghui Peng, Zhihao Gavin Tang, Runzhou Tao, Xiaowei Wu and Yuhao Zhang
  The 30th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2019)
  [arXiv] [paper]

  
  

• A Case for Synthesis of Recursive Quantum Unitary Programs
  Haowei Deng*, Runzhou Tao*, Yuxiang Peng and Xiaodi Wu
  The 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), to appear

  
  

• A Formally Certified End-to-End Implementation of Shor’s Factorization Algorithm -
  Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks and Xiaodi Wu
  Proceedings of the National Academy of Sciences (PNAS) 120.21 (2023): e2218775120
  [arXiv]

  
  

• 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 and Ronghui Gu
  The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022)
  [arXiv] [code] [video]

  
  

• Gleipnir: Toward Practical Error Analysis for Quantum Programs
  Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong and Ronghui Gu
  The 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021)
  [arXiv] [paper] [code] [video]

  
  

• A Case for Synthesis of Recursive Quantum Unitary Programs
  Haowei Deng*, Runzhou Tao*, Yuxiang Peng and Xiaodi Wu
  The 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), to appear

  
  

• Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
  Jianan Yao, Runzhou Tao, Ronghui Gu and Jason Nieh
  The 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), to appear

  
  

• 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 and Ronghui Gu
  The 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022)
  [arXiv] [code] [video]

  
  

• Gleipnir: Toward Practical Error Analysis for Quantum Programs
  Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong and Ronghui Gu
  The 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021)
  [arXiv] [paper] [code] [video]

  
  

• Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
  Jianan Yao, Runzhou Tao, Ronghui Gu and Jason Nieh
  The 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), to appear

  
  

• DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols
  Jianan Yao, Runzhou Tao, Ronghui Gu and Jason Nieh
  The 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2022)

  
  

• Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware -
  Runzhou Tao, Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh and Ronghui Gu
  The 28th ACM Symposium on Operating Systems Principles (SOSP 2021)
  [paper] [code] [video]

  
  

• DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
  Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana and Gabriel Ryan
  The 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2021)
  Jay Lepreau Best Paper Award
  [paper] [code] [video]

  
  

(The authors are listed by alphabetical order.)

• Solving SDP Faster: A Robust IPM Framework and Efficient Implementation
  Baihe Huang, Shunhua Jiang, Zhao Song, Runzhou Tao and Ruizhe Zhang
  The 63rd IEEE Annual Symposium on Foundations of Computer Science (FOCS 2022)
  [arXiv]

  
  

• Symmetric Sparse Boolean Matrix Factorization and Applications
  Sitan Chen, Zhao Song, Runzhou Tao and Ruizhe Zhang
  The 13th Innovations in Theoretical Computer Science Conference (ITCS 2022)
  [arXiv] [video]

  
  

• Edge-Weighted Online Bipartite Matching
  Matthew Fahrbach, Zhiyi Huang, Runzhou Tao and Morteza Zadimoghaddam
  The 61st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2020)
  Best Paper Award
  [arXiv] [paper] [video]

  
  

• Streaming Hardness of Unique Games
  Venkatesan Guruswami and Runzhou Tao
  The 22nd International Conference on Approximation Algorithms for Combinatorial Optimization Problems (APPROX 2019)
  [arXiv] [paper]

  
  

• Tight Competitive Ratios of Classic Matching Algorithms The Fully Online Model
  Zhiyi Huang, Binghui Peng, Zhihao Gavin Tang, Runzhou Tao, Xiaowei Wu and Yuhao Zhang
  The 30th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2019)
  [arXiv] [paper]