+ +

KLEE Open Projects

+ + + This page lists a variety of open projects that are natural (and tractable) + extensions of KLEE and things that we would love to see people work on. If + you are interested in tackling any of the projects, please mail + klee-dev + with your ideas -- or even better, your patches!. + +

+ Implement SMT support for Kleaver: + +
We would like to make Kleaver (KLEE's constraint solver) a more viable + standalone product. One of the steps in this direction is to implement SMT + support. This would also allow us to enter Kleaver into + the SMT-COMP theorem prover + competition, which would be a good proving ground for our optimizations + and benchmarking our underlying constraint solver (STP, currently) against + other implementations.
+
+ Distributed Constraint Solving: + +
Much of the execution time of KLEE is spent inside the constraint + solver. A natural extension would be to implement support for a + distributed constraint solver, which would run KLEE on a single machine, + but would farm out the constraints to be solved on a network of + machines.
+
+ Improve User Interface: + +
This is not a very glamorous project, but it is still + important. Currently, KLEE has a myriad of command line options and flags, + most of which are left over from its research project roots. In order to + promote KLEE's use as a user tool, we would like to clean up most of the + UI so that the default behavior matches best practice, and so that more + arcane or research-only options are hidden by default.
+
+ Experiment With Other Constraint Solvers: + +
For the most part, KLEE has been written so that it is possible to swap + in other constraint solvers, but we have never tried anything other than + STP. We would love to see the results of using other contraint solvers + (like Yices or Z3) with KLEE.
+
+ Implement Expression Level Constraint Optimization: + +
KLEE does not currently do much optimization of constraint expressions + before sending them to the constraint solver. We would like to have an + internal framework for doing optimization of constraint expressions (e.g., + (A & ~A) => 0) so that these optimizations are only done once instead of + on every solver query.
+ +
In general, because KLEE is dealing with expressions which result from + dynamic execution traces, many expressions end up having constant + components. This means we can frequently apply the same optimizations a + compiler would do, but to much greater effect because we are more likely + to see constant values. For reference, see the kinds of optimizations done + by LLVM's InstCombine + pass here.
+ +
The bulk of this project involves defining a good framework for us to + apply optimizations to expressions, and for deciding when to attempt to + optimization expressions.
+