An Empirical Study of Path Feasibility Queries
1 Theory for symbolic execution is QF_ABV (Why? Research needed.) He said is better than . 2 He have tried , , . 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 . 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.
Sergey Vartanov, 2007–2020