多项式循环程序的终止性研究及其应用

结题报告
项目介绍
AI项目解读

基本信息

  • 批准号：
    61572024
  • 项目类别：
    面上项目
  • 资助金额：
    48.0万
  • 负责人：
    李轶
  • 依托单位：
    中国科学院重庆绿色智能技术研究院
  • 学科分类：
    F0214.新型计算及其应用基础
  • 结题年份：
    2019
  • 批准年份：
    2015
  • 项目状态：
    已结题
  • 起止时间：
    2016-01-01 至2019-12-31

项目摘要

Analysis and verification of correctness of application-oriented software is of great significance. Termination analysis guarantees the complete correctness of software. For polynomial loop programs, this project will focus on the termination problem of the type of programs. By using symbolic-numeric computation tools, we will explore various verification techniques based on analysis of fixed points, invariant polytopes and Ranking functions. We will further study that the correlation between fix points and termination problems, and correlation between fix points and Ranking functions. Different from the existing methods of termination verification and analysis, the technique based on fixed points enables us not only to explore more loop programs whose termination can be proven to be decidable, but also to find Ranking functions over the integers. This work will make up for the deficiency of current termination analysis of polynomial programs. Moreover, this work is also very promising to be applied to verify and analyze the termination problems arising in embedded systems.
面向应用的软件正确性分析与验证具有十分重要的意义。终止性分析是保障程序完全正确性的必要基础。嵌入式软件中的循环程序往往具有多项式结构。因此，本课题针对多项式循环程序的非线性性、动力行为的不确定性等特点，围绕多项式循环程序的终止性验证这一大难题，采用符号数值混合计算理论及工具，深入探索基于不动点技术、 多面体不变集分析以及秩函数计算的终止性验证理论和算法。其中，着重研究不动点理论与终止性问题的内在联系以及与秩函数之间的深刻关系。不同于现有终止性验证方法，我们提出的基于不动点分析的验证技术不仅能在终止性这一不可判定问题中探测到更多的终止性可判定子类，而且能将秩函数合成问题从实域上拓展到整数环上，为终止性问题的研究提供了新的研究手段和方法，丰富了终止性验证的基础理论。这项研究将弥补目前在非线性多项式循环程序终止性验证方面研究的不足。同时，研究结果有望广泛应用于嵌入式软件的终止性分析与验证中。

结项摘要

本项目运用计算机代数的理论和工具，围绕程序终止性这一问题，从可判定性，秩函数构造与计算等方面，对多项式循环程序的终止性问题进行了研究。对线性循环程序，我们首次证明了这类循环不可终止的充分必要条件是循环条件形成的区域中存在多面体吸引集，并给出了该吸引集的代数刻画。与传统方法不同，新的方法并不依赖Jordan标准型的计算，从而避免了Jordan标准型的浮点计算所造成的判定误差。该成果发表在国际期刊Theoretical Computer Science. 非线性循环程序由于更为复杂的动力行为，使得当前从可判定角度对其研究的结果甚少。基于函数不动点理论，我们建立了适定条件，使得在该条件下，可将这类循环程序的终止性问题等价地归结为不动点的判定，为非线性循环程序的终止性研究提供了新的研究手段和方法。相关成果发表在ICTAC 2016，SETTA 2017，软件学报等会议期刊上。秩函数（Ranking Functions）法仍是当前终止性研究的主流方法。从几何角度，我们对线性秩函数的构造做了深入分析，建立了线性程序不存在线性秩函数的witness points的代数刻画。不同于现有方法，我们的方法揭示了线性秩函数与状态点集间的内在关联。该成果发表在国际期刊STTT上。但程序的秩函数未必是线性的。针对非线性多项式型秩函数的计算问题，我们提出两种途径来解决它。一是利用Polya定理，将多项式秩函数计算问题归结为线性约束求解问题，从而便于利用线性规划算法进行求解。实验表明该方法效率上优于传统的量词消去方法。二是我们证明了秩函数计算问题等价于在两个点集间超平面的计算问题，继而利用机器学习算法探寻候选秩函数，并借助符号计算工具对其予以精确验证。上述系列成果已发表在软件学报，ICFEM 2019，STTT上。此外，我们提出了L-eventual 秩函数及局部秩函数的概念。实验表明，对于部分没有传统秩函数的程序，我们发现它们的确具有L-eventual秩函数或局部秩函数。相关成果已发表在TASE 2016，ESTC 2018上。本项目中，基于不动点分析的工作丰富了当前终止性研究的基础理论，为我们今后在终止性方面的研究提供了可持续的科研思路。

