首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   17篇
  国内免费   1篇
  完全免费   22篇
  自动化技术   40篇
  2018年   1篇
  2017年   1篇
  2016年   2篇
  2015年   4篇
  2014年   4篇
  2013年   2篇
  2012年   3篇
  2011年   2篇
  2010年   6篇
  2009年   2篇
  2008年   3篇
  2007年   1篇
  2006年   5篇
  1996年   2篇
  1994年   2篇
排序方式: 共有40条查询结果,搜索用时 78 毫秒
1.
基于静态分析的安全漏洞检测技术研究   总被引:9,自引:0,他引:9       下载免费PDF全文
夏一民  罗军  张民选 《计算机科学》2006,33(10):279-282
消除软件中的安全漏洞是建立安全信息系统的前提。静态分析方法可以自动地提取软件的行为信息,从而检测出软件中的安全漏洞。和其它程序分析方法相比,该方法具有自动化程度高和检测速度快的优点。在本文中,我们首先描述了静态分析的理论基础,然后说明了类型推断、数据流分析和约束分析等主要静态分析方法及其在安全漏洞检测中的应用,并比较这些方法的优缺点。最后给出了几种支持安全漏洞静态检测的编程语言。  相似文献
2.
基于抽象解释的代码迷惑有效性比较框架   总被引:8,自引:0,他引:8  
高鹰  陈意云 《计算机学报》2007,30(5):806-814
代码迷惑是一种以增加理解难度为目的的程序变换技术,用来保护软件免遭逆向剖析.代码迷惑是否有效是代码迷惑研究中首要解决的问题.目前对有效性证明的研究大都是基于非语义的方式.文章将语义与有效性证明联系起来,建立了基于语义的代码迷惑有效性比较框架,该框架能够为迷惑算法在静态分析这样的限定环境下提供有效性证明,而且也能严格比较迷惑算法之间的有效性,最后使用实例描述比较框架如何应用到证明代码迷惑的有效性.  相似文献
3.
单变量区间线性不等式抽象域   总被引:3,自引:0,他引:3  
程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中.  相似文献
4.
基于抽象解释理论的程序验证技术   总被引:2,自引:0,他引:2       下载免费PDF全文
抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.  相似文献
5.
安全而又精确的值范围分析对编译器优化至关重要.系统地提出了一个基于抽象解释和通用单调数据流框架的值范围分析框架,包括精确的定叉、分析和完整的正确性证明.与一般的值范围分析方法不同,该框架不仅包括抽象解释,还包括与之对应的具体解释,以及相应的正确性证明.  相似文献
6.
基于完备抽象解释的模型检验CTL公式研究   总被引:1,自引:0,他引:1  
在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.  相似文献
7.
基于抽象解释的Prolog程序验证技术研究   总被引:1,自引:0,他引:1       下载免费PDF全文
作为一种通用的语义近似理论,抽象解释已广泛应用于各类程序的形式化验证中.现有基于抽象解释的逻辑程序验证技术未涉及与程序点相关联的程序性质的验证,设计能够描述此类性质的逻辑程序具体语义和抽象语义是构造相应验证工具的关键.本文给出了一种基于抽象解释的Prolog程序验证方法,该方法采用了具有路径信息的Prolog语义及其抽象作为语义基础,因而可用于验证与程序点相关联的程序特性.本文例子表明了该验证方法的有效性.  相似文献
8.
基于缺陷关联的静态分析优化   总被引:1,自引:0,他引:1       下载免费PDF全文
缺陷检测一般包括静态分析与人工审查两个阶段.静态检测工具报告大量缺陷,但是主要的缺陷确认工作仍由人工完成,这是一件费时、费力的工作.巨大的审查开销可能会导致软件开发人员拒绝使用该静态缺陷检测工具.提出一种可靠的基于缺陷关联的静态分析优化方法,能够分组静态检测工具所报告的缺陷,在分组后的任意一组缺陷中,如果其主导缺陷被证明是误报(或者是真实的),就能确认其他缺陷也是误报(也是真实的).实验结果表明,基于缺陷关联的静态分析优化方法在较小的时间和空间开销下减少了22%的缺陷审查工作,能够较好地适应于大型的关键嵌入式系统程序缺陷检测.  相似文献
9.
本文给出了在逻辑程序抽象解释的理论框架下进行模式推导的方法,并就其中的别名处理问题和定点计算问题进行了详细的讨论提出了一种正确,有铲的别名自理方法以及基于”护展表“的定点求解算法。该方案已用Prolog语言实现。  相似文献
10.
本文从实例分析总结了在宽度优先语义下对CLP(R)程序进行部分演绎的基本规则和两条特殊规则,首次提出了将抽象解释技术应用于CLP(R)程序的部分演绎的新课题。本文的结果虽然是初步的,但它是在CLP(R)程序的部分演绎这一研究方向上的首次尝试。  相似文献
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号