KLEE Options

Search Heuristics

Main search heuristics

KLEE provides four main search heuristics:

1. Depth-First Search (DFS): Traverses states in depth-first order.
2. Random State Search:Randomly selects a state to explore.
3. Random Path Selection: Described in our KLEE OSDI'08 paper.
4. Non Uniform Random Search (NURS): Selects a state randomly according to a given distribution. The distribution can be based on the minimum distance to an uncovered instruction (MD2U), the query cost, etc.

To select a search heuristic, use the --search option provided by KLEE. For example:

    $ klee --search=dfs demo.o

runs demo.o using DFS, while

    $ klee --search=random-path demo.o 

runs it using the random path selection strategy. The full list of options is shown in KLEE's help message:

    $ klee --help
    -search                                 - Specify the search heuristic (default=random-path interleaved with nurs:covnew)
      =dfs                                  -   use Depth First Search (DFS)
      =random-state                         -   randomly select a state to explore
      =random-path                          -   use Random Path Selection (see OSDI'08 paper)
      =nurs:covnew                          -   use Non Uniform Random Search (NURS) with Coverage-New heuristic
      =nurs:md2u                            -   use NURS with Min-Dist-to-Uncovered heuristic
      =nurs:depth                           -   use NURS with 2^depth heuristic
      =nurs:icnt                            -   use NURS with Instr-Count heuristic
      =nurs:cpicnt                          -   use NURS with CallPath-Instr-Count heuristic
      =nurs:qc                              -   use NURS with Query-Cost heuristic   

Interleaving search heuristics

Search heuristics in KLEE can be interleaved in a round-robin fashion. To interleave several search heuristics to be interleaved, use the --search multiple times. For example:

    $ klee --search=random-state --search=nurs:md2u demo.o 

interleaves the Random State and the NURS:MD2U heuristics in a round robin fashion.

Default search heuristics

The default heuristics used by KLEE are random-path interleaved with nurs:covnew.