KLEE verifier

KLEE verifier
[Google Scholar] [Website]

Notes: LLVM compiler, symbolic execution
Papers: cadar:cacm:2013, cadar:osdi:2008

KLEE is a symbolic virtual machine built on top of the LLVM compiler. KLEE uses symbolic execution to generate tests by constructing the “path conditions” associated with paths through the program and, for each path, using a constraint solver to solve those conditions to generate inputs that would cause the program to follow that path.


Fuzz testing, S2E verifier, Symbolic execution, Software Testing Competition (Test-Comp), Verification performance of code, Verification profiling of code, Verifier performance