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

量子计算是具有颠覆性的新一代计算技术。作为大规模部署量子计算的关键，量子程序与软件同样得到越来越多的关注。不幸的是，量子力学诸多反直觉特性为量子程序开发带来困难，从语言设计、特性分析，到程序测试调试，都成为错误的可能来源。因此，引入形式化方法——利用数学分析技术证明特性、利用证明助手开发高可靠的验证工具，成为很有吸引力的交叉方向。特别是形式化方法与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, 博士后