The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more

被引：7
|
作者：
Hentschel, Martin [1 ]
Bubel, Richard [1 ]
Haehnle, Reiner [1 ]
机构：
[1] Tech Univ Darmstadt, Darmstadt, Germany
来源：
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER | 2019年 / 21卷 / 05期
关键词：
Symbolic execution; Program understanding; Deductive program verification; Debugging; Slicing; PROGRAM; GENERATION;
D O I：
10.1007/s10009-018-0490-9
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The Symbolic Execution Debugger (SED), is an extension of the debug platform for interactive debuggers based on symbolic execution. The SED comes with a static symbolic execution engine for sequential programs, but any third-party symbolic execution engine can be integrated into the SED. An interactive debugger based on symbolic execution allows one like a traditional debugger to locate defects in the source code. The difference is that all feasible execution paths are explored at once, and thus there is no need to know input values resulting in an execution that exhibits the failure. In addition, such a debugger can be used in code reviews and to guide and present results of an analysis based on symbolic execution such as, in our case, correctness proofs. Experimental evaluations proved that the SED increases the effectiveness of code reviews and proof understanding tasks.
引用
收藏
页码：485 / 513
页数：29
相关论文
共 50 条
  • [1] The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging, verification and more
    Martin Hentschel
    Richard Bubel
    Reiner Hähnle
    [J]. International Journal on Software Tools for Technology Transfer, 2019, 21 : 485 - 513
  • [2] Symbolic Execution Debugger (SED)
    Hentschel, Martin
    Bubel, Richard
    Haehnle, Reiner
    [J]. RUNTIME VERIFICATION, RV 2014, 2014, 8734 : 255 - 262
  • [3] Interactive verification of concurrent systems using symbolic execution
    Baeumler, Simon
    Balser, Michael
    Nafz, Florian
    Reif, Wolfgang
    Schellhorn, Gerhard
    [J]. AI COMMUNICATIONS, 2010, 23 (2-3) : 285 - 307
  • [4] Sound Gradual Verification with Symbolic Execution
    Zimmerman, Conrad
    Divincenzo, Jenna
    Aldrich, Jonathan
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2024, 8 (POPL):
  • [5] VERIFICATION OF PROTOCOLS USING SYMBOLIC EXECUTION
    BRAND, D
    JOYNER, WH
    [J]. COMPUTER NETWORKS AND ISDN SYSTEMS, 1978, 2 (4-5): : 351 - 360
  • [6] EXECUTION REPLAY - A MECHANISM FOR INTEGRATING A VISUALIZATION TOOL WITH A SYMBOLIC DEBUGGER
    LEU, E
    SCHIPER, A
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 634 : 55 - 66
  • [7] No Panic! Verification of Rust Programs by Symbolic Execution
    Lindner, Marcus
    Aparicius, Jorge
    Lindgren, Per
    [J]. 2018 IEEE 16TH INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2018, : 108 - 114
  • [8] FORMAL PROGRAM VERIFICATION USING SYMBOLIC EXECUTION
    DANNENBERG, RB
    ERNST, GW
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1982, 8 (01) : 43 - 52
  • [9] Achieve Fuzzing Based on Symbolic Execution Platform
    He Hao
    Gan Shuitao
    [J]. PROCEEDINGS OF THE 2015 JOINT INTERNATIONAL MECHANICAL, ELECTRONIC AND INFORMATION TECHNOLOGY CONFERENCE (JIMET 2015), 2015, 10 : 991 - 993
  • [10] Symbolic Types for Lenient Symbolic Execution
    Chang, Stephen
    Knauth, Alex
    Torlak, Emina
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2018, 2
12345