形状分析符号执行引擎中的状态合并

符号执行技术以其良好的精确度控制和代码覆盖率被广泛应用于静态程序分析和高覆盖率测试用例自动生成。 符号执行 在分析程序时,以模拟真实的程序执行过程的方式分析程序的数据流和控制流信息,并检查程序可能出现的所有状态,得到程序的分析结果。高精确度和高覆盖率要求对程序状态描述具体而完备,这会导致符号执行过程中常见的状态爆炸问题。首先提出在不同的执行路径上对具体内存状态进行合并的算法,然后对内存模型进行适度的抽象,扩大状态合并算法的适用范围,最后讨论状态合并所带来的实际效果,并提出了状态合并的优化解决方案。所提出的算法在符号执行引擎ShapeChecker上实现,并取得了良好的实验结果。     

单代号网络图的计算机辅助生成研究

研究了在绘制单代号网络图时,工序在深度上和宽度上的布置以及工序间折角形箭线在纵向上和横向上的布置问题,给出了它们的具体计算公式,并基于此提出了单代号网络计划图的布图模型．通过开发接口程序,实现了用Access管理网络数据和用AutoCAD打印出图;通过采用方框型来表达事项节点的形式,拓展了单代号网络图的表达信息．     

大粒度Pull Request描述自动生成

在GitHub平台中,许多项目贡献者在提交Pull Request(PR)时往往会忽略提交PR描述,这使得提交的PR容易被评审者忽略或者拒绝.因此,自动生成PR描述以帮助项目贡献者提高PR通过率是很有必要的.然而,现有PR描述生成方法的表现会受到PR粒度影响,无法有效为大粒度的PR生成描述.因此,该工作专注于大粒度PR...     

随程序规模动态调整的通道优化布线算法

针对常规层次型布图算法在大规模程序中布线混乱的缺点,借鉴Sugiyama层次布局算法,提出了一种随着程序规模动态调整的通道优化布线算法。通过将节点的通道数目与程序规模建立函数关系,以解决现有算法在布图时出现的线路重叠和效率低下的问题;在布图中结合广义张量平衡思想,以减少交叉并实现布图的美观性;并根据调用节点之间的相对位置关系,给出了相应的线路分配和申请策略,实现了布线的有序性。实践证明,该算法能够提高布图效率,有效地减少交叉,实现节点的有序布线和实现简单等优点。     

SVM based layout retargeting for fast and regularized inverse lithography

Inverse lithography technology （ILT）, also known as pixel-based optical proximity correction （PB-OPC）, has shown promising capability in pushing the current 193 nm lithography to its limit. By treating the mask optimization process as an inverse problem in lithography, ILT provides a more complete exploration of the solution space and better pattern fidelity than the tradi-tional edge-based OPC. However, the existing methods of ILT are extremely time-consuming due to the slow convergence of the optimization process. To address this issue, in this paper we propose a support vector machine （SVM） based layout retargeting method for ILT, which is designed to generate a good initial input mask for the optimization process and promote the convergence speed. Supervised by optimized masks of training layouts generated by conventional ILT, SVM models are learned and used to predict the initial pixel values in the‘undefined areas’ of the new layout. By this process, an initial input mask close to the final optimized mask of the new layout is generated, which reduces iterations needed in the following optimization process. Manu-facturability is another critical issue in ILT;however, the mask generated by our layout retargeting method is quite irregular due to the prediction inaccuracy of the SVM models. To compensate for this drawback, a spatial filter is employed to regularize the retargeted mask for complexity reduction. We implemented our layout retargeting method with a regularized level-set based ILT （LSB-ILT） algorithm under partially coherent illumination conditions. Experimental results show that with an initial input mask generated by our layout retargeting method, the number of iterations needed in the optimization process and runtime of the whole process in ILT are reduced by 70.8%and 69.0%, respectively.     

Symbolic approximation: an approach to verification in the large

This article describes symbolic approximation, a theoretical foundation for techniques evolved for large-scale verification – in particular, for post hoc verification of the C code in large-scale open-source projects such as the Linux kernel. The corresponding toolset’s increasing maturity means that it is now capable of treating millions of lines of C code source in a few hours on very modest support platforms. In order to explicitly manage the state-space-explosion problem that bedevils model-checking approaches, we work with approximations to programs in a symbolic domain where approximation has a well-defined meaning. A more approximate program means being able to say less about what the program does, which means weaker logic for reasoning about the program. So we adjust the approximation by adjusting the applied logic. That guarantees a safe approximation (one which may generate false alarms but no false negatives) provided the logic used is weaker than the exact logic of C. We choose the logic to suit the analysis.     

