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

量子计算是具有颠覆性的新一代计算技术。作为大规模部署量子计算的关键，量子程序与软件同样得到越来越多的关注。不幸的是，量子力学诸多反直觉特性为量子程序开发带来困难，从语言设计、特性分析，到程序测试调试，都成为错误的可能来源。因此，引入形式化方法——利用数学分析技术证明特性、利用证明助手开发高可靠的验证工具，成为很有吸引力的交叉方向。特别是形式化方法与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） Automating Equational Proofs in Dirac Notation, Proceedings of the ACM on Programming Languages (POPL 2025), 2025, 第 3 作者  通讯作者
（2） CoqQ: Foundational Verification of Quantum Programs, Proceedings of the ACM on Programming Languages (POPL 2023), 2023, 第 1 作者  通讯作者
（3） A proof system for disjoint parallel quantum programs, THEORETICAL COMPUTER SCIENCE, 2022, 第 2 作者
（4） 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), 2022, 第 2 作者
（5） When is the Chernoff Exponent for Quantum Operations Finite?, IEEE TRANSACTIONS ON INFORMATION THEORY, 2021, 第 2 作者
（6） Protocols for Packet Quantum Network Intercommunication, IEEE TRANSACTIONS ON QUANTUM ENGINEERING, 2021, 第 3 作者
（7） EasyPQC: Verifying Post-Quantum Cryptography, Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS '21), 2021, 第 9 作者
（8） A Quantum Interpretation of Bunched Logic for Quantum Separation Logic, 2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS 2021, 2021, 第 1 作者  通讯作者
（9） Entirety of Quantum Uncertainty and Its Experimental Verification, Entirety of Quantum Uncertainty and Its Experimental Verification, CHINESE PHYSICS LETTERS, 2021, 第 2 作者
（10） Strassen's theorem for quantum couplings, THEORETICAL COMPUTER SCIENCE, 2020, 第 1 作者  通讯作者
（11） Relational Proofs for Quantum Programs, Proceedings of the ACM on Programming Languages (POPL 2020), 2020, 第 5 作者  通讯作者
（12） Projection-based runtime assertions for testing and debugging Quantum programs, Proceedings of the ACM on Programming Languages (OOPSLA 2020), 2020, 第 2 作者
（13） An Applied Quantum Hoare Logic, PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, 第 1 作者  通讯作者
（14） Differential Privacy in Quantum Computation, 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 2017, 第 1 作者  通讯作者

   

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