支持单位: 中国科学院国际合作局

本项目由中国科学院软件研究所承担，与法国法国国家信息与自动化研究所合作，围绕 “量化系统的形式化验证”这一课题，共同开展前沿科学与技术研究。在本项目的支持下，中法双方有效开展交流合作，在项目实施期间顺利完成研究计划，达成既定目标，有力推动学术前沿，在论文发表、人才培养、国际合作交流等多个方面取得成果。

项目重要进展

理论研究

项目组拓宽了概率和量子系统形式验证的边界，特别是基于定理证明系统对概率系统的并发进行了形式化，并提出了关于量子模型的符号化推理方法，突破了现有的研究瓶颈。

工具研发

项目组设计了一个在经典计算机上模拟量子计算的工具——Qsimulation，其中实现的矩阵矢量乘法的加速算法使得其模拟运算效率远高于Qiskit、ProjectQ等国外的量子计算模拟器，达到国际前沿水平。

国际交流

项目组举办了计算机科学逻辑国际会议 (LICS 2020)，并同期联合举办了自动化、语言和程序设计国际会议 (ICALP 2020)，这两个会议是程序语言与计算机理论领域的顶级国际学术会议，会议的举办展示了项目组优秀的国际学术声誉与地位。

项目成果

学术论文

在I&C、TCS、TACAS、QIP等形式化方法、理论计算机、量子计算相关研究领域国际权威期刊或会议上发表高水平学术论文12篇。

发明专利

1. 一种基于禁忌搜索的量子电路映射方法（公开号 CN113962172A）
2. 一种针对安卓应用程序性质的检测方法及装置（公开号 CN114637664A）
3. 一种中文安卓应用程序的恶意行为静态检测方法及装置（公开号 CN202111171237）

软件著作权

• 量子模型检验软件（登记号2020SR0127396）

人才培养

• 合作培养研究生5名（其中博士3名、硕士2名）