Name: Yuan Feng

Title: Professor

Email: yuan_feng@tsinghua.edu.cn

Education Background

B.Sc.: Department of Applied Mathematics, Tsinghua University, 1999

Ph.D.: Department of Computer Science and Technology, Tsinghua University, 2004

Professional Positions

ACM Transactions on Software Engineering and Methodology: Associate Editor.

Research Areas

Model checking quantum systems, quantum program verification, quantum communicating systems

Research Overview

Model checking quantum systems: Model checking is an important technique for formal verification of sequential programs, concurrent protocols, and hardware systems. Due to its mechanizability and ability to provide diagnostic information, it has been widely used in industry. We proposed two different quantum Markov chain models and systematically developed model checking methods for linear and branching quantum temporal logic formulas. In 2021, we published "Model Checking Quantum Systems: Principles and Algorithms" (Cambridge University Press), which systematically reviews this emerging research direction of quantum model checking, especially the work of our research group. This is the first academic monograph in the field of quantum model checking.

Quantum Program Verification: Hoare logic is the logical foundation of program verification and occupies a central position in program design methodology. Hoare logic defines appropriate axioms and inference rules for all program constructs of an imperative programming language, enabling (partial) automated proofs of program correctness. We established Hoare logic for quantum programs with classical variables, proving its soundness and relative completeness. This logic has been used to verify the complete Shor algorithm for the first time (ACM TQC 2021). Recently, we further employed this technique to design Hoare logic systems for quantum parallel programs without shared variables (TCS 2022), distributed quantum programs with classical communication (ACM TOCL 2022), and nondeterministic quantum programs(ASPLOS’23).

Quantum Communicating Systems: Quantum communication and cryptography are currently the most mature technologies in the field of quantum information. In order to formally describe quantum communication networks and lay a theoretical foundation for formal verification of quantum network software and communication protocols, we proposed the quantum process algebra qCCS (Information and Computation 2007). More importantly, we have successfully established a notion of bisimulation for quantum processes and proved its congruence for various process constructs (POPL’11, ACM TOPLAS 2012). Our subsequent works, including symbolic bisimulation (ACM TOCL 2014), open bisimulation (TCS 2012), and distribution-based bisimulation (CONCUR 2015), have greatly enriched the theoretical foundation of qCCS and enhanced its ability to describe and verify practical quantum communicating systems.

Academic Achievements

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).