master branch


Try KLEE for Yourself

  1. First tutorial: Testing a small function.
  2. Second tutorial: Testing a simple regular expression library.
  3. Using symbolic environment: Guide with examples on how to use the symbolic environment such as symbolic files and command-line arguments for the program under test.
  4. Testing Coreutils: In-depth description of how to use KLEE to test GNU Coreutils.

We also recommend the following external resources. When using them, please take into account that they might be using old versions of KLEE.

  1. Symbolic execution with KLEE: A set of four instructional videos introducing KLEE, starting with how to get started with KLEE and ending with a demo that finds memory corruption bugs in real code.
  2. Solving a maze with KLEE: A nice explanation of how symbolic execution can be used to generate interesting program inputs. The example shows how to use KLEE to find all the solutions to a maze game.
  3. Keygenning with KLEE and Hex-Rays: A beginners explanation of using symbolic execution to solve a small binary’s pseudocode.
  4. Keygenning with KLEE: A more in-depth guide to using KLEE for key generation.
  5. How to generate tests automatically?: A basic introduction to symbolic execution with KLEE.
  6. Using KLEE to generate tests for binary search: A tutorial on using KLEE to test a binary search implementation).
  7. A Guide to KLEE LLVM Execution Engine Internals: A quick overview of KLEE’s internals and core classes in PoC||GTFO 0x18 (pp. 51).
  8. Testing Rust programs with KLEE: A collection of tools/libraries to support testing of Rust programs with KLEE.
  9. SAT/SMT by example: A comprehensive guide focusing on using SAT and SMT solvers, which includes lots of interesting examples involving KLEE.
  10. Measuring the coverage achieved by symbolic execution: A blog post that discusses the difference between the internal coverage reported by KLEE and the external coverage reported by a tool such as GCov.
  11. Binary symbolic execution with KLEE-Native: An extension of KLEE that analyses binaries by lifting them to LLVM IR