基本信息

周立  男  博导  中国科学院软件研究所
电子邮件: zhouli@ios.ac.cn
通信地址: 中科院软件所5号楼306
邮政编码:

研究领域

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

量子计算是具有颠覆性的新一代计算技术。作为大规模部署量子计算的关键,量子程序与软件同样得到越来越多的关注。不幸的是,量子力学诸多反直觉特性为量子程序开发带来困难,从语言设计、特性分析,到程序测试调试,都成为错误的可能来源。因此,引入形式化方法——利用数学分析技术证明特性、利用证明助手开发高可靠的验证工具,成为很有吸引力的交叉方向。特别是形式化方法与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, 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, 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, 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, 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, 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, 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, https://doi.org/10.1109/LICS52264.2021.9470673.
[8] 谢杰, 周立, 张傲男, 徐慧超, 翁文康, 徐平, 俞能昆, 张利剑. Entirety of Quantum Uncertainty and Its Experimental Verification. CHINESE PHYSICS LETTERS[J]. 2021, 38(7): 11-16, [9] Zhou, Li, Ying, Shenggang, Yu, Nengkun, Ying, Mingsheng. Strassen's theorem for quantum couplings. THEORETICAL COMPUTER SCIENCE[J]. 2020, 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, 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, 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, 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, 249-262, https://doi.org/10.1109/CSF.2017.23.

科研活动

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