项目成果

期刊论文数量（12）
专著数量（0）
科研奖励数量（0）
会议论文数量（10）
专利数量（1）
Parameterized inequalities about a point in the plane of a triangle
关于三角形平面上的点的参数化不等式
  • DOI：
    10.7153/jmi-2018-12-72
  • 发表时间：
    2018
  • 期刊：
    journal of mathematical inequalities
  • 影响因子：
    --
  • 作者：
    黄方剑;李轶
  • 通讯作者：
    李轶
基于Dixon结式和逐次差分代换的多项式秩函数探测方法
  • DOI：
    --
  • 发表时间：
    2019
  • 期刊：
    计算机应用
  • 影响因子：
    --
  • 作者：
    袁月;李轶
  • 通讯作者：
    李轶
Ranking Function Detection via SVM: A More General Method
通过 SVM 进行排序函数检测：一种更通用的方法
  • DOI：
    10.1109/access.2018.2890692
  • 发表时间：
    2019
  • 期刊：
    IEEE Access
  • 影响因子：
    3.9
  • 作者：
    袁月;李轶
  • 通讯作者：
    李轶
计算最终线性秩函数的新方法
  • DOI：
    10.1016/j.stemcr.2022.09.007
  • 发表时间：
    2017
  • 期刊：
    计算机科学
  • 影响因子：
    --
  • 作者：
    朱广;李轶;吴文渊
  • 通讯作者：
    吴文渊
基于svm的多项式循环程序秩函数生成
  • DOI：
    --
  • 发表时间：
    2019
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    李轶;蔡天训;樊建峰;吴文渊;冯勇
  • 通讯作者：
    冯勇

数据更新时间：{{ journalArticles.updateTime }}

{{ item.title }}
{{ item.translation_title }}
  • DOI：
    {{ item.doi || "--"}}
  • 发表时间：
    {{ item.publish_year || "--" }}
  • 期刊：
    {{ item.journal_name }}
  • 影响因子：
    {{ item.factor || "--"}}
  • 作者：
    {{ item.authors }}
  • 通讯作者：
    {{ item.author }}

