[klee-dev] KLEE strategies in solving complex contraints

[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

On 19/11/13 01:37, Sandeep wrote:
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>