抽象解释及其应用研究进展

1

作者 陈立前 范广生 +1 位作者 尹帮虎 王戟 《计算机研究与发展》 EI CSCD 北大核心 2023年第2期227-247,共21页

抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来,... 抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论.抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用.近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展.基于此,系统综述了抽象解释及其应用的研究进展.首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展;之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向. 展开更多

关键词 抽象解释 程序语义 程序分析 形式验证 抽象域

下载PDF 职称材料

含有析取语义循环的不变式生成改进方法 被引量：4

2

作者 潘建东 陈立前 +2 位作者 黄达明 孙浩 曾庆凯 《软件学报》 EI CSCD 北大核心 2016年第7期1741-1756,共16页

抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显... 抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理. 展开更多

关键词 抽象解释 抽象域 不变式 析取语义 循环分解

下载PDF 职称材料

算法语言L的设计与形式规范 被引量：1

3

作者 王岩冰 张家重 刘弘 《计算机研究与发展》 EI CSCD 北大核心 1996年第4期248-255,共8页

本文通过分析ＰＡＳＣＡＬ语言作为算法设计语言而存在的主要缺陷，借鉴Ｄ．Ｗａｔｔ的面之设计原则，而定义了一个小型的算法语言Ｌ。文中详细给出了它的具体文法、抽象文法和静态语义。通过Ｌ的设计和描述，对算法语言设计与规范的有... 本文通过分析ＰＡＳＣＡＬ语言作为算法设计语言而存在的主要缺陷，借鉴Ｄ．Ｗａｔｔ的面之设计原则，而定义了一个小型的算法语言Ｌ。文中详细给出了它的具体文法、抽象文法和静态语义。通过Ｌ的设计和描述，对算法语言设计与规范的有关问题进行了有益的探索。 展开更多

关键词 算法语言 PASCAL语言 形式规范 程序语言

下载PDF 职称材料

抽象语义引导的空指针引用自动修复

4

作者 王珣 孙玉雪 +2 位作者 董玉坤 位欣欣 唐道龙 《计算机系统应用》 2023年第1期376-384,共9页

程序依赖图往往只能根据语句中变量的定义使用关系来判定数据依赖而无法从语义上精准判断,从而容易引入虚假依赖关系,使得缺陷修复的过程中使用错误信息造成修复失败.因此,本文将利用抽象属性对与空对象或空指针有关的虚假依赖进行剪枝... 程序依赖图往往只能根据语句中变量的定义使用关系来判定数据依赖而无法从语义上精准判断,从而容易引入虚假依赖关系,使得缺陷修复的过程中使用错误信息造成修复失败.因此,本文将利用抽象属性对与空对象或空指针有关的虚假依赖进行剪枝,提出基于抽象语义的程序依赖图减少与程序缺陷语义无关的依赖关系分析,以完成空指针引用修复.依据分析获取的依赖关系,在空指针引用的不同修复策略的指导下实现一种多策略的修复方案,在尽可能减小修复副作用的前提下完成空指针引用缺陷的修复.本文利用Defects4J中的空指针引用对实现的修复工具DTSFix进行实验评估,结果显示DTSFix的修复效果远远高于对比工具,证明了方法的有效性. 展开更多

关键词 抽象语义 程序依赖图 程序自动修复 空指针引用 修复策略

下载PDF 职称材料

Statecharts的形式化验证研究 被引量：1

5

作者 钱俊彦 古天龙 赵岭忠 《计算机工程》 EI CAS CSCD 北大核心 2005年第18期19-21,24,共4页

给出了Statecharts的抽象语法描述,以及Statecharts各个构成元素的语义,包括状态、迁移、事件和条件、表达式、动作和当前状态格局的语义函数等,并给出Statecharts一步的操作语义。然后在此基础上把一个图形化的语言转换为文本的方式来... 给出了Statecharts的抽象语法描述,以及Statecharts各个构成元素的语义,包括状态、迁移、事件和条件、表达式、动作和当前状态格局的语义函数等,并给出Statecharts一步的操作语义。然后在此基础上把一个图形化的语言转换为文本的方式来描述,并对Statecharts进行形式化分析及验证。 展开更多

关键词 STATECHARTS 抽象语法 操作语义 一步

下载PDF 职称材料

关于抽象逻辑紧致性的一个定理 被引量：2

6

作者 王国俊 《陕西师范大学学报（自然科学版）》 CAS CSCD 北大核心 2000年第1期1-4,共4页

