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

Malte Mues, Falk Howar

2022Lecture notes in computer science17 citationsDOI Open Access PDF

Abstract

Abstract 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.

Topics & Concepts

ExecutorComputer scienceSymbolic executionConcolic testingProgramming languageJavaThe SymbolicComponent (thermodynamics)SolverOperating systemSoftwareThermodynamicsPolitical sciencePsychologyPhysicsPsychoanalysisLawFormal Methods in VerificationSoftware Testing and Debugging TechniquesSoftware Reliability and Analysis Research