About SEG
SEG News
SEG Seminar
Internal Site
Hot Link
Contact SEG



  间:201392418: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.