摘要：从HDL设计描述中提取电路在VLSI设计验证、低功耗分析、测试生成等方面有广泛的应用需求。提出了一种采用程序切片技术实现的新的电路提取方法,并深入论述了基于程序切片技术从Verilog描述中进行电路提取的理论基础。该方法可以为每一个感兴趣的信号获取其"链接切片"。与以前的方法相比,该方法的优点是细粒度的、不受书写格式的限制,并且能处理更多Verilog的语法元素。该方法已经被集成到现有设计流程中,实验结果表明其方便、高效,有良好的通用性。

摘要：针对目前程序切片方法较单一,且其模块性和程序语言适应性较差,提出一种新型的形式化程序切片方法—基于模块单子语义的切片方法.通过设计切片单子转换器,切片这一类计算被抽象成独立于具体语言的切片单子转换器,它可模块化地加载到实际程序中,得到相应的模块单子切片算法.这种模块化的抽象机制使得单子切片算法具有较强的模块性和语言适应性.还给出切片单子转换器的若干性质,并证明模块单子切片算法的正确性和终止性,同时研究单子切片算法与基于图可达性切片算法间的联系.

摘要：针对Ｃ语言的特点，文中引入了Ｃ程序的一些重要概念，诸如数据依赖、控制依赖和程序依赖等。在分析Ｃ程序的程序依赖性的基础上，介绍了作者设计并实现的一个Ｃ程序切片系统，其中包括系统的概要设计思想，系统中使用的数据结构以及切片生成算法。Ｃ程序切片系统不仅可用于产生Ｃ程序的切片，而且可用于观察Ｃ程序的框架结构和有关变量的多种数据字典。所有这些结果，为Ｃ程序的测试、排错与维护提供许多有用的信息，对Ｃ程序的并行性检测、波动分析和复杂性度量提供有力的支持。

摘要：符号执行技术以其良好的精确度控制被广泛应用于程序分析领域,它将程序中变量的值用抽象的符号表示,模拟真实的程序执行.由于其路径敏感,在分析过程中会带来严重的状态爆炸问题.提出针对缺陷的程序切片方法来缓解这一问题,首先根据用户关心的缺陷生成源程序的切片准则,然后分析源代码生成数据依赖图和控制依赖图,由两者构成程序依赖图,再根据切片准则做程序切片,将源程序规模缩小,最后将切片后的程序交给程序分析工具分析.在符号执行分析工具ShapeChecker上的实验结果表明,提出的方法具有良好的效果.

摘要：当前程序切片的相关理论已经较为成熟,但针对Java程序的静态切片工具却非常少见。为便于展开切片应用研究,设计并实现了一个基于系统依赖图的Eclipse切片插件——Slithice。该插件支持不同粒度的底层分析和系统依赖图构建,从而可以使切片算法能够在精度和性能之间进行权衡,适应各种规模程序的分析需要。

摘要：Exception是一类特殊的对象,它在 Java方法出错时被创建,并利用 try/catch/finally机制抛出、处理异常。本文提出了一种合理的新方法,在系统依赖图中表示异常处理模块,利用图可达性算法实现了 Java程序切片。

摘要：模型检查技术在硬件和协议设计方面已经取得很大成功,但在软件验证方面仍存在很多困难。其主要问题是如何从源代码中自动抽取验证所要模型并精简其状态空间。文中通过对程序切片技术的研究,来解决并发程序验证的建模问题,包括把验证公式映射到切片准则,并把得到的程序切片转化为验证所需的模型。经程序切片处理后,软件模型检查效率得到提高。

摘要：程序切片是一种程序分析技术,它主要应用在程序的调试和逆向工程。文中介绍了笔者设计并实现的一个C++程序切片系统。其中包括系统的总体框架,系统中使用的数据结构以及切片生成算法。本系统已经成功应用到了X型导弹指挥软件的故障诊断中。

摘要：并发程序切片是并发程序分析的一种重要手段。针对多线程共享变量通信机制,在通过程序分析工具CodeSurfer获取程序基本信息的基础上构造程序可达图,生成以程序状态和语句二元组为节点的并发程序依赖图,实现了基于程序可达图的并发程序切片原型系统。初步实验结果表明,与传统的切片方法相比,采用基于程序可达图的并发程序切片方法,可有效地解决依赖关系不可传递问题,获得高精度的并发程序切片。

摘要：程序切片技术可以有效地运用在程序调试之中,但因为JavaScript语言动态的特性,传统的程序切片技术难以直接运用在JavaScript程序上。本文提出一种新的动态切片技术,结合JavaScript自身的语言特性,扩展了系统依赖图对于JavaScript程序的定义,设计并实现了系统依赖图的构建算法,最后基于系统依赖图进行了程序的切片工作。实验结果表明,该技术可以有效地运用在JavaScript程序的动态程序切片中,切片结果占原程序的比重较小。