- -

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.
-