数据更新时间：{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ monograph.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者：
    {{ item.authors }}

数据更新时间：{{ patent.updateTime }}

其他文献

Effect of Granular Activated Carbon on the Enhancement of Cometabolic Biodegradation of Phenol and 4-Chlorophenol
颗粒活性炭对苯酚和4-氯苯酚共代谢生物降解的促进作用
  • DOI：
    10.1016/s0926-3373(99)00068-5
  • 发表时间：
    2010
  • 期刊：
    Applied Catalysis B-environmental
  • 影响因子：
    22.1
  • 作者：
    李轶;饶婷;刘志刚
  • 通讯作者：
    刘志刚
电形成法制备脂质体
  • DOI：
    --
  • 发表时间：
    2011
  • 期刊：
    Progress in Chemistry
  • 影响因子：
    1.3
  • 作者：
    景婧;李轶;刘剑;展思辉
  • 通讯作者：
    展思辉
应用于MEMS的单晶硅上无电镀铜、
  • DOI：
    --
  • 发表时间：
    --
  • 期刊：
    半导体学报，第26卷，第5期，pp.1059-1064，2005年5月。
  • 影响因子：
    --
  • 作者：
    韩翔;李轶;吴文刚;闫桂珍;郝
  • 通讯作者：
    郝
The Computation of Private Set Intersection Cardinality over Complex Number
复数上私有集合交基数的计算
  • DOI：
    10.12677/csa.2021.116170
  • 发表时间：
    2021
  • 期刊：
    计算机科学与应用
  • 影响因子：
    --
  • 作者：
    唐桐;李轶;吴文渊;冯勇
  • 通讯作者：
    冯勇
RNAi干扰Ska2对H1299细胞增殖、迁移及侵袭能力的影响
  • DOI：
    --
  • 发表时间：
    2014
  • 期刊：
    中国细胞生物学学报
  • 影响因子：
    --
  • 作者：
    张莹;朱慧芳;李轶;卜友泉
  • 通讯作者：
    卜友泉

其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI：
    {{ item.doi || "--" }}
  • 发表时间：
    {{ item.publish_year || "--"}}
  • 期刊：
    {{ item.journal_name }}
  • 影响因子：
    {{ item.factor || "--" }}
  • 作者：
    {{ item.authors }}
  • 通讯作者：
    {{ item.author }}
empty
内容获取失败，请点击重试
重试联系客服
title开始分析
查看分析示例
此项目为已结题，我已根据课题信息分析并撰写以下内容，帮您拓宽课题思路：

AI项目思路

AI技术路线图

相似国自然基金

{{ item.name }}
  • 批准号：
    {{ item.ratify_no }}
  • 批准年份：
    {{ item.approval_year }}
  • 资助金额：
    {{ item.support_num }}
  • 项目类别：
    {{ item.project_type }}

相似海外基金

{{ item.name }}
{{ item.translate_name }}
  • 批准号：
    {{ item.ratify_no }}
  • 财政年份：
    {{ item.approval_year }}
  • 资助金额：
    {{ item.support_num }}
  • 项目类别：
    {{ item.project_type }}
{{ showInfoDetail.title }}

作者：{{ showInfoDetail.author }}

知道了

AI项目解读示例

课题项目：调控A型流感病毒诱导IFN-β表达的机制研究

AI项目摘要：

本研究聚焦于TRIM2蛋白在A型流感病毒诱导的IFN-β表达中的调控机制。A型流感病毒是全球性健康问题，其感染可导致严重的呼吸道疾病。IFN-β作为关键的抗病毒因子，其表达水平对抗病毒防御至关重要。然而，TRIM2如何调控IFN-β的表达尚未明确。本研究假设TRIM2通过与病毒RNA或宿主因子相互作用，影响IFN-β的产生。我们将采用分子生物学、细胞生物学和免疫学方法，探索TRIM2与A型流感病毒诱导IFN-β表达的关系。预期结果将揭示TRIM2在抗病毒免疫反应中的作用，为开发新的抗病毒策略提供理论基础。该研究对理解宿主抗病毒机制具有重要科学意义，并可能对临床治疗流感病毒感染提供新的视角。

AI项目思路：

科学问题：TRIM2如何调控A型流感病毒诱导的IFN-β表达？
前期研究：已有研究表明TRIM2参与抗病毒反应，但其具体机制尚不明确。
研究创新点：本研究将深入探讨TRIM2在IFN-β表达中的直接作用机制。
技术路线：包括病毒学、分子生物学、细胞培养和免疫检测技术。
关键技术：TRIM2与病毒RNA的相互作用分析，IFN-β启动子活性检测。
实验模型：使用A型流感病毒感染的细胞模型进行研究。

AI技术路线图

        graph TD
          A[研究起始] --> B[文献回顾与假设提出]
          B --> C[实验设计与方法学准备]
          C --> D[A型流感病毒感染模型建立]
          D --> E[TRIM2与病毒RNA相互作用分析]
          E --> F[TRIM2对IFN-β启动子活性的影响]
          F --> G[IFN-β表达水平测定]
          G --> H[TRIM2功能丧失与获得研究]
          H --> I[数据收集与分析]
          I --> J[结果解释与科学验证]
          J --> K[研究结论与未来方向]
          K --> L[研究结束]
关闭
close
客服二维码