Crucible support as a Symbolic Engine

Open rafaelsamenezes opened this issue 5 years ago • 1 comments

Is your feature request related to a problem? Please describe. Currently, we only have support for KLEE as a symbolic engine, the issue is that it contains a limitation for floating numbers. Crucible supports enconding for floats, has support for SV-COMP notation and it's API contains all that is needed for a Generator.

Describe the solution you'd like Implement a NonDetGeneratorCrucible and compare it with KLEE specially for floats.

May 29 '20 10:05 rafaelsamenezes

Thanks for your help @rafaelsamenezes . Could you point me some paper or DOCs for Crucible?

Jun 04 '20 22:06 hbgit