PV3 KLEEchecks properties by symbolic execution

Application domain/field

Type of tool

Symbolic execution engine

Expected input


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.


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


Related papers

Last publication date

2 June 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.