一种语音IC的设计

描述了一种语音IC的设计原理和掩膜编程方法。通过采用可编程阵列逻辑（PAL），使电路在语音信号的编码数据集成时达到较高的效率。掩膜版自动生成程序缩短了电路的应用开发周期，保证了掩膜版设计的正确性。     

SymFuzz:一种复杂路径条件下的漏洞检测技术

当前漏洞检测技术可以实现对小规模程序的快速检测,但对大型或路径条件复杂的程序进行检测时其效率低下。为实现复杂路径条件下的漏洞快速检测,文中提出了一种复杂路径条件下的漏洞检测技术SymFuzz。SymFuzz将导向式模糊测试技术与选择符号执行技术相结合,通过导向式模糊测试技术对程序路径进行过滤,利用选择符号执行技术对可能触发漏洞的路径进行求解。该技术首先通过静态分析获取程序漏洞信息;然后使用导向式模糊测试技术,快速生成可以覆盖漏洞函数的测试用例;最后对漏洞函数内可以触发漏洞的路径进行符号执行,生成触发程序漏洞的测试用例。文中基于AFL与S2E等开源项目实现了SymFuzz的原型系统。实验结果表明,SymFuzz与现有的模糊测试技术相比,在复杂路径条件下的漏洞检测效果提高显著。     

Automated design of MOS circuits and layout

As the integration size of VLSI chips increases, programmable logic arrays (PLAs) are indispensable for reducing chip design time. In many cases, however, PLAs are too larger or too slow. Here is presented a new approach to overcome such disadvantages. This produces a circuit of a smaller area and faster response time than PLAs, still maintaining the short design time. The approach works as follows: electronic circuits are automatically designed by an algorithm DIMN directly from given logic functions, and then a symbolic layout for them is automatically made by a program SIMON.     

A planar graph drawing program

This paper describes a program, written in FORTRAN, for a 64K I.C.L. 4130 which will accept data describing the ordering of nodes and branches within the regions of a planar graph, and generate a two-dimensional representation, without crossovers, from these data. The program was written to provide one of the basic ‘tools’ required in the development of a printed wiring board layout program for the electronics industry The program generates display code which is sent to a satellite PDP-7 computer driving a 340 display. On completion of the automatic drawing phase an interactive phase is entered in which the user can ‘tidy’ and label the drawing, by means of keyboard and light-pen commands Brief notes are included on the hardware, the data structures package (MINIJASP, derived from ASP) and the graphics package, employed.     

结合静态分析与动态符号执行的软件漏洞检测方法

动态符号执行是近年来新兴的一种软件漏洞检测方法,它可以为目标程序的不同执行路径自动生成测试用例,从而获得较高的测试代码覆盖率。然而,程序的执行路径很多,且大部分路径都是漏洞无关的,通常那些包含危险函数调用的路径更有可能通向漏洞。提出一种基于静态分析的有导动态符号执行方法,并实现了一个工具原型SAGDSE。该方法通过静态分析识别目标程序中调用危险函数的指令地址,在动态符号执行过程中遇到这些指令地址时收集危险路径约束,再通过约束求解生成走危险路径的测试用例,这些测试用例将更可能触发程序漏洞。实验结果表明了该方法的有效性。     

EFSM模型的字符串类型测试数据自动生成

基于软件描述模型的测试数据自动生成研究中,字符串类型测试数据生成是一个研究热点和难点。EFSM模型是一种重要的软件描述模型。分析了EFSM模型的特点,针对面向EFSM模型目标路径的字符串测试数据生成,建立了字符串输入变量模型和操作模型,结合静态测试的特点,给出了通过字符串变量模型在目标路径上的符号执行结果生成字符串类型测试数据的方法。实验结果表明,该方法能够达到预期效果,提高测试生成效率。     

Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis

Symbolic PathFinder (SPF) is a software analysis tool that combines symbolic execution with model checking for automated test case generation and error detection in Java bytecode programs. In SPF, programs are executed on symbolic inputs representing multiple concrete inputs and the values of program variables are represented by expressions over those symbolic inputs. Constraints over these expressions are generated from the analysis of different paths through the program. The constraints are solved with off-the-shelf solvers to determine path feasibility and to generate test inputs. Model checking is used to explore different symbolic program executions, to systematically handle aliasing in the input data structures, and to analyze the multithreading present in the code. SPF incorporates techniques for handling input data structures, strings, and native calls to external libraries, as well as for solving complex mathematical constraints. We describe the tool and its application at NASA, in academia, and in industry.