solving

1 Theory for symbolic execution is QF_ABV (Why? Research needed.) He said STP is better than Z3. 2 He have tried KLEE, Bitblaze, Java PathFinder. All experiment results are from Bitblaze. He tested SQLite and libPNG. They modify Bitblaze to generate mapping between the variables used in formula to the variables used in the assembly code. And they map symbols from assembly to source code using Binutils. 3 They extract formulae of different size from formula of executed path (all them from the start of the program).

5 They use number a ratio branches (control flow) to memory writes (data flow) as path characteristics. For libPNG and SQLite this ratio is different (1.7 and 0.9) but doesn't change for different formula sizes.

So, you can predict time for path solving? Think about.

10 pages

Sergey Vartanov, 2007–2020