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
关键词
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
相关论文
共 50 条
  • [41] Testing multithreaded programs with contextual unfoldings and dynamic symbolic execution
    Kahkonen, Kari
    Heljanko, Keijo
    Proceedings - International Conference on Application of Concurrency to System Design, ACSD, 2014, 2015-January (January): : 142 - 151
  • [42] Symbolic Types for Lenient Symbolic Execution
    Chang, Stephen
    Knauth, Alex
    Torlak, Emina
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
  • [43] Neuro-Symbolic Execution: Augmenting Symbolic Execution with Neural Constraints
    Shiqi, Shen
    Shinde, Shweta
    Ramesh, Soundarya
    Roychoudhury, Abhik
    Saxena, Prateek
    26TH ANNUAL NETWORK AND DISTRIBUTED SYSTEM SECURITY SYMPOSIUM (NDSS 2019), 2019,
  • [44] Quantum symbolic execution
    Nan, Jiang
    Zichen, Wang
    Jian, Wang
    QUANTUM INFORMATION PROCESSING, 2023, 22 (10)
  • [45] Relational Symbolic Execution
    Farina, Gian Pietro
    Chong, Stephen
    Gaboardi, Marco
    PROCEEDINGS OF THE 21ST INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2019), 2019,
  • [46] Symbolic Execution with CEGAR
    Beyer, Dirk
    Lemberger, Thomas
    LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I, 2016, 9952 : 195 - 211
  • [47] Certified Symbolic Execution
    Qiu, Rui
    Pasareanu, Corina S.
    Khurshid, Sarfraz
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2016, 2016, 9938 : 495 - 511
  • [48] Chopped Symbolic Execution
    Trabish, David
    Mattavelli, Andrea
    Rinetzky, Noam
    Cadar, Cristian
    PROCEEDINGS 2018 IEEE/ACM 40TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2018, : 350 - 360
  • [49] Quantum symbolic execution
    Jiang Nan
    Wang Zichen
    Wang Jian
    Quantum Information Processing, 22
  • [50] Directed Symbolic Execution
    Kin-Keung Ma
    Khoo Yit Phang
    Foster, Jeffrey S.
    Hicks, Michael
    STATIC ANALYSIS, 2011, 6887 : 95 - 111