\section{Technique}
Unlike the original \textsc{klee} which execute one single program at a time,
our tool performs execution on a pool of the program's revisions
at the same time.

An overview of our approach is illustrated in figure~\ref{fig:arch}.

\begin{figure}[h]\centering
  \begin{tikzpicture}[mymatrix/.style={matrix of nodes,
                                       nodes=typetag,row sep=1ex},
                      typetag/.style={draw,anchor=west},
                      title/.style={draw=none,inner sep=0pt},
                      line width=0.2ex]
    \linespread{0.8}
    \node[draw,label={[name=sched]Scheduler}] (states) {States};
    \node[draw,below=0.5ex of states] (clstr) {Clusters};
    \node[draw,fit={(sched) (states) (clstr)}] {};

    \node[draw,right=11em of states] (symb) {Interpreter};
    \draw[-angle 45] (states.north east) to[in=90,out=15]
      node[sloped,above,pos=0.4]{selected state} (symb.north west);
    \draw[-angle 45] (symb.south west) to[in=0,out=-90]
      node[sloped,above,pos=0.6]{child state} (states.east);

    \node[draw,below=6em of symb] (smt) {Theorem prover};
    \draw[angle 45-angle 45] (symb) to (smt);

    \node[draw,below=7em of sched,label={[name=diff]Differentiator}]
      (outs) {Fruitful states};
    \draw[-angle 45] (symb.south west) to[in=45,out=-90]
      node[sloped,above,pos=0.6]{state with output} (outs.15);
    \draw[-angle 90] (outs) to[in=90,out=0,pos=0.4]
      node[sloped,below]{path conditions} (smt.north west);
    \draw (outs.south east) to[in=90,out=10] (smt.north west);

    \node[draw,below=0.5ex of outs] (prog) {Metaprogram};
    \node[draw,fit={(diff) (outs) (prog)}] {};
    \draw[-angle 45] (smt.south west) to[out=-90,in=0]
      node[sloped,below]{concrete input} (prog);
    \draw[-angle 45] (prog) to[out=180,in=-150]
      node[left,align=center]{diff.\\test} (clstr.south west);

    \node[left=4em of states.west] (bc) {bitcode};
    \draw[-angle 90] (bc) to[in=180,out=60] (states.west);
    \node[below=1em of bc,align=center] (tree) {decision\\tree};
    \draw[-angle 45] (clstr.west) to[out=180,in=60] (tree);
    \node[above=1em of bc,align=center] (seed) {seed\\input};
    \draw[dotted] (seed) to[out=0,in=180] (states);
    \draw[-angle 45] (bc.south west)
      to[out=-135,in=-135] (prog.south west);
  \end{tikzpicture}
  \caption{\textsc{Psychic} overview.}\label{fig:arch}
\end{figure}

\begin{algorithm}
\caption{Overall execution}
\begin{algorithmic}[1]
  \Require set of program revisions $D$
  \Ensure set of differential tests $T$
  \State $T \gets \varnothing$
  \State $E \gets \varnothing$  \Comment{Exited states}
  \State $q \gets \text{new\_searcher}(D)$
  \For{$d \in D$}
    \State $s \gets \text{initial\_state}(d)$
    \State $\text{add\_states}(q, \{s\})$
  \EndFor
  \While{has\_state($q$)}
    \State $s \gets \text{select\_state}(q)$
    \State $i \gets \text{next\_instruction}(s)$
      \Comment{$i$ is a state}
    \If{$i$ is exit}
      \State $E' \gets \text{head}(\text{sort}(\text{distance\_to}(i),
        \text{different\_revision}(E, i)))$
      \For{$e \in E'$}
        \State $t \gets \text{generate\_test}(i, e)$
        \If{$t$ is not null}
          \State $T \gets T \cup \{t\}$
        \EndIf
      \EndFor
      \State $E \gets E \cup \{i\}$
    \Else
      \State $S_+, S_- \gets \text{execute\_instruction}(i)$
      \State $\text{remove\_states}\left(q, S_-\right)$
      \State $\text{add\_states}\left(q, S_+\right)$
    \EndIf
  \EndWhile
\end{algorithmic}
\end{algorithm}

\begin{algorithm}
\caption{State selection}
\begin{algorithmic}[1]
  \Require searcher $q$
  \Ensure state $s$
  \State $S \gets \varnothing$
  \State $P \gets \text{base\_priority}(q)$
    \Comment{Scheduling priority from base search algorithm}
  \For{$z \in \text{states}(q)$}
    \If{$z \notin S$}
      \State $S' \gets \text{parallel\_states}(q, z)$
      \If{$S' \ne \varnothing$}
        \State $S \gets S \cup S' \cup \{z\}$
      \EndIf
    \EndIf

    \State $l \gets \text{local\_frontier}(q, z)$
    \State $g \gets \text{global\_frontier}(q, z)$
    \If{$l$ is null $\land$ $g$ is not null}
      \State $P_z \gets P_z + \text{distance\_bonus}(g, z)$
      \Comment{Should further or nearer be prioritised?}
    \EndIf
  \EndFor
  \For{$z \in S$}
    \State $P_z \gets P_z + \text{PARALLEL\_BONUS}$
  \EndFor
  \State $s \gets \text{max\_priority}(P)$
\end{algorithmic}
\end{algorithm}