期刊文献+

精确的程序静态分析 被引量:36

Sharp Static Analysis of Programs
下载PDF
导出
摘要 程序的静态分析是程序语言和编译领域的一个重要研究方向,已经被研究了很多年.近年来,它也引起形式方法和软件工程领域的重视,被用于程序测试和正确性验证.文中从程序的语法特征、所关心的数据类型和程序性质等方面比较了一些静态分析技术.着重描述基于路径的分析方法,特别是符号执行技术,讨论了程序路径可行性分析问题及其分类、复杂度.针对程序分析精度的一种量化指标,说明了其计算方法. Static program analysis has been studied for many years. It is an important topic in the research of programming languages and compilers. Recently, it has also attracted researchers from other areas such as formal methods and software engineering, and some ideas have been used for program verification and testing. This paper compares various static analysis techniques, according to the syntactic features, data types and correctness properties targeted by the techniques. The paper focuses on a class of analysis techniques that are based on program paths, especially symbolic execution; discusses the path feasibility problem, its difficulty and its subproblems. A method for computing a data coverage measure of paths is also described.
作者 张健
出处 《计算机学报》 EI CSCD 北大核心 2008年第9期1549-1553,共5页 Chinese Journal of Computers
基金 the National Natural Science Foundation of China (NSFC) under grant No.60673044 and No.60633010 the National High-Tech Program (863) under grant No.2006AA01Z402
关键词 静态分析 程序路径 符号执行 数据覆盖 static analysis program paths symbolic execution data coverage
  • 相关文献

参考文献17

  • 1Hoare C A R. The verifying compiler: A grand challenge for computing research. Journal of the ACM, 2003, 50(1): 63-69
  • 2Horwitz S. Precise flow-insensitive may-alias analysis is NP- hard. ACM Transactions on Programming Languages and Systems, 1997, 19(1): 1-6
  • 3Ball T, Rajamani S K. The SLAM project: Debugging system software via static analysis//Proeeedings of the 29th ACM Symposium on Principles of Programming Languages (POPL 2002). Portland, OR, USA, 2002:1-3
  • 4Lev-Ami T et al. Putting static analysis to work for verification: A case study//Proceedings of the International Symposium on Software Testing and Analysis (ISSTA 2000). Portland, OR, USA, 2000:26-38
  • 5Zhang J, Wang X. A constraint solver and its application to path feasibility analysis. International Journal of Software Engineering and Knowledge Engineering, 2001, 11(2): 139- 156
  • 6Zhang J. Symbolic execution of program paths involving pointer and structure variables//Proceedings of the QSIC. Braunschweig, Germany, 2004:87-92
  • 7King J C. Symbolic execution and testing. Communications of the ACM, 1976, 19(7): 385-394
  • 8Yates D F, Malevris N. Reducing the effects of infeasible paths in branch testing. ACM SIGSOFT Software Engineering Notes, 1989, 14(8): 48-54
  • 9Ngo M N, Tan H B K. Heuristics-based infeasible path detection for dynamic test data generation. Information & Software Technology, 2008, 50(7-8): 641-655
  • 10Zhang J et al. Path-oriented test data generation using symbolic execution and constraint solving techniques//Proeceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004). Beijing, China,2004: 242-250

二级参考文献31

  • 1Kylin project.2007.http://www.kylin.org.cn
  • 2Linux kernel mailing list archive.2007.http://www.uwsg.indiana.edu/hypermail/linux/kernel/
  • 3Corbet J,Kroah-Hartman G,Rubini A.Linux Device Drivers.3rd ed.,O'Reilly,2005.
  • 4Love R.Linux Kernel Development.2nd ed.,Sams Publishing,2005.
  • 5Bovet DP,Cesati M.Understanding the Linux Kernel.3rd ed.,O'Reilly,2005.
  • 6Russell R.Unreliable guide to locking.2003.Http://www.kernel.org/pub/linux/kernel/people/rusty/kernel-locking/index.html
  • 7The Linux kernel API.2005.http://kernelbook.sourceforge.net/kernel-api.html/
  • 8Chou A,Yang J,Chelf B,Hallem S,Engler DR.An empirical study of operating systems errors.In:Proc.of the 18th ACM Symp.Operating Systems Principles.ACM Press,2001.73-88.
  • 9Beyer D,Henzinger TA,Jhala R,Majumdar R.Checking memory safety with blast.In:Proc.of the FASE 2005.LNCS 3442,Springer-Verlag,2005.2-18.
  • 10Musuvathi M,Engler DR.Model checking large network protocol implementations.In:Proc.of the 1st Symp.on Networked Systems Design and Implementation.San Francisco:USENIX,2004.

共引文献4

同被引文献342

引证文献36

二级引证文献233

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部