JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution)

10Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

JDart performs dynamic symbolic execution of Java programs: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A portfolio of constraint solvers is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. For SV-COMP 2021, we improved JDart by implementing exploration strategies, bounded analysis, and path-specific constraint solving strategies, as well as by enabling the use of SMT-Lib string theory for encoding of string operations.

Cite

CITATION STYLE

APA

Mues, M., & Howar, F. (2021). JDart: Portfolio Solving, Breadth-First Search and SMT-Lib Strings (Competition Contribution). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12652 LNCS, pp. 448–452). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-72013-1_30

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free