[klee-dev] Use Klee with Java?

[Sean Bartell]

Zhenyu Zhou on 2015-06-20:
>I'm looking for a tool for symbolic execution and find that Klee is a
>fantastic tool. But now I'm wondering whether Klee can analyse JAVA codes
>(or class files)? I have searched in the mail list and found the same
>question is posted several years ago. Does anyone know are there any
>progresses in this direction?

KLEE only understands LLVM bitcode--this is part of the fundamental design of 
KLEE. If you need to use KLEE on Java code, you might be able to use RoboVM[0] 
or VMKit[1] (unmaintained) to convert Java into LLVM bitcode. However, this 
will require a lot of work to get usable bitcode, especially when you have to 
deal with Java libraries and OS interaction.

It will be much easier to use a Java-specific tool instead of KLEE, such as 
JPF-symbc[2].

[0] http://docs.robovm.com/
[1] http://vmkit.llvm.org/
[2] http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc