软件工程组开放讨论班（No.4）

时  间：2013年9月24日18:30               地  点：计算机楼229

主持人：王林章 副教授

报告一：Steering Symbolic Execution to Less Traveled Paths

报告人：李游

简介：Symbolic execution is a promising testing and analysis methodology. It systematically explores a program’s execution space and can generate test cases with high coverage. One significant practical challenge for symbolic execution is how to effectively explore the enormous number of program paths in real-world programs. Various heuristics have been proposed for guiding symbolic execution, but they are generally inefficient and ad-hoc. In this paper, we introduce a novel, unified strategy to guide symbolic execution to less explored parts of a program. Our key idea is to exploit a specific type of path spectra, namely the length-n subpath program spectra, to systematically approximate full path information for guiding path exploration. In particular, we use frequency distributions of explored length-n subpaths to prioritize “less traveled” parts of the program to improve test coverage and error detection. We have implemented our general strategy in KLEE, a state-of-the-art symbolic execution engine. Evaluation results on the GNU Coreutils programs show that (1) varying the length n captures program-specific information and exhibits different degrees of effectiveness, and (2) our general approach outperforms traditional strategies in both coverage and error detection.

报告二：Computing and Proving Node Set Properties in Scope Logic

报告人：汤震浩

简介：Scope Logic, as an extension to Hoare Logic, is born to deal with pointers and recursive data structures. Firstly, in this talk, I will show basic concepts and features of Scope Logic. Secondly, I will demonstrate how to prove a program in Scope Logic using some basic facilities. Then, some previous work to compute and prove NodeSet properties automatically will be introduced. NodeSet property of a data structure is the set of nodes that can be reached from a pointer. This information is very useful in proving programs. For instance, it can broaden the usage of Weakest Precondition (WP), which can only deal with formulas containing no user-defined functions. Finally, I will come to a conclusion and introduce our future work.

报告三：模块化设备驱动程序开发途径研究

报告人：张一帆


简介：设备驱动程序是计算机系统中最重要的组成部分之一，应用程序和操作系统都需要通过设备驱动程序对外设进行管理和操作。此外，设备驱动程序代码在现代操作系统中占据了非常大的比重，同时也是操作系统中各类错误最主要的源头。设备驱动程序体量庞大且易于出错是由其自身复杂性较高所决定的。针对上述问题，报告从分析设备驱动程序特点开始，提出一种模块化设备驱动开发方法，以降低开发复杂度、提高复用性和减少错误；并介绍运用这一方法，针对以太网网卡类设备设计的开发框架。最后对下一步的工作进行介绍和讨论。