动态数据结构的形状性质与数据约束：基于分离逻辑的自动分析与验证

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

基本信息

  • 批准号：
    61472474
  • 项目类别：
    面上项目
  • 资助金额：
    60.0万
  • 负责人：
    吴志林
  • 依托单位：
    中国科学院软件研究所
  • 学科分类：
    F0201.计算机科学的基础理论
  • 结题年份：
    2018
  • 批准年份：
    2014
  • 项目状态：
    已结题
  • 起止时间：
    2015-01-01 至2018-12-31

项目摘要

The correctness of computer software is vital for the smooth operation of information society. Since dynamic data structures are widely used in fundamental software codes, ensuring the correctness of programs with dynamic data structures is critical for the correctness of software systems.Separation logic is an extension of Hoare logic proposed around the year 2000, with the virtue of the local reasoning of the properties of programs with dynamic data structures. Separation logic has become a research hotpot of the program analysis and verification field in the last decades. Although most of the known work of separation logic focuses on shape properties (topology), the scalar data stored in the cells are also essential for the behavior of programs. The goal of this project is to analyze and verify automatically both shape properties and data constraints of programs with dynamic data structures. At first, we plan to extend separation logic with data constraints, and identify the fragments which achieve a good balance between expressiveness and decidability/complexity. Then, we consider to establish a framework of abstract interpretation by taking as the abstract domain the set of formulas in the identified decidable fragments, in order to analyze and verify automatically the behavior of programs. Meanwhile, we plan to investigate the integration of abstract interpretation with abstraction and refinement technique, as well as consider the modular verification of the programs containing procedure calls.
计算机软件的正确性对于保证信息社会的正常运行至关重要。动态数据结构在各种基础软件代码中被广泛使用，保证具有动态数据结构的程序的正确性对于保证软件的正确性非常关键。分离逻辑是2000年左右由研究人员提出的Hoare逻辑的一种扩展，其优点是可以对具有动态数据结构的程序的行为进行局部化的推理。分离逻辑近十年来成为程序分析与验证领域的一个研究热点。虽然分离逻辑已有的大部分工作集中在形状性质（拓扑结构）方面，但程序的行为也与存储单元中的标量数据密切相关。本项目拟基于分离逻辑对含有动态数据结构的程序的形状性质与数据约束同时进行自动的分析与验证。首先我们对分离逻辑进行扩展以包含数据约束，寻找在表达能力与可判定性/复杂性方面取得良好平衡的子集。然后，以得到的可判定子集的公式集为抽象域，建立抽象解释的框架来对程序进行自动的分析与验证。同时，考虑引入抽象求精技术，并探讨对含有过程调用的程序进行模块化的验证。

结项摘要

计算机软件的正确性对于保证信息社会的正常运行至关重要。动态数据结构在各种基础软件代码中被广泛使用，保证具有动态数据结构的程序的正确性对于保证软件的正确性非常关键。.分离逻辑是2000年左右由研究人员提出的Hoare逻辑的一种扩展，其优点是可以对具有动态数据结构的程序的行为进行局部化的推理。分离逻辑近十年来成为程序分析与验证领域的一个研究热点。虽然分离逻辑已有的大部分工作集中在形状性质（拓扑结构）方面，但程序的行为也与存储单元中的标量数据密切相关。本项目基于分离逻辑对含有动态数据结构的程序的形状性质与数据约束同时进行自动的分析与验证。.首先，我们寻找能描述数据约束的、在表达能力与可判定性/复杂性方面取得良好平衡的分离逻辑的子集，取得了以下成果：.-- 我们探讨了分离逻辑蕴涵问题证明过程中的引理自动生成问题，提出了分离逻辑的可组合归纳谓词的概念，从而大大简化了分离逻辑公式的蕴涵问题的求解.-- 我们提出了可以描述线性数据结构的算术数据约束和集合数据约束的含有线性可组合归纳谓词的分离逻辑的子集，设计了其可满足性问题和蕴涵问题的判定算法，并实现了分离逻辑求解器COMPSPEN，并参加了分离逻辑求解器竞赛SL-COMP 2018；.-- 我们为树结构上的分离逻辑的带算术数据约束扩展的子集基于自动机理论设计了判定算法；.-- 我们证明了含有双链表片段的分离逻辑子集的可满足性问题是NP完全的，而Cook等人关于单链表片段的分离逻辑子集的多项式可解性结果可以扩展到树结构上。.而且，我们以得到的可判定子集的公式集为抽象域，初步建立了抽象解释的框架来对程序进行自动的分析与验证。

