形式化方法；量子程序理论；量子密码学

量子计算是具有颠覆性的新一代计算技术。作为大规模部署量子计算的关键，量子程序与软件同样得到越来越多的关注。不幸的是，量子力学诸多反直觉特性为量子程序开发带来困难，从语言设计、特性分析，到程序测试调试，都成为错误的可能来源。因此，引入形式化方法——利用数学分析技术证明特性、利用证明助手开发高可靠的验证工具，成为很有吸引力的交叉方向。特别是形式化方法与AI的结合，为构建系统性的量子理论、大规模算法库提供了技术支持。

研究方向关注量子程序理论与形式化方法的交叉融合，包括数学与量子理论形式化（参考Lean对大量数学的形式化工作）、量子程序与软件理论、量子与抗量子密码协议证明等。

课题组招收有志于从事科研事业的硕士和博士生、本科阶段的实习生。

如果你是大二/大三的本科生，并且对研究方向感兴趣并具备优秀的学业成绩与综合能力，可以提前与我联系，合适的情况下课题组会进行（长期）1对1的科研指导，并尽早确定组内保研指标。由于研究方向非常前沿，希望你拥有科研热情，享受探索新领域的过程，学术工作将是你后续研究生阶段的唯一主题。我会全程亲自培养学生，保持每周1-2次固定时间学术讨论，不会在研究成果上push，但需要你认真持续和投入地进行科研工作。

其他要求：

保研/报考学生满足中国科学院大学和中国科学院软件研究所的基本要求。

明确保研指标后不会在最后阶段放弃。如果双方明确保研与招生意向，课题组会保证你的保研指标，也希望你能信守承诺，最后阶段放弃指标会对我们招生带来很大影响。

联系方式：发送简历至 zhouli@ios.ac.cn

081202-计算机软件与理论

形式化方法
量子程序设计
量子密码学

2014-09--2019-07   清华大学   博士
2010-08--2014-07   清华大学   本科

   

2022-09~现在, 中国科学院软件研究所, 副研究员
2019-09~2022-08,Max Planck Institute for Security and Privacy, 博士后

   

[1] Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying. CoqQ: Foundational Verification of Quantum Programs. Proceedings of the ACM on Programming Languages[J]. 2023, 第 1 作者  通讯作者  7(POPL): 29:1-33, https://doi.org/10.1145/3571222.
[2] Ying, Mingsheng, Zhou, Li, Li, Yangjia, Feng, Yuan. A proof system for disjoint parallel quantum programs. THEORETICAL COMPUTER SCIENCE[J]. 2022, 第 2 作者897: 164-184, http://dx.doi.org/10.1016/j.tcs.2021.10.025.
[3] Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. PROCEEDINGS OF THE 37TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS)[J]. 2022, 第 2 作者4:1-13, https://doi.org/10.1145/3531130.3533327.
[4] Yu, Nengkun, Zhou, Li. When is the Chernoff Exponent for Quantum Operations Finite?. IEEE TRANSACTIONS ON INFORMATION THEORY[J]. 2021, 第 2 作者67(7): 4517-4523, http://dx.doi.org/10.1109/TIT.2021.3067924.
[5] Nengkun Yu, ChingYi Lai, Li Zhou. Protocols for Packet Quantum Network Intercommunication. IEEE TRANSACTIONS ON QUANTUM ENGINEERING[J]. 2021, 第 3 作者2: 1-9, https://doi.org/10.1109/TQE.2021.3112594.
[6] Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou. EasyPQC: Verifying Post-Quantum Cryptography. Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS '21)[J]. 2021, 第 9 作者2564-2586, https://doi.org/10.1145/3460120.3484567.
[7] Li Zhou, Gilles Barthe, Justin Hsu, Ying Mingsheng, Nengkun Yu. A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. 2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS 2021[J]. 2021, 第 1 作者  通讯作者  https://doi.org/10.1109/LICS52264.2021.9470673.
[8] JieXie, LiZhou, AonanZhang, HuichaoXu, ManHongYung, PingXu, NengkunYu, LijianZhang. Entirety of Quantum Uncertainty and Its Experimental Verification. Chinese Physics Letters[J]. 2021, 第 2 作者38(7): 70303-16, https://cpl.iphy.ac.cn/10.1088/0256-307X/38/7/070303.
[9] Zhou, Li, Ying, Shenggang, Yu, Nengkun, Ying, Mingsheng. Strassen's theorem for quantum couplings. THEORETICAL COMPUTER SCIENCE[J]. 2020, 第 1 作者  通讯作者  802: 67-76, http://dx.doi.org/10.1016/j.tcs.2619.08.026.
[10] Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou. Relational Proofs for Quantum Programs. Proceedings of the ACM on Programming Languages[J]. 2020, 第 5 作者  通讯作者  4(POPL): 21:1-29, https://doi.org/10.1145/3371089.
[11] Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, Yuan Xie. Projection-based runtime assertions for testing and debugging Quantum programs. Proceedings of the ACM on Programming Languages[J]. 2020, 第 2 作者4(OOPSLA): 150:1-29, https://doi.org/10.1145/3428218.
[12] Zhou, Li, Yu, Nengkun, Ying, Mingsheng. An Applied Quantum Hoare Logic. PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19)[J]. 2019, 第 1 作者  通讯作者  1149-1162, http://dx.doi.org/10.1145/3314221.3314584.
[13] Li Zhou, Mingsheng Ying. Differential Privacy in Quantum Computation. 2017 IEEE 30th Computer Security Foundations Symposium (CSF)[J]. 2017, 第 1 作者  通讯作者  249-262, https://doi.org/10.1109/CSF.2017.23.

   

（ 1 ） 量子程序与(后)量子密码协议的形式验证, 负责人, 国家任务, 2023-12--2026-12
（ 2 ） 量子计算的数学理论、算法和软件工具, 负责人, 国家任务, 2023-12--2028-11