姓名：冯元

职称：教授

邮件：yuan_feng@tsinghua.edu.cn

教育背景

本科，清华大学应用数学系 1999年

博士，清华大学计算机科学与技术系 2004年

社会兼职

ACM Transactions on Software Engineering and Methodology: Associate Editor .

研究领域

量子模型检测、量子程序验证、量子通信并发系统

研究概况

量子模型检测：经典模型检测是对顺序程序、并发协议、硬件系统进行形式化验证的一种重要技术。由于其可机械化和可以提供诊断信息，在工业界得到了广泛应用。我们提出了两种不同的量子马尔代夫链模型，并系统发展了线性和分支两种量子时序逻辑公式的模型检测方法。2021年，受剑桥大学出版社邀请，我们出版了《Model Checking Quantum Systems: Principles and Algorithms》，对量子模型检测这一新兴的研究方向，特别是我们课题组在这方面的工作进行了系统梳理。这是量子模型检测领域第一本学术专著。

量子程序验证：Hoare逻辑是程序验证的逻辑基础，在程序设计方法学中处于核心地位。Hoare逻辑通过为命令式编程语言的所有程序结构定义合适的公理和推理规则，使得该语言下程序的正确性都可以进行(部分)自动化证明。我们建立了含经典变量的量子Hoare逻辑，证明其可靠性和相对完备性，并在文献中第一次成功的利用Hoare逻辑验证完整的Shor算法(ACM TQC 2021)。最近，我们进一步利用这种技术分别为不共享变量的量子并行程序(TCS 2022)、只含经典通信的分布式量子程序(ACM TOCL 2022)、含不确定性构造的量子程序(ASPLOS’23)设计了Hoare逻辑系统，并证明了它们的可靠性和相对完备性。

量子通信并发系统：量子通信和密码是量子信息领域目前最为成熟、在某些方面已经获得实际应用的技术。为了形式化描述量子通信网络、为量子网络软件和通信协议的形式化验证奠定理论基础，我们提出了量子进程代数qCCS (Information and Computation 2007)。更重要的是，我们成功的找到了一种刻画量子进程等价性的互模拟关系，并证明了其对于各种进程构造的同余性(POPL’11, ACM TOPLAS 2012)。我们后续的一系列工作，包括符号互模拟 (ACM TOCL 2014)、开互模拟(TCS 2012)和基于分布的互模拟(CONCUR 2015)等，极大的丰富了qCCS的基础理论，也增强了其描述和验证实际量子通信系统的能力。

学术成果

Books

[1]. M. Ying and Y. Feng. Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press, 2021.

Journal Articles

[2]. J. Ren, Y. Sui, X. Cheng, Y. Feng, J. Zhao. Dynamic Transitive Closure-Based Static Analysis through the Lens of Quantum Search. ACM Transactions on Software Engineering and Methodology, accepted (2024).

[3]. Y. Feng, and S. Li. Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. Information and Computation, 294: 105077 (2023).

[4]. X. Zhou, Y. Feng, and S. Li. Supervised Learning Enhanced Quantum Circuit Trans- formation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 42(2): 437-447 (2023).

[5]. Y. Feng, S. Li, and M. Ying. Verification of Distributed Quantum Programs. ACM Transactions on Computational Logic 23(3), 19:1-19:40 (2022).

[6]. X. Zhou, Y. Feng, and S. Li. Quantum Circuit Transformation: A Monte Carlo Tree Search Framework. ACM Transactions on Design Automation of Electronic Systems 27(6) 59:1-59:27 (2022).

[7]. X. Hong, X. Zhou, S. Li, Y. Feng, and M. Ying. A Tensor Network based Decision Diagram for Representation of Quantum Circuits. ACM Transactions on Design Automation of Electronic Systems 27 (6) 60:1-60:30 (2022).

[8]. M. Ying, L. Zhou, Y. Li, Y. Feng. A proof system for disjoint parallel quantum programs. Theoretical Computer Science 897: 164-184 (2022).

