State Merging

[Daniel Liew]

Hi Patrick,

I'm not aware of any changes but I only have knowledge of the bits of
KLEE I actually work on and state merging is not one of them.

You may want to take a look at [1] which I believe implements
something more sophisticated than what mainline KLEE does. I believe
they implemented their work in their own fork of KLEE. It would be
nice if this work was merged into mainline KLEE but I believe EPFL's
version of KLEE has diverged significantly from mainline KLEE and
would require major effort to port many of their contributions to
mainline KLEE.

[1] Efficient State Merging in Symbolic Execution. Volodymyr
Kuznetsov, Johannes Kinder, Stefan Bucur, and George Candea.
Conference on Programming Language Design and Implementation (PLDI),
Beijing, China, June 2012

Thanks,
Dan.

Hello all,
I am writing to learn about the current support for state merging in KLEE. I
found this thread (State merging) from ~4 years ago, but I was wondering if
there had been any changes in the interim.
The -use-merge flag indicates that klee_merge() support is experimental. Has
klee_merge() been tested to work for special cases?
Very respectfully,
Patrick Copeland