冯元

冯元

教授

清华大学

研究概况

量子模型检测：经典模型检测是对顺序程序、并发协议、硬件系统进行形式化验证的一种重要技术。由于其可机械化和可以提供诊断信息，在工业界得到了广泛应用。我们提出了两种不同的量子马尔代夫链模型，并系统发展了线性和分支两种量子时序逻辑公式的模型检测方法。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的基础理论，也增强了其描述和验证实际量子通信系统的能力。

研究方向

  • 量子模型检测

  • 量子程序验证

  • 量子通信并发系统

教育经历

  • 本科 · 清华大学应用数学系

    1999

  • 博士 · 清华大学计算机科学与技术系

    2004

最新发表

Yuan Feng, Li Zhou, Yingte Xu, Xiaoquan Xu (2025). Refinement calculus of quantum programs with projective assertions. ACM Trans. Softw. Eng. Methodol..

引用 DOI URL

Afrad Basheer, Yuan Feng, Christopher Ferrie, Sanjiang Li, Hakop Pashayan (2025). On the Trainability and Classical Simulability of Learning Matrix Product States Variationally. Proceedings of the AAAI Conference on Artificial Intelligence.

引用 DOI URL

Yuan Feng, Li Zhou (2025). Refinement orders for quantum programs.

引用 arXiv URL

Jiawei Ren, Yulei Sui, Xiao Cheng, Yuan Feng, Jianjun Zhao (2024). Dynamic Transitive Closure-based Static Analysis through the Lens of Quantum Search. ACM Trans. Softw. Eng. Methodol..

引用 DOI URL

Sanjiang Li, Xiangzhen Zhou, Yuan Feng (2024). Benchmarking Quantum Circuit Transformation with QKNOB Circuits.

引用 arXiv URL

Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, Mingsheng Ying (2024). Equivalence Checking of Parameterised Quantum Circuits.

引用 arXiv URL

Chen Fu, Andrea Turrini, Xiaowei Huang, Lei Song, Yuan Feng, Li-Jun Zhang (2023). Model Checking for Probabilistic Multiagent Systems. Journal of Computer Science and Technology.

引用 DOI URL

Afrad Basheer, Yuan Feng, Christopher Ferrie, Sanjiang Li (2023). Alternating Layered Variational Quantum Circuits Can Be Classically Optimized Efficiently Using Classical Shadows. Proceedings of the AAAI Conference on Artificial Intelligence.

引用 DOI URL

Likang Liu, Keke Sun, Chunlai Zhou, Yuan Feng (2023). Two Views of Constrained Differential Privacy: Belief Revision and Update. Proceedings of the AAAI Conference on Artificial Intelligence.

引用 DOI URL

Yuan Feng, Sanjiang Li (2023). Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. Information and Computation.

引用 DOI URL

Afrad Basheer, Yuan Feng, Christopher Ferrie, Sanjiang Li (2023). Ansatz-Agnostic Exponential Resource Saving in Variational Quantum Algorithms Using Shallow Shadows.

引用 arXiv URL

Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, Chia-Shun Yeh, Mingsheng Ying (2023). Decision Diagrams for Symbolic Verification of Quantum Circuits. 2023 IEEE International Conference on Quantum Computing and Engineering (QCE).

引用 DOI

Sanjiang Li, Ky Dan Nguyen, Zachary Clare, Yuan Feng (2023). Single-Qubit Gates Matter for Optimising Quantum Circuit Depth in Qubit Mapping. 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD).

引用 DOI

Xiangzhen Zhou, Yuan Feng, Sanjiang Li (2023). Supervised Learning Enhanced Quantum Circuit Transformation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.

引用 DOI

Yuan Feng, Yingte Xu (2023). Verification of Nondeterministic Quantum Programs. Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3.

引用 DOI URL

Xin Hong, Xiangzhen Zhou, Sanjiang Li, Yuan Feng, Mingsheng Ying (2022). A Tensor Network based Decision Diagram for Representation of Quantum Circuits. ACM Trans. Des. Autom. Electron. Syst..

引用 DOI URL

Xiangzhen Zhou, Yuan Feng, Sanjiang Li (2022). Quantum Circuit Transformation: A Monte Carlo Tree Search Framework. ACM Trans. Des. Autom. Electron. Syst..

