Deconstructing Dynamic Symbolic Execution

被引：18
作者：
Ball, Thomas [1 ]
Daniel, Jakub [2 ]
机构：
[1] Microsoft Res, Redmond, WA 98052 USA
[2] Charles Univ Prague, Prague, Czech Republic
来源：
DEPENDABLE SOFTWARE SYSTEMS ENGINEERING | 2015年 / 40卷
关键词：
Symbolic Execution; Automatic Test Generation; White-box Testing; Automated Theorem Provers;
D O I：
10.3233/978-1-61499-495-4-26
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Dynamic symbolic execution (DSE) is a well-known technique for automatically generating tests to achieve higher levels of coverage in a program. Two keys ideas of DSE are to: (1) seed symbolic execution by executing a program on an initial input; (2) use concrete values from the program execution in place of symbolic expressions whenever symbolic reasoning is hard or not desired. We describe DSE for a simple core language and then present a minimalist implementation of DSE for Python (in Python) that follows this basic recipe. The code is available at https://www.github.com/thomasjball/PyExZ3/(tagged "v1.0") and has been designed to make it easy to experiment with and extend.
引用
收藏
页码：26 / 41
页数：16
相关论文
共 14 条
  • [1] [Anonymous], 2006, P 13 ACM C COMP COMM
  • [2] Cadar C, 2005, LECT NOTES COMPUT SC, V3639, P2
  • [3] Symbolic Execution for Software Testing: Three Decades Later
    Cadar, Cristian
    Sen, Koushik
    [J]. COMMUNICATIONS OF THE ACM, 2013, 56 (02) : 82 - 90
  • [4] Clarke L. A., 1976, IEEE Transactions on Software Engineering, VSE-2, P215, DOI 10.1109/TSE.1976.233817
  • [5] Z3: An efficient SMT solver
    de Moura, Leonardo
    Bjorner, Nikolaj
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 : 337 - 340
  • [6] Dijkstra Edsger W, 1976, A discipline of programming, V613924118
  • [7] DART: Directed automated random testing
    Godefroid, P
    Klarlund, N
    Sen, K
    [J]. ACM SIGPLAN NOTICES, 2005, 40 (06) : 213 - 223
  • [8] SAGE: Whitebox Fuzzing for Security Testing
    Godefroid, Patrice
    Levin, Michael Y.
    Molinar, David
    [J]. COMMUNICATIONS OF THE ACM, 2012, 55 (03) : 40 - 44
  • [9] Godefroid P, 2011, PLDI 11: PROCEEDINGS OF THE 2011 ACM CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION, P258
  • [10] Generating test data for branch coverage
    Gupta, N
    Mathur, AP
    Soffa, ML
    [J]. FIFTEENTH IEEE INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING, PROCEEDINGS, 2000, : 219 - 227
12