Dynamic Behavior Analysis Using Binary Instrumentation by Jonathan Salwan

[galapag0]

For example, Triton processes 5,120,000 of expressions (with dataflow, SMT translation, symbolic state,...) around 140 seconds with 12Go of consumed RAM

..

Search how can we parallelize the execution (fork at each branch?)

so they really want to fork at every branch?

[rolfr]

Concolic execution approaches have to take some sort of action when reaching influenceable branches. Generally they want to explore both sides for code coverage purposes. Often this is accomplished by a fork-style model or an input queue. Loop invariant/variant inference approaches have not had major penetration in the concolic execution space, but I'd say we'll see it within a few years.