Hello, I just enjoyed the OSDI 2008 paper about KLEE. I hope this list is a good place to ask questions about it!
Footnote 9 caught my attention because it suggests that the way KLEE lays out its state representations in memory affects the results of the run. But if I write code like assert((int)(malloc(1)) % 3); then shouldn't KLEE deterministically generate a test case that is triggered by unfortunate behavior of malloc in the C runtime? Or is the goal of KLEE only to find bugs that can be reliably triggered? A broader question is about how KLEE explores its search space of states. It seems that states only fork (on branches), never rejoin. Might it be profitable to identify states that are equivalent and merge them (so the search space is a DAG rather than tree)? Or is it pretty clear that the cost of merging states outweighs the benefits? Thanks for any comments! (I am not subscribed to the list - please let me know if I should be.)
