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

共 50 条

[21] Constraint Programming for Dynamic Symbolic Execution of Java']JavaScript
Amadini, Roberto
Andrlon, Mak
Gange, Graeme
Schachte, Peter
Sondergaard, Harald
Stuckey, Peter J.
INTEGRATION OF CONSTRAINT PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND OPERATIONS RESEARCH, CPAIOR 2019, 2019, 11494 : 1 - 19
[22] KROVER: A Symbolic Execution Engine for Dynamic Kernel Analysis
Pitigalaarachchi, Pansilu
Ding, Xuhua
Qiu, Haiqing
Tu, Haoxin
Hong, Jiaqi
Jiang, Lingxiao
PROCEEDINGS OF THE 2023 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY, CCS 2023, 2023, : 2009 - 2023
[23] Using Metamorphic Testing to Improve Dynamic Symbolic Execution
Alatawi, Eman
Miller, Tim
Sondergaard, Harald
2015 24TH AUSTRALASIAN SOFTWARE ENGINEERING CONFERENCE (ASWEC 2015), 2015, : 38 - 47
[24] Dynamic symbolic execution approach based on tabu search
Cai, Jun
Zou, Peng
Ma, Jinxin
He, Jun
Beijing Hangkong Hangtian Daxue Xuebao/Journal of Beijing University of Aeronautics and Astronautics, 2015, 41 (12): : 2348 - 2355
[25] TracerX: Dynamic Symbolic Execution with Interpolation (Competition Contribution)
Jaffar, Joxan
Maghareh, Rasool
Godboley, Sangharatna
Xuan-Linh Ha
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2020), 2020, 12076 : 530 - 534
[26] Leveraging Abstract Interpretation for Efficient Dynamic Symbolic Execution
Alatawi, Eman
Sondergaard, Harald
Miller, Tim
PROCEEDINGS OF THE 2017 32ND IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE'17), 2017, : 619 - 624
[27] Model Checking MSVL Programs Based on Dynamic Symbolic Execution
Duan, Zhenhua
Bu, Kangkang
Tian, Cong
Zhang, Nan
COMPUTING AND COMBINATORICS, 2015, 9198 : 521 - 533
[28] Design and implementation of a dynamic symbolic execution tool for windows executables
Chen, Ting
Zhang, Xiao-song
Zhu, Cong
Ji, Xiao-li
Guo, Shi-ze
Wu, Yue
JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS, 2013, 25 (12) : 1249 - 1272
[29] Fitness-Guided Path Exploration in Dynamic Symbolic Execution
Xie, Tao
Tillmann, Nikolai
de Halleux, Jonathan
Schulte, Wolfram
2009 IEEE/IFIP INTERNATIONAL CONFERENCE ON DEPENDABLE SYSTEMS & NETWORKS (DSN 2009), 2009, : 359 - +
[30] DyTa: Dynamic Symbolic Execution Guided with Static Verification Results
Ge, Xi
Taneja, Kunal
Xie, Tao
Tillmann, Nikolai
2011 33RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE), 2011, : 992 - 994

← 1 2 3 4 5 →