引用 DOI URL

Yuan Feng, Sanjiang Li, Mingsheng Ying (2022). Verification of Distributed Quantum Programs. ACM Trans. Comput. Logic.

引用 DOI URL

Mingsheng Ying, Li Zhou, Yangjia Li, Yuan Feng (2022). A proof system for disjoint parallel quantum programs. Theoretical Computer Science.

引用 DOI URL

Xin Hong, Yuan Feng, Sanjiang Li, Mingsheng Ying (2022). Equivalence Checking of Dynamic Quantum Circuits. Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design.

引用 DOI URL

Yuxin Deng, Yuan Feng (2022). Formal semantics of a classical-quantum language. Theoretical Computer Science.

引用 DOI URL

Ming Xu, Cheng-Chao Huang, Yuan Feng (2021). Measuring the constrained reachability in quantum Markov chains. Acta Informatica.

引用 DOI URL

X. Fu, Jintao Yu, Xing Su, Hanru Jiang, Hua Wu, Fucheng Cheng, Xi Deng, Jinrong Zhang, Lei Jin, Yihang Yang, Le Xu, Chunchao Hu, Anqi Huang, Guangyao Huang, Xiaogang Qiang, Mingtang Deng, Ping Xu, Weixia Xu, Wanwei Liu, Yu Zhang, Yuxin Deng, Junjie Wu, Yuan Feng (2021). Quingo: A Programming Framework for Heterogeneous Quantum-Classical Computing with NISQ Features. ACM Transactions on Quantum Computing.

引用 DOI URL

Wen-Jun Shi, Qin-Xiang Cao, Yu-Xin Deng, Han-Ru Jiang, Yuan Feng (2021). Symbolic Reasoning About Quantum Circuits in Coq. Journal of Computer Science and Technology.

引用 DOI URL

Sanjiang Li, Xiangzhen Zhou, Yuan Feng (2021). Qubit Mapping Based on Subgraph Isomorphism and Filtered Depth-Limited Search. IEEE Transactions on Computers.

引用 DOI

Xiangzhen Zhou, Yuan Feng, Sanjiang Li (2020). A monte carlo tree search framework for quantum circuit transformation. Proceedings of the 39th International Conference on Computer-Aided Design.

引用 DOI URL

Xiangzhen Zhou, Sanjiang Li, Yuan Feng (2020). Quantum Circuit Transformation Based on Simulated Annealing and Heuristic Search. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems.

引用 DOI

Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying (2019). Model Checking Applied to Quantum Physics.

引用 arXiv URL

Mingsheng Ying, Yuan Feng (2018). Model-checking quantum systems. National Science Review.

引用 DOI URL

Chen Fu, Andrea Turrini, Xiaowei Huang, Lei Song, Yuan Feng, Lijun Zhang (2018). Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18.

引用 DOI URL

Ji Guan, Yuan Feng, Mingsheng Ying (2018). Decomposition of quantum Markov chains and its applications. Journal of Computer and System Sciences.

引用 DOI URL

Mingsheng Ying, Yuan Feng (2018). Model Checking Quantum Systems --- A Survey.

引用 arXiv URL

Ji Guan, Yuan Feng, Mingsheng Ying (2018). Super-activating Quantum Memory with Entanglement.

引用 arXiv URL

Ji Guan, Yuan Feng, Mingsheng Ying (2018). The Structure of Decoherence-free Subsystems.

引用 arXiv URL

Yuan Feng, \Ernst Moritz\ Hahn, Andrea Turrini, Shenggang Ying (2017). Model Checking Omega-regular Properties for Quantum Markov Chains. 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany.

引用 DOI

Yuxin Deng, Yuan Feng (2017). Bisimulations for probabilistic linear lambda calculi. 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE).

引用 DOI

Yuan Feng, Lijun Zhang (2017). Precisely deciding CSL formulas through approximate model checking for CTMCs. Journal of Computer and System Sciences.

引用 DOI URL

Yuxin Deng, Yuan Feng (2017). Probabilistic bisimilarity as testing equivalence. Information and Computation.

引用 DOI URL

