It's taken a little while to get organized, but KLEE is finally open source! Check out the KLEE website for more information; now available at http://klee.llvm.org
We've been hard at work the past month trying to make KLEE more approachable -- cleaning up the code base, starting on user-level documentation, etc. There is still a lot of work to be done to migrate KLEE from its research beginnings (particularly documentation), but I think we've made a good start. We'd love your help! Several notes on our status: - Currently the supported platforms are Linux and OS X on 32-bit Intel x86. I've had some confirmation that KLEE works on FreeBSD, and we hope to add full 64-bit x86 support in the near term. The POSIX runtime currently only works on Linux with uClibc. - For now, the KLEE trunk will track LLVM top-of-tree. Once LLVM 2.6 is released I will consider maintaining 2.6 compatibility for users who want to track KLEE, but not upgrade LLVM. - Due to moving to a newer LLVM, KLEE currently cannot execute a lot of optimized code (some optimization passes now create arbitrary sized integer types). This problem is tracked by: http://llvm.org/PR4295 I recommend compiling input programs at -O0 (and not using the --optimize option) until this bug is fixed. - We aren't yet providing our customized uCibc library, needed for using the POSIX runtime to automatically make parts of the environment symbolic. This should be available soon. I'd appreciate feedback if you try it out, and don't hesitate to send questions to me or this list. Bugs can be filed at http://llvm.org/bugs in the "klee" component. Enjoy! - Daniel