以模糊语义为背景 ,在标号集具有一定结构的一族全序完备格的乘积上引入了抽象语义及其连续性概念 ,证明了具有这种连续性的抽象语义是紧致的 ,由此可以推出取值于 [0 。

关键词 模糊推理 完备格 抽象语义 紧致性

下载PDF 职称材料

抽象图形在音乐形象设计中的运用 被引量：1

7

作者 陈瞻 《包装工程》 CAS CSCD 北大核心 2007年第2期151-152,共2页

对抽象图形在音乐招帖与唱片封套设计中的运用进行了研究,通过形式上的分析,了解并掌握抽象图形运用的基本方法,有针对性的提高音乐形象设计的表现力。

关键词 抽象图形 音乐形象设计 再现性的语义抽象图形 非再现性的抽象表现

下载PDF 职称材料

开放系统之间语义的传送:实例研究 被引量：1

8

作者 杨仲华 张汝澜 《系统工程与电子技术》 EI CSCD 1991年第2期1-18,共18页

开放系统互连(OSI)的主要目标是实现驻留在不同系统中的应用之间的互通与互操作。这要求在这些系统之间正确地传送应用语义。本文以文卷传送为实例,阐述了OSI为实现语义传送而提出的概念、工具与标准,探讨了这个在OSI中较为难以理解的... 开放系统互连(OSI)的主要目标是实现驻留在不同系统中的应用之间的互通与互操作。这要求在这些系统之间正确地传送应用语义。本文以文卷传送为实例,阐述了OSI为实现语义传送而提出的概念、工具与标准,探讨了这个在OSI中较为难以理解的领域。 展开更多

关键词 开放系统 语义 计算机网络 OSI

下载PDF 职称材料

基于抽象解释的Prolog程序验证技术研究 被引量：1

9

作者 赵岭忠 古天龙 +1 位作者 蔡国永 钱俊彦 《计算机科学》 CSCD 北大核心 2008年第7期261-268,共8页

作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中。现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键。... 作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中。现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键。本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性。本文例子表明了该验证方法的有效性。 展开更多

关键词 抽象解释 程序验证 PROLOG 不动点语义

下载PDF 职称材料

抽象解释全总域模型

10

作者 王蓁蓁 倪庆剑 +1 位作者 张志政 邢汉承 《中国科学技术大学学报》 CAS CSCD 北大核心 2014年第7期599-604,共6页

抽象解释自1977年提出后,许多作者做了大量工作,将抽象解释理论应用于程序分析和验证研究等领域.本文为有关抽象解释论述构造了一个统一模型,称为抽象解释的全总域模型,目前现存的有关抽象解释文献所采取的框架都相容于全总域模型,且是... 抽象解释自1977年提出后,许多作者做了大量工作,将抽象解释理论应用于程序分析和验证研究等领域.本文为有关抽象解释论述构造了一个统一模型,称为抽象解释的全总域模型,目前现存的有关抽象解释文献所采取的框架都相容于全总域模型,且是等价的.在此基础上,我们还提出有关抽象解释理论需要解决的几个基本问题.模型和问题都可以作为今后抽象解释理论发展的参考基点. 展开更多

关键词 抽象解释 语义 全总域 完备性

下载PDF 职称材料

Smalltalk-80的形式语义研究

11

作者 李舟军 王兵山 《国防科技大学学报》 EI CAS CSCD 北大核心 1993年第3期80-89,共10页

Smalltalk-80是原型的面向对象程序设计语言和环境。本文简要地介绍了Smalltalk-80的基本概念和抽象文法,给出了其形式模型,并基于该模型描述了Smalltalk-80的静态指称语义和动态指称语义。

关键词 面向对象 程序设计 SMALLTALK-80

下载PDF 职称材料

基于抽象解释的数据迷惑正确性分析

12

作者 曾颖 《信息工程大学学报》 2011年第6期670-675,共6页

数据迷惑是代码迷惑中重要的一类迷惑变换,在软件保护领域中应用广泛,常被用于防止攻击者对程序进行数据流分析、程序切片等逆向工程攻击。从语义的角度,给出了一种基于抽象解释的数据迷惑正确性的分析方法。首先使用抽象解释理论,从程... 数据迷惑是代码迷惑中重要的一类迷惑变换,在软件保护领域中应用广泛,常被用于防止攻击者对程序进行数据流分析、程序切片等逆向工程攻击。从语义的角度,给出了一种基于抽象解释的数据迷惑正确性的分析方法。首先使用抽象解释理论,从程序语义的角度,对数据迷惑进行形式化描述,用一种语义变换形式化地描述数据迷惑。然后在形式化描述的基础上,由语义变换和语法变换之间的关系,构造得到数据迷惑算法。最后在基于抽象解释的数据迷惑的形式化描述的基础上,对数据迷惑变换的正确性进行分析和讨论。 展开更多

关键词 数据迷惑 抽象解释 正确性 程序语义 程序变换

下载PDF 职称材料

自然语言句子抽象语义表示AMR研究综述 被引量：19

13

作者 曲维光 周俊生 +3 位作者 吴晓东 戴茹冰 顾敏 顾彦慧 《数据采集与处理》 CSCD 北大核心 2017年第1期26-36,共11页

句子的语义处理是自然语言处理的重要难题与挑战。抽象语义表示(Abstract meaning representation,AMR)是近几年国际上新兴的句子级语义表示方法,突破了传统的句法树结构的限制,将一个句子语义抽象为一个单根有向无环图,很好地解决了论... 句子的语义处理是自然语言处理的重要难题与挑战。抽象语义表示(Abstract meaning representation,AMR)是近几年国际上新兴的句子级语义表示方法,突破了传统的句法树结构的限制,将一个句子语义抽象为一个单根有向无环图,很好地解决了论元共享问题,成为语言资源建设和句子语义解析的研究热点。本文从AMR概念与规范、解析算法和应用等方面对AMR相关研究进行系统的梳理,特别对AMR的各种解析算法进行了比较深入的分析和比较,指出了现有算法存在的问题和不足,同时介绍了中文AMR的开发进展,最后展望了AMR未来的研究方向。 展开更多

关键词 抽象语义表示 句法语义 语义解析 自然语言处理

下载PDF 职称材料

背景关联世界中抽象数据类型的关联性 被引量：2

14

作者 赵愚 钟珞 《四川建材学院学报》 1992年第1期76-82,共7页

基于背景关联世界理论,本文提出了认识模式中抽象数据类型的关联等价与关联性扩充的概念。并认为关联等价揭示了思维活动中的模式识别过程和再认现象;关联性扩充则揭示了科学的发现过程;以及关联性扩充思想在计算机软件工程中的应用。

关键词 计算机 抽象数据类型 关联

下载PDF 职称材料

基于动态规划的优先语义扩充求解算法

15

作者 熊才权 宗泽华 吴歆韵 《计算机应用研究》 CSCD 北大核心 2022年第5期1343-1348,共6页

抽象辩论框架中的优先语义是判断争议可接受程度的最重要语义。现有优先扩充求解方法多用标记映射求解,依赖于标记的定义、转换规则、相邻争议的标记。算法每次迭代会产生一个新的抽象辩论框架导致时间、空间复杂度较高。提出一种基于... 抽象辩论框架中的优先语义是判断争议可接受程度的最重要语义。现有优先扩充求解方法多用标记映射求解,依赖于标记的定义、转换规则、相邻争议的标记。算法每次迭代会产生一个新的抽象辩论框架导致时间、空间复杂度较高。提出一种基于动态规划的优先扩充算法,在动态规划中加入争议可接受性判断,求出辩论框架中极大可容许集得到优先扩充。在基于随机抽象辩论框架与ICCMA提供的数据集进行实验,同Heureka、ArgSemSAT等算法进行对比。结果表明,求解相同数量的优先扩充,算法耗时较少,时间、空间复杂度有所降低。 展开更多

关键词 抽象辩论框架 语义扩充 可容许集 优先扩充

下载PDF 职称材料

顺序图与状态图的递归语义一致性研究 被引量：1

16

作者 周翔 邵志清 《计算机科学》 CSCD 北大核心 2010年第8期172-174,223,共4页

建模面向对象的软件系统是UML的动态图的重要应用,采用顺序图描述消息传送,动态图描述活动。在大型系统开发过程中,往往存在大量顺序图和状态图,由于语义的缺失,导致这些图形表达涵义模糊不清,特别是在递归的信息传送上,由于表达方式的... 建模面向对象的软件系统是UML的动态图的重要应用,采用顺序图描述消息传送,动态图描述活动。在大型系统开发过程中,往往存在大量顺序图和状态图,由于语义的缺失,导致这些图形表达涵义模糊不清,特别是在递归的信息传送上,由于表达方式的特点,状态图很容易造成实现过程的歧义甚至死锁。提出了基于ASM的多agent实时控制方法,结合形式化的规则定义,通过多个层次agent控制状态的跃迁,保证状态图在描述复杂信息传送时,能够和顺序图的时序保持一致,这对提高系统的可靠性具有一定的现实意义。 展开更多

关键词 顺序图 状态图 ASM 递归语义

下载PDF 职称材料

基于操作语义的时间隐通道分析 被引量：1

17

作者 戴梅 孙国强 刘志锋 《计算机工程与设计》 CSCD 北大核心 2009年第7期1593-1595,1599,共4页

主要讨论了计算机信息安全领域中比较热点的话题——基于操作语义的时间隐通道。根据隐通道中的时间隐通道的特点和存在的最小条件,针对其特点提出了一种搜索方法。该搜索方法将进程看作一个抽象机状态机,以Plotkin的结构化操作语义等... 主要讨论了计算机信息安全领域中比较热点的话题——基于操作语义的时间隐通道。根据隐通道中的时间隐通道的特点和存在的最小条件,针对其特点提出了一种搜索方法。该搜索方法将进程看作一个抽象机状态机,以Plotkin的结构化操作语义等推导规则为基础,以及完整的信息传导操作语义的模型,分析了两个高低安全级进程抽象机状态变化及其状态动态变化序列,最后对可视窗口的分析,可以找到其中存在的时间隐通道。 展开更多

关键词 隐通道 时间隐通道 抽象机 信息传导 结构化操作语义

下载PDF 职称材料

抽象论辩系统的动态性分析

18

作者 徐康 廖备水 《重庆理工大学学报（社会科学）》 CAS 2017年第8期6-13,共8页

抽象论辩系统是一种非单调推理系统,它随底层的知识或信息的变化而变化,这就是抽象论辩系统的动态性。如何刻画这种动态性是论辩理论研究领域的一个关键问题。抽象论辩系统的动态变化包括语法变化和语义变化,抽象论辩系统动态性研究着... 抽象论辩系统是一种非单调推理系统,它随底层的知识或信息的变化而变化,这就是抽象论辩系统的动态性。如何刻画这种动态性是论辩理论研究领域的一个关键问题。抽象论辩系统的动态变化包括语法变化和语义变化,抽象论辩系统动态性研究着重研究这二者之间的影响关系。文章总结了目前抽象论辩系统动态性研究的方向,包括动态语义求解的方法以及抽象论辩系统的修正;分析了抽象理论动态性研究的价值和意义;探讨了抽象论辩系统动态性研究的基本原理和研究方法。 展开更多

关键词 抽象论辩系统动态性 动态论辩语义求解 抽象论辩系统修正

下载PDF 职称材料

基于抽象机模式的Java虚拟机设计

19

作者 黄强 李峻 楼新远 《重庆通信学院学报》 2005年第3期24-26,31,共4页

Java虚拟机（JVM）作为Java程序与操作系统之间的桥梁，解决了Java程序在异构操作系统上运行的问题．但现有JVM功能模块之间的强耦合性，给JVM结构和指令集的扩展带来了困难．本文基于抽象机模式设计的JVM．通过将JVM的静态特性和动态... Java虚拟机（JVM）作为Java程序与操作系统之间的桥梁，解决了Java程序在异构操作系统上运行的问题．但现有JVM功能模块之间的强耦合性，给JVM结构和指令集的扩展带来了困难．本文基于抽象机模式设计的JVM．通过将JVM的静态特性和动态特性定义为分离组件来分散关注点，以及抽象机模式与JVM固有特性的结合实现的JVM具有松散的耦合度．可扩展的结构和指令集．以及易分配的指令语义． 展开更多

关键词 JAVA虚拟机 抽象机模式 指令集 指令语义

原文传递

抽象数据类型的极大代数语义

20

作者 吕文进 《贵州大学学报（自然科学版）》 1992年第1期38-43,共6页

传统的定义抽象数据类型语义的方法难以描述软件非形式说明和程序设计语言文本中的非确定性,为了弥补这种不足,本文引入了极大代数语义的概念并讨论了其性质。

关键词 抽象数据类型 代数语义 不确定性

下载PDF 职称材料