PV3 ⊧ KLEEchecks properties by symbolic execution

Application domain/field

• Symbolic execution
• Dynamic symbolic execution
• Bug finding
• Test generation

Type of tool

Symbolic execution engine

Expected input

• Program
• Optionally KLEE and/or program options, e.g. whether to check for integer overflows.

Format:

• Program: LLVM bitcode file (.bc)
• Optional: options passed as arguments when calling KLEE

Expected output

KLEE generates some statistics (e.g. how many generated tests, running time, number of explored paths, etc.), warnings emitted by KLEE, and other messages emitted by KLEE. The output can be found in the terminal or in a text file. Moreover, it also generates a human readable version of the bitcode executed by KLEE, a SQLite file with statistics and an istats file with statistics.

Internals

Symbolic execution can be used for several purposes including test generation, bug finding,