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
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II | 2022年 / 13244卷
关键词：
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 条
  • [21] A secure Java']Java™ Virtual Machine
    van Doom, L
    USENIX ASSOCIATION PROCEEDINGS OF THE NINTH USENIX SECURITY SYMPOSIUM, 2000, : 19 - 34
  • [22] Platform independent dynamic Java']Java virtual machine analysis: the Java']Java Grande Forum benchmark suite
    Gregg, D
    Power, J
    Waldron, J
    CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE, 2003, 15 (3-5): : 459 - 484
  • [23] A Java']Java/CORBA virtual machine architecture for remote execution of optimization solvers in heterogeneous networks
    González-Castaño, FJ
    Anido-Rifón, L
    Pousada-Carballo, JM
    Rodríguez-Hernández, PS
    López-Gómez, R
    SOFTWARE-PRACTICE & EXPERIENCE, 2001, 31 (01): : 1 - 16
  • [24] Formalizing the safety of Java']Java, the Java']Java virtual machine, and Java']Java card
    Hartel, PH
    Moreau, L
    ACM COMPUTING SURVEYS, 2001, 33 (04) : 517 - 558
  • [25] Probabilistic Programming for Java']Java using Symbolic Execution and Model Counting
    Visser, Willem
    Pasareanu, Corina S.
    SOUTH AFRICAN INSTITUTE OF COMPUTER SCIENTISTS AND INFORMATION TECHNOLOGISTS (SACSIT 2017), 2017, : 319 - 328
  • [26] Dynamic monitor allocation in the Java virtual machine
    Dombrowski, Marcel
    Kent, Kenneth B.
    Dawson, Michael
    Gracie, Charlie
    Herpers, Rainer
    ACM International Conference Proceeding Series, 2013, : 30 - 37
  • [27] Verification of Java']Java programs using symbolic execution and invariant generation
    Pasareanu, CS
    Visser, W
    MODEL CHECKING SOFTWARE, 2004, 2989 : 164 - 181
  • [28] JPF-SE: A symbolic execution extension to Java']Java PathFinder
    Anand, Saswat
    Pasareanu, Corina S.
    Visser, Willem
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2007, 4424 : 134 - +
  • [29] Runtime Exception Detection in Java']Java Programs Using Symbolic Execution
    Kadar, Istvan
    Hegedus, Peter
    Ferene, Rudolf
    ACTA CYBERNETICA, 2014, 21 (03): : 331 - 352
  • [30] Sound Regular Expression Semantics for Dynamic Symbolic Execution of Java']JavaScript
    Loring, Blake
    Mitchell, Duncan
    Kinder, Johannes
    PROCEEDINGS OF THE 40TH ACM SIGPLAN CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '19), 2019, : 425 - 438
12345