The LIME testbench is a collection of tools that allows concolic testing of Java programs. Concolic testing is also known as dynamic symbolic execution. It attempts to visit every possible execution path of the program under test.
Note: The software is only known to work on 64-bit Ubuntu Linux.
boolector-1.4-ffc2089-100608.tar.gz
from http://fmv.jku.at/boolector/ and picosat-936.tar.gz
from http://fmv.jku.at/picosat/, and place them into the subdirectory dependencies/solvers
.make
in the subdirectory dependencies/solvers
.bin
subdirectory to your PATH.JAVA_HOME
environment variable. Define an environment variable JRELIBPATH
that points to the directory that holds the Java libraries, namely jce.jar
, jsse.jar
and rt.jar
.examples
subdirectory. For example, you can run a concolic testing example in the examples/lct
subdirectory with the following commands:
LCTserver
(start this in a separate terminal)LCTcompile BitvectorTest1.java
LCTinstrument BitvectorTest1
cd output
LCTrun BitvectorTest1 all
There is a user manual available for the tools. The manual and some more documentation is available under the doc
directory of the distribution.
For more information, see the LIME2 project web page: http://www.tcs.hut.fi/Research/Logic/LIME2/.