diff options
Diffstat (limited to 'www/klee-options.html')
| -rw-r--r-- | www/klee-options.html | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/www/klee-options.html b/www/klee-options.html new file mode 100644 index 00000000..22871e0e --- /dev/null +++ b/www/klee-options.html @@ -0,0 +1,73 @@ +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" + "http://www.w3.org/TR/html4/strict.dtd"> +<!-- Material used from: HTML 4.01 specs: http://www.w3.org/TR/html401/ --> +<html> +<head> + <META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1"> + <title>The KLEE Symbolic Virtual Machine</title> + <link type="text/css" rel="stylesheet" href="menu.css"> + <link type="text/css" rel="stylesheet" href="content.css"> +</head> +<body> +<!--#include virtual="menu.html.incl"--> +<div id="content"> + <!--*********************************************************************--> + <h1>KLEE Options</h1> + <!--*********************************************************************--> + + <h2>Search Heuristics</h2> + + <h3>Main search heuristics</h3> + + <p> + KLEE provides four main search heuristics: + <ol> + <li><b>Depth-First Search (DFS):</b> Traverses states in depth-first order.</li> + <li><b>Random State Search:</b>Randomly selects a state to explore.</li> + <li><b>Random Path Selection:</b> Described in our <a href="http://www.doc.ic.ac.uk/~cristic/papers/klee-osdi-08.pdf">KLEE OSDI'08</a> paper.</li> + <li><b>Non Uniform Random Search (NURS):</b> 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. + </ol> + + To select a search heuristic, use the <b>--search</b> option provided by KLEE. For example: + <pre class="output"> + $ klee --search=dfs demo.o</pre> + + runs <i>demo.o</i> using DFS, while + <pre class="output"> + $ klee --search=random-path demo.o </pre> + runs it using the random path selection strategy. + + The full list of options is shown in KLEE's help message: + <pre class="output"> + $ 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 </pre> + + + <h3>Interleaving search heuristics</h3> + <p> + Search heuristics in KLEE can be interleaved in a round-robin + fashion. To interleave several search heuristics to be interleaved, use the <b>--search</b> multiple times. For example: + <pre class="output"> + $ klee --search=random-state --search=nurs:md2u demo.o </pre> + interleaves the Random State and the NURS:MD2U heuristics in a round robin fashion. + <br/> + </p> + + + <h3>Default search heuristics</h3> + <p> + The default heuristics used by KLEE are <i>random-path</i> interleaved with <i>nurs:covnew</i>. + </p> + +</div> +</body> +</html> |