GDart: An Ensemble of Tools for Dynamic Symbolic Execution on the Java']Java Virtual Machine (Competition Contribution)

被引:6
|
作者
Mues, Malte [1 ]
Howar, Falk [1 ,2 ]
机构
[1] TU Dortmund Univ, Dortmund, Germany
[2] Fraunhofer ISST, Dortmund, Germany
关键词
Dynamic Symbolic Execution; Software Verification;
D O I
10.1007/978-3-030-99527-0_27
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
GDART is an ensemble of tools allowing dynamic symbolic execution of JVM programs. The dynamic symbolic execution engine is decomposed into three different components: a symbolic decision engine (DSE), a concolic executor (SPouT), and a SMT solver backend allowing meta-strategy solving of SMT problems (JConstraints). The symbolic decision component is loosely coupled with the executor by a newly introduced communication protocol. At SV-COMP 2022, GDART solved 471 of 586 tasks finding more correct false results (302) than correct true results (169). It scored fourth place.
引用
收藏
页码:435 / 439
页数:5
相关论文
共 50 条
  • [1] JDART: Dynamic Symbolic Execution for Java']Java Bytecode (Competition Contribution)
    Mues, Malte
    Howar, Falk
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 398 - 402
  • [2] SWAT: Modular Dynamic Symbolic Execution for Java']Java Applications using Dynamic Instrumentation (Competition Contribution)
    Loose, Nils
    Maechtle, Felix
    Sieck, Florian
    Eisenbarth, Thomas
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, TACAS 2024, 2024, 14572 : 399 - 405
  • [3] SWAT: Modular Dynamic Symbolic Execution for Java Applications using Dynamic Instrumentation (Competition Contribution)
    Loose, Nils
    Mächtle, Felix
    Sieck, Florian
    Eisenbarth, Thomas
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2024, 14572 LNCS : 399 - 405
  • [4] Dynamic Symbolic Execution of Java']Java Programs Using JNI
    Vartanov, Sergey
    2017 ELEVENTH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGIES (CSIT), 2017, : 83 - 86
  • [5] Java']Java Virtual Machine Educational Tools
    Dobravec, Tomasz
    2019 IEEE 15TH INTERNATIONAL SCIENTIFIC CONFERENCE ON INFORMATICS (INFORMATICS 2019), 2019, : 383 - 387
  • [6] Dynamic Symbolic Execution for the Analysis of Web Server Applications in Java']Java
    Balasubramanian, Daniel
    Zhang, Zhenkai
    McDermet, Dan
    Karsai, Gabor
    SAC '19: PROCEEDINGS OF THE 34TH ACM/SIGAPP SYMPOSIUM ON APPLIED COMPUTING, 2019, : 2178 - 2185
  • [7] A symbolic Java']Java virtual machine for test case generation
    Müller, RA
    Lembeck, C
    Kuchen, H
    Proceedings of the IASTED International Conference on Software Engineering, 2004, : 365 - 371
  • [8] Dynamic class loading in the Java']Java™ virtual machine
    Liang, S
    Bracha, G
    ACM SIGPLAN NOTICES, 1998, 33 (10) : 36 - 44
  • [9] 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
  • [10] Symbolic Execution for Java']JavaScript
    Santos, Jose Fragoso
    Maksimovic, Petar
    Grohens, Theotime
    Dolby, Julian
    Gardner, Philippa
    PPDP'18: PROCEEDINGS OF THE 20TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2018,