The LIME testbench

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.

Releases

• LimeTB-1.1.0.tar.gz (used in SPIN 2010 Workshop paper)
• LimeTB-2.2.0.tar.gz
• LIME Concolic Tester for C has its own page

Note: The software is only known to work on 64-bit Ubuntu Linux.

Benchmarks

• DPOR benchmarks (Benchmarks for evaluating dynamic partial-order reduction)

Quickstart

• Download one of the releases above and unpack the contents.
• Download 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.
• Run make in the subdirectory dependencies/solvers.
• Add the bin subdirectory to your PATH.
• Define the 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.
• There are example code snipplets in the 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

Documentation

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

---

Latest update: 26 January 2012.