Guoxin Su, Taolue Chen, Yuan Feng, David S. Rosenblum (2017). ProEva: Runtime Proactive Performance Evaluation Based on Continuous-Time Markov Chains. 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE).

引用 DOI

Shenggang Ying, Mingsheng Ying, Yuan Feng (2017). Quantum Privacy-Preserving Data Analytics.

引用 arXiv URL

Shenggang Ying, Mingsheng Ying, Yuan Feng (2017). Quantum Privacy-Preserving Perceptron.

引用 arXiv URL

Guoxin Su, Taolue Chen, Yuan Feng, David S. Rosenblum, P. S. Thiagarajan (2016). An Iterative Decision-Making Scheme for Markov Decision Processes and Its Application to Self-adaptive Systems. Fundamental Approaches to Software Engineering.

引用

Guoxin Su, Yuan Feng, Taolue Chen, David S. Rosenblum (2016). Asymptotic Perturbation Bounds for Probabilistic Model Checking with Empirically Determined Probability Parameters. IEEE Transactions on Software Engineering.

引用 DOI

Shenggang Ying, Mingsheng Ying, Yuan Feng (2016). Quantum Privacy-Preserving Data Mining.

引用 arXiv URL

Yong Li, Lei Song, Yuan Feng, Lijun Zhang (2016). Verify LTL with Fairness Assumptions Efficiently. 2016 23rd International Symposium on Temporal Representation and Reasoning (TIME).

引用 DOI

Yuan Feng, Lijun Zhang (2015). A nearly optimal upper bound for the self-stabilization time in Herman's algorithm. Distributed Computing.

引用 DOI URL

Yuan Feng, Lei Song, Lijun Zhang (2015). Distribution-based Bisimulation and Bisimulation Metric in Probabilistic Automata.

引用 arXiv URL

Lvzhou Li, Yuan Feng (2015). On hybrid models of quantum finite automata. Journal of Computer and System Sciences.

引用 DOI URL

Yuan Feng, Ernst Moritz Hahn, Andrea Turrini, Lijun Zhang (2015). QPMC: A Model Checker for Quantum Programs and Protocols. FM 2015: Formal Methods.

引用

Lvzhou Li, Yuan Feng (2015). Quantum Markov chains: Description of hybrid systems, decidability of equivalence, and model checking linear-time properties. Information and Computation.

引用 DOI URL

Yuan Feng, Mingsheng Ying (2015). Toward automatic verification of quantum cryptographic protocols.

引用 arXiv URL

Mingsheng Ying, Yangjia Li, Nengkun Yu, Yuan Feng (2014). Model-Checking Linear-Time Properties of Quantum Systems. ACM Trans. Comput. Logic.

引用 DOI URL

Yuan Feng, Yuxin Deng, Mingsheng Ying (2014). Symbolic Bisimulation for Quantum Processes. ACM Trans. Comput. Logic.

引用 DOI URL

Mingsheng Ying, Nengkun Yu, Yuan Feng (2014). Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs.

引用 arXiv URL

Taolue Chen, Yuan Feng, David S. Rosenblum, Guoxin Su (2014). Perturbation Analysis in Verification of Discrete-Time Markov Chains. CONCUR 2014 – Concurrency Theory.

引用

Yuan Feng, Lijun Zhang (2014). When Equivalence and Bisimulation Join Forces in Probabilistic Automata. FM 2014: Formal Methods.

引用

Yuan Feng, Lijun Zhang (2013). A tighter bound for the self-stabilization time in Hermanʼs algorithm. Information Processing Letters.

引用 DOI URL

Yuan Feng, Nengkun Yu, Mingsheng Ying (2013). Model checking quantum Markov chains. Journal of Computer and System Sciences.

引用 DOI URL

Mingsheng Ying, Yuan Feng, Nengkun Yu (2013). Quantum Information-Flow Security: Noninterference and Access Control. 2013 IEEE 26th Computer Security Foundations Symposium.

引用 DOI

Yuan Feng, Nengkun Yu, Mingsheng Ying (2013). Reachability Analysis of Recursive Quantum Markov Chains. Mathematical Foundations of Computer Science 2013.

引用

