【摘 要】
：
程序验证中的常见情景是判断某个用户指定的性质在程序执行之后或执行过程中的某个程序点上是否成立。人工的形式化验证过程繁琐且容易出错,因此形式化验证的自动化是提高代
【机 构】
：
南京大学计算机软件新技术国家重点实验室
【基金项目】
：
国家自然科学基金资助项目（91118007）资助
论文部分内容阅读
程序验证中的常见情景是判断某个用户指定的性质在程序执行之后或执行过程中的某个程序点上是否成立。人工的形式化验证过程繁琐且容易出错,因此形式化验证的自动化是提高代码验证效率的重要方法。数据流分析技术是一种能够自动发现程序中某类性质的技术。研究了将一种数据流分析技术（单链表形状分析）和基于Scope Logic的代码验证过程相结合的方法。通过数据流分析获得所有程序点上的单链表可达性性质,将结果表达为带有递归函数的一阶逻辑公式,并将其插入到相应程序点中。分析程序还根据Scope Logic的证明法则设定了这些公
其他文献
介绍了利用Ｉｎｔｅｒｎｅｔ进行远程机械故障诊断的技术。重点介绍了远程诊断专家系统和远程信号处理系统的方法，同时介绍了动态网页，ＣＯＲＢＡ等技术在其中的应用。
分析了MapX的特点和车辆监控系统的基本要求 ,以及利用MapX实现基于MAPINFO矢量地图的图层、图标控制、地理信息控制、用户信息控制以及轨迹回放等电子地图控制的方法
文章针对焊件检测过程中需大量采集和分析实时图像的要求,利用小波分析的特点,相关跟踪识别视频图像运动状态,实现自动采集、分析处理和储存一并完成,解决了视频图像连续捕获
在信号处理领域中,互相关运算对于寻找未知信号中的特性具有重要的作用.互相关常被用于图像匹配、粒子图像测速等领域.针对互相关运算计算量大而实时系统中要求较快运算速度
提出了一类新的蕴涵算子族L-λ-Π,说明了它是ukasiewicz蕴涵算子、Goguen蕴涵算子更一般的形式。基于该算子族,给出了模糊推理FMP模型、FMT模型的三I支持算法和α-三I支持
在测试工程学中,应用测试生成树构建测试序列是相关测试方法的基础步骤,在传统测试生成树的基础上加入约束集的概念,使产生的测试生成树符合生产实际。同时在面向状态识别的测试方法中,考虑约束集对所生成状态区分序列的影响,基于带约束的测试生成树产生相应的特征集、状态识别集和UIO序列,提出或者改进了相应的算法。同时将测试方法扩展到了NFSM的情形下,提出了NFSM模型中前缀序列的生成算法和状态识别集的构建算
理解开发者的合作行为是促进开源社区协作开发的关键一步。已有文献主要对社区成员的加入与迁移展开研究,而对社区中已有开发者之间的实际合作行为关注甚少。主要从开发者的交互关系与个人技能两个角度出发,探析社区已有开发者如何建立新合作以及哪些因素影响他们的合作。应用Sourceforge.net平台公开的数据进行实验,结果表明不同的开发者的偏好合作模式不同,拓扑距离上的优势("朋友的朋友"关系)对开发者间首
随着云计算、大数据等新技术的发展和成熟,传统网络架构已不能满足现代业务的需求,软件定义网络(Software Defined Network,SDN)应运而生.但随着SDN技术的发展,其安全问题越来越突出.攻击者可以利用感染应用层、SDN控制器、OpenFlow协议的漏洞等来进行攻击,影响正常通信,威胁数据安全,甚至获取整个网络的控制权.针对上述可能出现的攻击,提出了一种面向SDN的网络溯源系统,
基于英特尔集成众核（Many Integrated Core,MIC）架构,将有限元网格积分算法在至强融核（Xeon Phi）协处理器做了移植和性能分析.该应用全面测试了有限元分析的核心计算过程在MIC上
网络协议是网络通信中一系列标准的集合,未知协议的识别和分析对网络监管、保障网络安全具有重大意义。协议识别技术多种多样,但大都不适用于二进制的协议识别。在此针对现有的协议识别技术的局限性,提出了一种在双方单协议通信环境下的多种类型二进制数据帧的协议识别方法。该方法首先利用n-gram技术对数据帧进行分割,然后利用无监督的特征选择算法提取特征串集合,从而利用聚类算法实现协议消息的识别。最后在ICMP上