[9]. Y. Deng and Y. Feng. Formal Semantics of a Classical-Quantum Language. Theoretical Computer Science 913: 73-93 (2022).

[10]. C. Fu, A. Turrini, X. Huang, L. Song, Y. Feng, L. Zhang. Model Checking for Probabilistic Multiagent Systems under Uniform Schedulers. Journal of Computer Science and Technology (2022).

[11]. Y. Feng and M. Ying. Quantum Hoare logic with classical variables, ACM Transactions on Quantum Computing 2(4), 16:1-16:43 (2021).

[12]. X. Fu, ..., Y. Feng. Quingo: A Programming Framework for Heterogeneous Quantum- Classical Computing with NISQ Features, ACM Transactions on Quantum Computing 2(4), 19:1-19:37 (2021).

[13]. S. Li, X. Zhou, Y. Feng. Qubit Mapping Based on Subgraph Isomorphism and Filtered Depth-Limited Search, IEEE Transactions on Computers 70(11): 1777-1788 (2021).

[14]. M. Xu, C. Huang, Y. Feng. Measuring the constrained reachability in quantum Markov chains, Acta Informatica 58(6), 653-674 (2021).

[15]. W. Shi, Q. Cao, Y. Deng, H. Jiang, and Y. Feng. Symbolic Reasoning about Quantum Circuits in Coq, Journal of Computer Science and Technology 36 (6): 1291-1306 (2021).

[16]. M. Ying, Y. Feng, S. Ying. Optimal Policies for Quantum Markov Decision Processes. International Journal of Automation and Computing 18(3): 410-421 (2021).

[17]. X. Zhou, S. Li, Y. Feng. Quantum Circuit Transformation Based on Simulated Annealing and Heuristic Search, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39(12), 4683–4694 (2020).

Conference Papers

[18]. J. Guan, Y. Feng, A. Turrini, M. Ying. Measurement-based Verification of Quantum Markov Chains. Proceedings of the 36th International Conference on Computer Aided Verification (CAV’24), accepted.

[19]. A. Basheer, Y. Feng, C. Ferrie, and S. Li. Ansatz-Agnostic Exponential Resource Saving in Variational Quantum Algorithms Using Shallow Shadows. Proceedings of the 33rd International Joint Conference on Artificial Intelligence (IJCAI’24), accepted.

[20]. S. Li, K. Nguyen, Z. Clare and Y. Feng. Single-Qubit Gates Matter for Optimising Quantum Circuit Depth in Qubit Mapping. Proceedings of the 41st International Conference on Computer-Aided Design (ICCAD’23), 1-9.

[21]. Y. Feng and Y. Xu. Verification of nondeterministic quantum programs. Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’23)(3): 789-805 (2023).

[22]. A. Basheer, Y. Feng, C. Ferrie, and S. Li. Alternating Layered Variational Quantum Circuits Can Be Classically Optimized Efficiently Using Classical Shadows. Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI’23): 6770-6778 (2023).

[23]. L. Liu, K. Sun, C. Zhou, and Y. Feng. Two Views of Constrained Differential Privacy: Belief Revision and Update. Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI’23): 6450-6457 (2023).

[24]. X. Hong, Y. Feng, S. Li, and M. Ying. Equivalence Checking of Dynamic Quantum Circuits. Proceedings of the 41st International Conference on Computer-Aided Design (ICCAD’22), 127:1-127:8 (2022).

[25]. X. Hong, X. Zhou, S. Li, Y. Feng, and M. Ying. Approximate Equivalence Checking of Noisy Quantum Circuits. Proceedings of the 58th Design Automation Conference (DAC’21), 637-642 (2021).

[26]. X. Zhou, Y. Feng, S. Li. A Monte Carlo Tree Search Framework for Quantum Circuit Transformation. Proceedings of the 39th International Conference on Computer-Aided Design (ICCAD’20), 138:1-138:7 (2020).