Shenggang Ying, Yuan Feng, Nengkun Yu, Mingsheng Ying (2013). Reachability Probabilities of Quantum Markov Chains. CONCUR 2013 – Concurrency Theory.

引用

Mingsheng Ying, Nengkun Yu, Yuan Feng, Runyao Duan (2013). Verification of quantum programs. Science of Computer Programming.

引用 DOI URL

Mingsheng Ying, Yuan Feng, RunYao Duan, YangJia Li, NengKun Yu (2012). Quantum programming: From theories to implementations. Chinese Science Bulletin.

引用 DOI URL

Mingsheng Ying, Nengkun Yu, Yuan Feng (2012). Defining Quantum Control Flow.

引用 arXiv URL

Yuxin Deng, Yuan Feng (2012). Open Bisimulation for Quantum Processes. Theoretical Computer Science.

引用

Mingsheng Ying, Yuan Feng (2011). A Flowchart Language for Quantum Programming. IEEE Transactions on Software Engineering.

引用 DOI

Yuan Feng, Runyao Duan, Mingsheng Ying (2011). Bisimulation for quantum processes. Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

引用 DOI URL

Mingsheng Ying, Yuan Feng (2010). Quantum loop programs. Acta Informatica.

引用 DOI URL

Runyao Duan, Yuan Feng, Mingsheng Ying (2009). Perfect Distinguishability of Quantum Operations. Phys. Rev. Lett..

引用 DOI URL

Mingsheng Ying, Yuan Feng, Runyao Duan, Zhengfeng Ji (2009). An algebra of quantum processes. ACM Trans. Comput. Logic.

引用 DOI URL

Mingsheng Ying, Yuan Feng (2009). An Algebraic Language for Distributed Quantum Computing. IEEE Transactions on Computers.

引用 DOI

Yuan Feng, Yaoyun Shi (2009). Characterizing Locally Indistinguishable Orthogonal Product States. IEEE Transactions on Information Theory.

引用 DOI

Runyao Duan, Yuan Feng, Yu Xin, Mingsheng Ying (2009). Distinguishability of Quantum States by Separable Operations. IEEE Transactions on Information Theory.

引用 DOI

Runyao Duan, Yuan Feng, Mingsheng Ying (2008). Local Distinguishability of Multipartite Unitary Operations. Phys. Rev. Lett..

引用 DOI URL

Yuan Feng, Runyao Duan, Mingsheng Ying (2008). Locally undetermined states, generalized Schmidt decomposition, and an application in distributed computing.

引用 arXiv URL

Zhengfeng Ji, Guoming Wang, Runyao Duan, Yuan Feng, Mingsheng Ying (2008). Parameter Estimation of Quantum Channels. IEEE Transactions on Information Theory.

引用 DOI

Runyao Duan, Yuan Feng, Zhengfeng Ji, Mingsheng Ying (2007). Distinguishing Arbitrary Multipartite Basis Unambiguously Using Local Operations and Classical Communication. Phys. Rev. Lett..

引用 DOI URL

Runyao Duan, Yuan Feng, Mingsheng Ying (2007). Entanglement is Not Necessary for Perfect Discrimination between Unitary Operations. Phys. Rev. Lett..

引用 DOI URL

Mingsheng Ying, Jianxin Chen, Yuan Feng, Runyao Duan (2007). Commutativity of quantum weakest preconditions. Information Processing Letters.

引用 DOI URL

Yuan Feng, Runyao Duan, Zhengfeng Ji, Mingsheng Ying (2007). Probabilistic bisimulations for quantum processes. Information and Computation.

引用 DOI URL

Yuan Feng, Runyao Duan, Zhengfeng Ji, Mingsheng Ying (2007). Proof rules for the correctness of quantum programs. Theoretical Computer Science.

引用 DOI URL

Yuan Feng, Runyao Duan, Mingsheng Ying (2006). Relation between catalyst-assisted transformation and multiple-copy transformation for bipartite pure states. Phys. Rev. A.

引用 DOI URL

Run-Yao Duan, Zhengfeng Ji, Yuan Feng, Mingsheng Ying (2006). Some Issues in Quantum Information Theory. Journal of Computer Science and Technology.

引用 DOI URL

