KLEE strategies in solving complex contraints

[Sandeep]

Hello All,
I am aware of the query optimizations strategies that KLEE follows to
simplify the expressions before they each STP.
But what if even after applying these, the query is still complex. Will
KLEE simply give up by time out or it will try something like
concertizing some of the values of the complex constraint to make that
simpler (and thereby give up on exploring some of the paths).

Thanks in advance.

[Cristian Cadar]

KLEE doesn't do any concretization is this case. My experience with
this suggests that the main challenge is to choose a general strategy
for the bytes to concretize and the number/kind of iterations to
perform. While I can't seem to find the code in question, adding
another Solver pass of this type is relatively easy. KLEE already
concretizes values in various cases (calls to external functions,
floating-point code), so all the needed basic blocks are there.

Best,
Cristian

Post by Sandeep
Hello All,
I am aware of the query optimizations strategies that KLEE follows to
simplify the expressions before they each STP.
But what if even after applying these, the query is still complex. Will
KLEE simply give up by time out or it will try something like
concertizing some of the values of the complex constraint to make that
simpler (and thereby give up on exploring some of the paths).
Thanks in advance.
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev