DyTa: Dynamic Symbolic Execution Guided With Static Verification Results

Software-defect detection is an increasingly important research topic in software engineering. To detect defects in a program, static verification and dynamic test generation are two important proposed techniques. However, both of these techniques face their respective issues. Static verification produces false positives, and on the other hand, dynamic test generation is often time consuming. To address the limitations of static verification and dynamic test generation, the authors present an automated defect-detection tool, called DyTa, that combines both static verification and dynamic test generation.