中法联合项目JRP:量化系统的形式化验证 (2019 – 2021)

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

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

项目重要进展

理论研究

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

工具研发

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

国际交流

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

项目成果

学术论文

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

发明专利

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

软件著作权

  • 量子模型检验软件(登记号2020SR0127396)

人才培养

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