Papers, awards, and milestones from the VQC Lab.
Prof. Tao is teaching CMSC 437: Quantum Software Lab (co-taught with Prof. Xiaodi Wu) and CMSC 858Y: Quantum Computing Systems in Spring 2026.
Our paper, with Hongzheng Zhu, Jason Nieh, Jianan Yao, and Ronghui Gu, was accepted to the 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2025).
The lab is actively developing several open-source formal verification projects, including ForShor (verified Shor's algorithm in Lean 4), ShorECDLP (verified resource estimates for Shor's algorithm against ECDSA), and Lean-QEC (end-to-end formalization of quantum error correction). See the Projects page for details.
Prof. Tao taught CMSC/PHYS 457: Introduction to Quantum Computing.
Runzhou Tao joined the Department of Computer Science at the University of Maryland as an Assistant Professor, and became a Fellow at the Joint Center for Quantum Information and Computer Science (QuICS).
With Haowei Deng, Yuxiang Peng, and Xiaodi Wu — accepted to the 51st ACM SIGPLAN Symposium on Principles of Programming Languages.
Advised by Ronghui Gu, completing a dissertation on formal verification for quantum and distributed systems.
With Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, and Ronghui Gu — accepted to the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation.
With Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu — accepted to the 28th ACM Symposium on Operating Systems Principles.
"DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols," with Jianan Yao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan, received the Jay Lepreau Best Paper Award at the 15th USENIX Symposium on Operating Systems Design and Implementation.
With Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, and Ronghui Gu — accepted to the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation.
With Matthew Fahrbach, Zhiyi Huang, and Morteza Zadimoghaddam — received the Best Paper Award at the 61st IEEE Annual Symposium on Foundations of Computer Science.