Yuan Feng, Runyao Duan, Zhengfeng Ji (2006). Optimal dense coding with arbitrary pure entangled states. Phys. Rev. A.

引用 DOI URL

Zhengfeng Ji, Yuan Feng, Runyao Duan, Mingsheng Ying (2006). Identification and Distance Measures of Measurement Apparatus. Phys. Rev. Lett..

引用 DOI URL

Zhengfeng Ji, Yuan Feng, Runyao Duan, Mingsheng Ying (2006). Boundary effect of deterministic dense coding. Phys. Rev. A.

引用 DOI URL

Runyao Duan, Yuan Feng, Mingsheng Ying (2006). Partial recovery of quantum entanglement. IEEE Transactions on Information Theory.

引用 DOI

Chi Zhang, Yuan Feng, Mingsheng Ying (2006). Unambiguous discrimination of mixed quantum states. Physics Letters A.

引用 DOI URL

Zhengfeng Ji, Yuan Feng, Mingsheng Ying (2005). Local cloning of two product states. Phys. Rev. A.

引用 DOI URL

Runyao Duan, Yuan Feng, Mingsheng Ying (2005). Entanglement-assisted transformation is asymptotically equivalent to multiple-copy transformation. Phys. Rev. A.

引用 DOI URL

Yuan Feng, Runyao Duan, Zhengfeng Ji (2005). Condition and capability of quantum state separation. Phys. Rev. A.

引用 DOI URL

Runyao Duan, Yuan Feng, Xin Li, Mingsheng Ying (2005). Trade-off between multiple-copy transformation and entanglement catalysis. Phys. Rev. A.

引用 DOI URL

Runyao Duan, Yuan Feng, Xin Li, Mingsheng Ying (2005). Multiple-copy entanglement transformation and entanglement catalysis. Phys. Rev. A.

引用 DOI URL

Runyao Duan, Yuan Feng, Zhengfeng Ji, Mingsheng Ying (2005). Efficiency of deterministic entanglement transformation. Phys. Rev. A.

引用 DOI URL

Runyao Duan, Yuan Feng, Mingsheng Ying (2005). An Equivalence of Entanglement-Assisted Transformation and Multiple-Copy Entanglement Transformation.

引用 arXiv URL

Yuan Feng, Runyao Duan, Mingsheng Ying (2005). Catalyst-assisted probabilistic entanglement transformation. IEEE Transactions on Information Theory.

引用 DOI

Yuan Feng, Runyao Duan, Mingsheng Ying (2004). Unambiguous discrimination between mixed quantum states. Phys. Rev. A.

引用 DOI URL

Yuan Feng, Runyao Duan, Mingsheng Ying (2004). When catalysis is useful for probabilistic entanglement transformation. Phys. Rev. A.

引用 DOI URL

Yuan Feng, Mingsheng Ying (2004). Process algebra approach to reasoning about concurrent actions. Journal of Computer Science and Technology.

引用 DOI URL

Runyao Duan, Zhengfeng Ji, Yuan Feng, Mingsheng Ying (2004). Quantum operation, quantum Fourier transform and semi-definite programming. Physics Letters A.

引用 DOI URL

Yuan Feng, Shengyu Zhang, Runyao Duan, Mingsheng Ying (2002). Lower bound on inconclusive probability of unambiguous discrimination. Phys. Rev. A.

引用 DOI URL

Xiaoming Sun, Shengyu Zhang, Yuan Feng, Mingsheng Ying (2002). Mathematical nature of and a family of lower bounds for the success probability of unambiguous discrimination. Phys. Rev. A.

引用 DOI URL

Yuan Feng, Shengyu Zhang, Mingsheng Ying (2002). Probabilistic cloning and deleting of quantum states. Phys. Rev. A.

引用 DOI URL

Yuan Feng, Shengyu Zhang, Xiaoming Sun, Mingsheng Ying (2002). Universal and original-preserving quantum copying is impossible. Physics Letters A.

引用 DOI URL

Shengyu Zhang, Yuan Feng, Xiaoming Sun, Mingsheng Ying (2001). Upper bound for the success probability of unambiguous discrimination among quantum states. Phys. Rev. A.

引用 DOI URL