开云·kaiyun(中国)官方网站

       简介：本中心瞄准自动推理和可信计算的发展前沿，密切结合国家重大战略需求和重庆本地的经济发展，立足零误差计算的基础研究，并以其为工具积极开展在信息安全、量子信息和计算、生物数学、程序自动生成、优化和验证等领域的交叉创新性应用基础研究。

       研究团队包括中国科学院|开云·kaiyun院士在内的研究员3名，副研究员2名，助理研究员2名以及多名研究生。核心科研骨干都具有海外学习工作经历，承担过多项科研项目研发, 在学术方面具有一定的国际影响力。近5年获得科研经费1040万元，包括国家级项目8项, 中科院项目7项；发表SCI/EI文章70篇，获得专利授权4项，软件著作权2项。

研究方向

零误差计算

       数值计算方法不可避免地给计算结果带来多种误差，在航天航空、生物医疗等领域，计算误差可能会带来严重后果。符号计算可以得到问题精确地完备解，但是计算量大且表达式庞大，导致计算效率较低，或者受到计算机内存大小的限制而无法得到结果，往往不能满足实际问题求解的需要。据此，我们提出“零误差计算“的构想，即采用近似计算获得准确结果，并研究兼具数值计算高效性和符号计算准确性的零误差数值计算高效算法.

成果：

       1.将有理数域上的零误差计算理论推广到了代数数域，并从理论上给出了计算过程误差控制范围，可以充分保证代数数计算结果的无误差；

       2.给出了PSLQ 的扰动分析，据此有望设计首个数值的PSLQ算法，成为零误差计算理论走向实际应用的桥梁；

       3.给出了稀疏多项式因式分解快速算法以及数值多变元因式分解的几何含义和数值稳定性定理；

       4.提出了利用数值代数几何给出参数半代数系统解的完整刻画的理论。

全同态密码及其应用

       全同态加密是后量子时代信息安全研究的前沿，它可保证对密文进行直接运算解密的结果与对明文进行等价运算所得到的结果相同。所以它可以从根本上解决将计算委托给第三方时的保密问题，可满足传统加密方案所保障的通信安全和存储安全外的云端的运算安全。此外,它有望抵御量子攻击。

       成果：基于IBM公司的HeLib开发了同态整数运算库，实现了在计算机上使用密文来进行不同进制下的加减乘除等算术运算的功能； 优化了基于RLWE问题的加密方案，用c++开发了低膨胀率、高效的抗量子加密算法，可满足安全数据通信及云端服务。

程序正确性验证

       随着计算机和互联网的迅猛发展，以通信、存储和计算为核心的信息基础设施已经渗透到政治、经济、军事、文化以及社会的各个层面。软件是信息基础设施的灵魂，但它并不总是让人信任，从而产生“软件可信性”问题。面向应用的程序正确性验证是可信软件基础研究的重要课题之一。其主要研究包括如何使用数学方法去证明给定程序是否符合预先设定的目标, 程序停机问题证明与不变式构造。

       成果：建立了基于不动点理论的多项式循环程序终止性判定理论； 提出了基于三角分解的实闭域一阶理论的量词消去算法并应用于含参程序的自动并行化。