项目成果

期刊论文数量（5）
专著数量（0）
科研奖励数量（0）
会议论文数量（23）
专利数量（0）
On temporal logics with data variable quantifications: Decidability and complexity
关于具有数据变量量化的时态逻辑：可判定性和复杂性
  • DOI：
    10.1016/j.ic.2016.08.002
  • 发表时间：
    2016-12
  • 期刊：
    Information and Computation
  • 影响因子：
    1
  • 作者：
    Fu Song;Zhilin Wu
  • 通讯作者：
    Zhilin Wu
Multiconstraint Static Scheduling of Synchronous Dataflow Graphs Via Retiming and Unfolding
通过重定时和展开的同步数据流图的多约束静态调度
  • DOI：
    10.1109/tcad.2015.2495167
  • 发表时间：
    2016
  • 期刊：
    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
  • 影响因子：
    2.9
  • 作者：
    Zhu Xue-Yang;Geilen Marc;Basten Twan;Stuijk S;er
  • 通讯作者：
    er
基于模型的嵌入式系统性能分析框架
  • DOI：
    --
  • 发表时间：
    2016
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    朱雪阳
  • 通讯作者：
    朱雪阳

数据更新时间：{{ 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 }}

其他文献

手枪弹对带软防护明胶靶标侵彻机理与实验研究
  • DOI：
    --
  • 发表时间：
    --
  • 期刊：
    兵工学报
  • 影响因子：
    --
  • 作者：
    刘坤;吴志林;宁建国;任会兰;李忠新
  • 通讯作者：
    李忠新
面向无穷数据的形式模型综述
  • DOI：
    10.13328/j.cnki.jos.004989
  • 发表时间：
    2016
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    宋富;吴志林
  • 通讯作者：
    吴志林
COMPSPEN: 对形状性质与数据约束进行融合推理的分离逻辑求解器
  • DOI：
    --
  • 发表时间：
    2021
  • 期刊：
    软件学报
  • 影响因子：
    --
  • 作者：
    苏婉昀;高冲;古新才;吴志林
  • 通讯作者：
    吴志林
分散剂对FSP制备IMC/Al复合材料组织与拉伸性能的影响
  • DOI：
    --
  • 发表时间：
    2017
  • 期刊：
    机械工程材料
  • 影响因子：
    --
  • 作者：
    吴志林;黄春平;王承剑;黄硕文
  • 通讯作者：
    黄硕文
球形破片侵彻明胶运动模型对比研究
  • DOI：
    --
  • 发表时间：
    2017
  • 期刊：
    中国科学:技术科学
  • 影响因子：
    --
  • 作者：
    刘坤;宁建国;吴志林;李忠新;任会兰
  • 通讯作者：
    任会兰

其他文献

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

AI项目思路

AI技术路线图

吴志林的其他基金

分布式流处理程序的分析与验证
  • 批准号：
    61872340
  • 批准年份：
    2018
  • 资助金额：
    63.0 万元
  • 项目类别：
    面上项目
无穷字母表上的形式模型：逻辑与自动机
  • 批准号：
    61100062
  • 批准年份：
    2011
  • 资助金额：
    21.0 万元
  • 项目类别：
    青年科学基金项目

相似国自然基金

{{ 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
客服二维码