Hi, I am a graduate student studying KLEE.
We found that the time overhead of KLEE is too much for our target program(13585 LOC). There are three kinds of time overhead in KLEE. First, generating test case overhead. When we applied the --max-time option, after halting execution, generating test cases for remained states takes too much time. Second, for each search strategy, with --max-time option, total execution time has too much gap, e.g. when --max-time=1800, in DFS case, total execution time is 3795 sec, and in random path case, 8720 sec. Finally, counter example cache. Using a counter example cache reduces # of redundant queries, but it can take too much time for the target program having long size of symbolic input array. The solving time is exponentially increasing as the size of symbolic input array are longer. Why are these time-consuming? Is there any idea about reducing the time ? Thank you. - YJK
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
