Open
Description
Concolic Execution is a mixed symbolic / concrete fuzzing approach where we would leverage the path conditions generated from a symbolic execution along a single (randomly selected) branch in the execution tree to synthesize an input that will visit a new branch.
We could add a concolic execution engine and combine it with the explore test type to allow very high coverage testing against contracts that are not amenable to exhaustive symbolic exeuction (e.g. highly non linear, dynamic data).
If the solver is unable to synthesize a value that satisfies the given path conditions, we can fallback to fuzzing until we find a value that would explore the new branch.
Metadata
Assignees
Labels
No labels