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

2021 ◽  
pp. 448-452
Author(s):  
Malte Mues ◽  
Falk Howar
Keyword(s):  
String Theory ◽  
Symbolic Execution ◽  
Constraint Solving ◽  
Breadth First Search ◽  
Dynamic Symbolic Execution ◽  
Symbolic Constraints

AbstractJDartperforms dynamic symbolic execution ofJavaprograms: 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 improvedJDartby 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.

scholarly journals JDart: Dynamic Symbolic Execution for Java Bytecode (Competition Contribution)

2020 ◽  
pp. 398-402 ◽  
Author(s):  
Malte Mues ◽  
Falk Howar
Keyword(s):  
Symbolic Execution ◽  
Model Checker ◽  
Constraint Solver ◽  
Java Bytecode ◽  
Software Model ◽  
Dynamic Symbolic Execution ◽  
Symbolic Constraints

Abstract JDart performs dynamic symbolic execution of Java programs: it executes programs with concrete inputs while recording symbolic constraints on executed program paths. A constraint solver is then used for generating new concrete values from recorded constraints that drive execution along previously unexplored paths. JDart is built on top of the Java PathFinder software model checker and uses the JConstraints library for the integration of constraint solvers.

scholarly journals Enhancing Dynamic Symbolic Execution by Automatically Learning Search Heuristics

2021 ◽  
pp. 1-1
Author(s):  
Sooyoung Cha ◽  
Seongjoon Hong ◽  
Jiseong Bak ◽  
Jingyoung Kim ◽  
Junhee Lee ◽  
...  
Keyword(s):  
Symbolic Execution ◽  
Search Heuristics ◽  
Dynamic Symbolic Execution

SMT Solvers in Application to Static and Dynamic Symbolic Execution: A Case Study

2019 ◽  
Author(s):  
Nikita Malyshev ◽  
Irina Dudina ◽  
Daniil Kutz ◽  
Alexander Novikov ◽  
Sergey Vartanov
Keyword(s):  
Symbolic Execution ◽  
Smt Solvers ◽  
Dynamic Symbolic Execution

Generating Test Suites with Augmented Dynamic Symbolic Execution

2013 ◽  
pp. 152-167 ◽  
Author(s):  
Konrad Jamrozik ◽  
Gordon Fraser ◽  
Nikolai Tillman ◽  
Jonathan de Halleux
Keyword(s):  
Symbolic Execution ◽  
Dynamic Symbolic Execution ◽  
Test Suites
Sign in / Sign up

Export Citation Format

Share Document