Fuzzing Symbolic Expressions\\ % for Concolic Execution \thanks{This paper is supported in part by European Union's Horizon 2020 research and innovation programme (grant agreement No. 830892, project SPARTA).
\IEEEauthorblockN{Luca Borzacchiello
%Finding bugs in software is of paramount importance for its reliability. Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, \fuzzysat, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid fuzzers. %by concolic and hybrid fuzzing engines.
solve_one.tex
% !TEX root = ../paper.tex

\begin{figure}[t]
\vspace{-2mm}
\removelatexerror
%\setlength{\textfloatsep}{0mm}
\begin{algorithm}[H]
 \footnotesize
 \DontPrintSemicolon
 \SetAlgoNoEnd
 \SetAlgoNoLine
 \SetNlSkip{-0.5em}
 \SetKwFunction{FMain}{\sc Solve}
 \SetKwProg{Fn}{function}{:}{}
 \Fn{\FMain{e, $\pi$, i, opt}}{   
 %\KwData{this text}
 %\KwResult{how to write algorithm with \LaTeX2e }
 \tikzmk{A} 
 \nextnr M $\gets$ {\sc Analyze}($\pi$, M)\;
 \nextnr M $\gets$ {\sc Analyze}(e, M)\; 
 \tikzmk{B}
 \boxit{gray1}
 \tikzmk{A} 
 \nextnr a, SA $\gets$ {\sc Mutate}(e, $\pi$, i, M)\;
 \nextnr \lIf{{\upshape a} {\upshape is not} {\upshape NULL}}{\Return{a}}
 \tikzmk{B}
 \boxit{gray2}
 \tikzmk{A} 
 \nextnr a $\gets$ {\sc PickBestAssignment}($\pi$, SA)\;
 \nextnr \If{{\upshape a} {\upshape is not} {\upshape NULL}}{\Indmm
            \nextnr M$'$ $\gets$ {\sc FixInputBytes}(a, M)\;
            \nextnr CC $\gets$ {\sc GetConflictingExpressions}(e, $\pi$, M$'$)\;
            \nextnr \For{{\upshape e$'$}$\,\in\,\,${\upshape CC}}{\Indmm\Indmm
              \nextnr a$'$, SA $\gets$ {\sc Mutate}(e$'$, $\pi$, i, M$'$)\;
              \nextnr \lIf{{\upshape a$'$} {\upshape is not} {\upshape NULL}}{\Return{\upshape a$'$}}
              \nextnr a$'$ $\gets$ {\sc PickBestAssignment}($\pi$, SA)\;
              \nextnr \lIf{{\upshape a$'$} {\upshape is} {\upshape NULL}}{{\bf break}}
              \nextnr a $\gets$ a$'$\;
              \nextnr M$'$ $\gets$ {\sc FixInputBytes}(a, M$'$)\;
            }
         }
 \tikzmk{B}
 \boxit{gray2}
 \tikzmk{A}\nextnr \If{{\upshape opt}}{\Indmm
 \nextnr \lIf{{\upshape a} {\upshape is} {\upshape NULL}}{ a $\gets$ {\sc MutateOpt}(e, $\pi$, i, M)}
 \nextnr {\Return{\upshape a}}\;
 }
 \tikzmk{B}
 \boxit{gray2}
 \nextnr {\Return{\upshape NULL}}\
 %\tikzmk{A}    
 %\tikzmk{B}
 %\boxit{blue}
}
\vspace{2pt}
\caption{{\sc Solve} implementation of \fuzzysat: analysis stage in light gray, reasoning stage in dark gray (initial mutations due to $e$ at lines 3-4, multi-goal strategy at lines 5-15, and optimistic solving at lines 16-18).\label{alg:solve-one}}
\end{algorithm}
\setlength{\textfloatsep}{\textfloatsepsave}
%\vspace{-2mm}
\end{figure}
approach-analysis.tex
% !TEX root = paper.tex
\subsection{Analyzing symbolic expressions}
\label{ss:analysis}

We now present the details of the main analyses integrated into the {\sc Analyze} function, which incrementally build the knowledge of \fuzzysat\ over an expression $e$.

\medskip\noindent
{\bf Detecting inputs and input groups.}
The first analysis identifies which input bytes $i_k$ are involved in an expression and evaluates how these bytes are grouped. In particular, \fuzzysat\ checks whether the expression can be regarded as an {\em input group}, i.e., the expression is equivalent to a concatenation ($\mdoubleplus$) of input bytes or constants that never {\em mix} their bits. Single byte expressions are also detected as input groups. 
%\rem{it is a 1-byte input group $\rightarrow$ why 1-byte? Is $i_0$ always a single byte?}
\boxedspit{
\noindent{\bf\small Examples:}
\begin{itemize}
    \item expression $i_1 \mdoubleplus i_0$ contains inputs $i_0$ and $i_1$, and it is an input group since the bits from these bytes do not mix with each other but are just appended;
    \item expression $0 \mdoubleplus i_0$ contains input $i_0$ and it is a 1-byte input group as it is a zero-extend operation on $i_0$;
    \item expression $i_1 + i_0$ contains inputs $i_0$ and $i_1$, but it is not an input group as bits from $i_0$ are mixed, i.e., added, with bits from $i_1$;
%    \item expression $5 + i_0$ contains inputs $i_0$, but it is not an input group as bits from $i_0$ are mixed, i.e., added, with bits from constant $5$;
    \item expression $(0 \mdoubleplus i_0) + (i_1 \ll 8)$ contains inputs $i_0$ and $i_1$, and it is an input group as the expression is equivalent to $i_1 \mdoubleplus i_0$, which is an input group.
\end{itemize}
}
Given an expression $e$, \fuzzysat\ stores in the expression metadata M the list of inputs involved in $e$, whether $e$ is an input group, and the list of input groups {\em contained} in $e$ when recursively considering subexpressions of $e$.

\medskip\noindent
{\bf Detecting uniquely defined inputs.} A crucial information about an input byte is knowing whether its value is fixed to a single value, dubbed {\em uniquely defined} in our terminology, due to one equality constraint that involves it. Indeed, it is not productive to fuzz input bytes whose value is fixed to a single constant. Given an expression $e$, then:
\begin{itemize}
    \item if $e$ is an equality constraint and one of its operands is an input group, or contains exactly only one input group, while the other operand is a constant, then M is updated to reflect that the bytes in the group will be uniquely defined due to $e$ if $e$ is later added to $\pi$;
    \item an input in $e$ is marked as uniquely defined whenever a constraint from $\pi$ marks it as uniquely defined;
    \item the input group in $e$ (if any) is marked as uniquely defined whenever the inputs forming it are all uniquely defined due to constraints in $\pi$;
\end{itemize}
\boxedspit{
\noindent{\bf\small Example.} The expression $i_1 \mdoubleplus i_0 == \mathrm{0xABCD}$ makes \fuzzysat\ mark inputs $i_0$ and $i_1$ as uniquely defined. If this expression is later added to $\pi$, then $i_0$ and $i_1$ will be considered uniquely defined in other expressions, disabling fuzzing on their values. 
%will not be fuzzed as their values must be kept equal to the ones from the input test case $i$.
}

\medskip\noindent
{\bf Detecting input-to-state branch conditions.} This analysis checks whether $e$ contains at least one operand that has input-to-state correspondence (\cref{se:related}). In \fuzzysat\, we use the following conditions to detect this kind of branch conditions: (a) $e$ matches the pattern $e'~op_{cmp}~e''$, where $op_{cmp}$ is a comparison operator (e.g., $\ge$, $==$, etc.) and (b) one operand ($e'$ or $e''$) is an input group. %(i.e., which by definition has input-to-state correspondence). 
When $e$ is a Boolean negation, \fuzzysat\  recursively analyzes the subexpression. %If $op_{cmp}$ is $==$ then the input group is expected to be uniquely defined.
%\vspace{-4mm}
\boxedspit{
\noindent{\bf\small Example.} The expression $\mathrm{10} \ge i_1 \mdoubleplus i_0$ is an input-to-state branch condition as $\ge$ is a comparison operator and $i_1 \mdoubleplus i_0$ is an input group.
}

\medskip\noindent
{\bf Detecting interesting constants.} \fuzzysat\ checks the expression $e$, looking for constants that could be valuable during the reasoning stage, dynamically building a dictionary to use during the transformations. When specific patterns are detected, \fuzzysat\ generates variants of the constants based on the semantics of the computation performed by $e$.%\rem{collects the constants $\mathrm{0xF0}$, $\mathrm{0xF0}$ $\rightarrow$ $\mathrm{0x0F}$?}
\boxedspit{
\noindent{\bf\small Example.} When analyzing $i_1\,\oplus\,\mathrm{0xF0} == \mathrm{0x0F}$, \fuzzysat\ collects the constants $\mathrm{0xF0}$, $\mathrm{0x0F}$, and $\mathrm{0xFF}$ (i.e., $\mathrm{0xF0} \oplus \mathrm{0x0F}$) since the computation is an exclusive or. %bitwise
}
The patterns used to generate interesting constants can be seen as a relaxation of the concept of input-to-state relations.

\medskip\noindent
{\bf Detecting range constraints.} \fuzzysat\ checks whether $e$ is a {\em range constraint}, i.e., a constraint that sets a lower bound or an upper bound on the values that are admissible for the input group in $e$ (if any). For instance, \fuzzysat\ looks for constraints matching the pattern $e'~op_{cmp}~e''$ where $e'$ is an input group, $op_{cmp}$ is a comparison operator, and $e''$ is a constant value. Other equivalent patterns, such as $(e'~-~e'')~op_{cmp}~e'''$ where $e'$ is an input group while $e''$ and $e'''$ are constants, are detected as range constraints as well. 

By considering bounds resulting from expressions in $\pi$ and not only from $e$, \fuzzysat\ can compute refined range intervals for the input groups contained in an expression. To compactly and efficiently maintain these intervals, \fuzzysat\ uses {\em wrapped intervals}~\cite{wrapped-intervals} which can transparently deal with both signed and unsigned comparison operators.
\boxedspit{
\noindent{\bf\small Examples.} 
\begin{itemize}
    \item given the expressions $i_1 \mdoubleplus i_0 > \mathrm{10}$ and $i_1 \mdoubleplus i_0 \le 30$, \fuzzysat\ computes the range interval $[11, 30]$ for the input group composed by $i_0$ and $i_1$;
    \item given the expression $(i_1 \mdoubleplus i_0) + \mathrm{0xAAAA} <_{unsigned} \mathrm{0xBBBB}$, \fuzzysat\ computes the intervals $[0, \mathrm{0x1110}] \cup [\mathrm{0x5556}, \mathrm{0xFFFF}]$ for $i_0$ and $i_1$, correctly 
    modeling the wrap-around that may result in the two's complement representation.
\end{itemize}
}

\medskip\noindent
{\bf Detecting conflicting expressions.} The last analysis is devised to identify which expressions from $\pi$ may {\em conflict} with $e$ when assigning some of its input bytes. In particular, \fuzzysat\ marks an expression $e'$ as in conflict with $e$ whenever the set of input bytes in $e'$ is not disjoint with the set from $e$.
\boxedspit{
\noindent{\bf\small Example.} 
The expression $i_1 + i_0 > 10$ is in conflict with the expression $i_1 + i_2 < 20$ as they both contain the input byte $i_1$. Hence, fuzzing the first expression may negatively affect the second expression.%When fuzzing $i_1$ in the first expression, \fuzzysat\ knows that the second expression may be affected, i.e., made unsatisfied.
% altering the value of $i_0$ and $i_1$ may affect the satisfiability of the second expression, possibly requiring to perform mutations also on $i_2$.

%both expressions and \fuzzysat\ may try to mutate $i_2$ when looking for an assignment.
%When mutating $i_0$ and $i_1$, \fuzzysat\ needs to understand that 
%this may make the second expression (contained, e.g., in $\pi$) unsatisfiable and thus it may have to mutate even input byte $i_2$.
}
Computing the set of conflicting expressions is essential for performing the multi-goal strategy during the reasoning stage. % (\cref{ss:overview}).
approach-reasoning.tex
% !TEX root = paper.tex
\subsection{Fuzzing symbolic expressions}
\label{ss:reasoning}

The core step during the reasoning stage of \fuzzysat\ is the execution of the function {\sc Mutate}, which attempts to find a valid assignment $a$. %that makes both $e$ and $\pi$ satisfied when executed in the context of {\sc SolveOne}\rem{in the context of SolveOne ?}. 
To reach this goal, {\sc Mutate} performs a sequence of mutations over the input test case $i$, returning as soon as a valid assignment is found by one of these transformations. When a mutation generates an assignment that satisfied $e$ but not $\pi$, then {\sc Mutate} saves it into a set of candidate assignment $SA$, which could be valuable later on during the multi-goal strategy (\cref{ss:overview}). In some cases, a transformation can determine that there exists a contradiction between $e$ and the conditions in $\pi$, leading {\sc Mutate} to an early termination. Additionally, when {\sc Mutate} builds a candidate assignment $a$, it checks that $a$ is consistent with the range intervals known for the modified bytes, discarding $a$ in case of failure and avoiding the (possibly expensive) check over $\pi$. We now review in detail the input transformations performed by the function {\sc Mutate}. 

\medskip\noindent
{\bf Fuzzing input-to-state relations.} When an expression $e$ is an input-to-state branch condition (\cref{ss:analysis}), \fuzzysat\ tries to replace the value from one operand $e'$ into the bytes composing the input group from the other (input-to-state) operand $e''$. If $e'$ is not constant, then \fuzzysat\ gets its concrete value by evaluating $e'$ on the test case $i$. When $e'$ is constant and the relation is an equality, if the assignment does not satisfy $\pi$, then \fuzzysat\ deems the query unsatisfiable. %On the other hand
Conversely, when the comparison operator is not an equality, \fuzzysat\ tests variants of the value from $e'$, e.g., by adding or subtracting one to it, in the same spirit as done by \redqueen.
\vspace{-4mm}
\boxedspit{
\noindent{\bf\small Example.} Given $i_1 \mdoubleplus i_0 == \mathrm{0xABCD}$, \fuzzysat\ builds the assignment $\{i_0 \gets \mathrm{0xCD}, i_1 \gets \mathrm{0xAB}\}$. If the range interval over $i_0$ is $[\mathrm{0xDD}, \mathrm{0xFF}]$ due to constraints from $\pi$, then the assignment can be discarded without testing $\pi$, deeming the query unsatisfiable (but keeping the assignment in SA in case of optimistic solving).%\vspace{-3mm}
}
\vspace{-1mm}

\medskip\noindent
{\bf Range interval brute force.} When a range interval is known for an input group contained an expression $e$, \fuzzysat\ can use this information to perform brute force on its value and possibly find a valid assignment. In particular, when an expression contains a single input group and its range interval is less than 2048, \fuzzysat\ builds assignments that brute force all the possible values assignable to the group. If no valid assignment is found, then the query can be deemed unsatisfiable. If the interval is larger than 2048, then \fuzzysat\ only tests the minimum and maximum value of the interval. To make this input transformation less conservative, \fuzzysat\ runs it even when $e$ contains at least one input group whose interval is less than\footnote{We pick the input group with the minimum range interval. %We use a smaller threshold in this scenario as the chances of success are lower because different input groups are contained in $e$ but only one is considered.
} 512. 
\boxedspit{
\noindent{\bf\small Example.} Given the expression $(i_1 \mdoubleplus i_0) * \mathrm{0xABCD} == \mathrm{0xCAFE}$ and the range interval $[1, 9]$ (built due to constraints from $\pi$) on the group $g$ with $i_0$ and $i_1$, then \fuzzysat\ builds assignments for $g \in [1, 9]$, deeming the query unsatisfiable if none of them satisfies $e \wedge \pi$.%\vspace{-3mm}
}

\medskip\noindent
{\bf Trying interesting constants.} For each constant $c$ collected by {\sc Analyze} when considering the expression $e$ and for each input group $g$ contained in $e$, \fuzzysat\ tries to set the bytes from $g$ to the value $c$. Since constants are collected through {\em relaxed} patterns, \fuzzysat\ tests different encodings (e.g., little-endian, big-endian, zero-extension, etc.) for each constant to maximize the chances of finding a valid assignment.
\boxedspit{
\noindent{\bf\small Example.} Given the expression $(i_1 \mdoubleplus i_0) * 100 == 200$ and assuming that {\sc Analyze} has collected the constants $\{2, 99, 100, 101, 199,200, 201\}$ where $2$ was obtained as $200/100$, while other constants are obtained from $100$ and $200$, then \fuzzysat\ would find a valid assignment when testing $\{i_0 \gets 2, i_1 \gets 0\}$ ($c = 2$, little-endian encoding).
\vspace{-0.5mm}
}

\medskip\noindent
{\bf Gradient descent.} Given an expression $e$, \fuzzysat\ tries to reduce the problem of finding a valid assignment for it to a minimization (or maximization) problem. This is valuable not only in the context of {\sc SolveMin}, {\sc SolveMax}, or {\sc SolveAll} where this idea seems natural, but also when reasoning over the branch condition $e$ in {\sc Solve}. Indeed, any expression of the form $e'\,op_{cmp}\,e''$, where $op_{cmp}$ is a comparison operator, can be transformed into an expression $f$ amenable to minimization to find a valid assignment~\cite{angora}, e.g.,  $e' < e''$ can be transformed\footnote{For the sake of simplicity, we ignore in our examples the wrap-around.} 
 into $f < 0$ with $f = e' - e''$. 

The search algorithm implemented in \fuzzysat\ is inspired by \angora~\cite{angora} and it is based on gradient descent. Although this iterative approach may fail to find a global minimum for $f$, a local minimum can be often {\em good enough} in the context of concolic execution as we do not always really need the global minimum but just an assignment that satisfies the condition, e.g., given $i_0 < 1$, the assignment $\{i_0 \gets \mathrm{0x0}\}$ satisfies the condition even if the global minimum for $i_0 - 1$ is given by $\{i_0 \gets \mathrm{0x81}\}$. For this reason, \fuzzysat\ in {\sc Solve} can stop the gradient descent as soon an assignment satisfies both $e$ and $\pi$. 
%
When the input groups from $e$ have disjoint bytes, \fuzzysat\ computes the gradient considering groups of bytes, instead of computing it for each distinct byte, as this makes the descent more effective. In fact, reasoning on $i_0$ and $i_1$ as a single value is more appropriate when these bytes are used in a two-byte operation since gradient descent may fail when these bytes are considered independently.

\boxedspit{
\noindent{\bf\small Example.} Given the expression $(i_0 \mdoubleplus i_1) - 10 > (i_2 \mdoubleplus i_3) - 5$ and a zero-filled input test case, then \fuzzysat\ transforms the expression into $((i_2 \mdoubleplus i_3) - 5) - ((i_1 \mdoubleplus i_0) - 10) < 0$, computes the gradients over the input groups $(i_1 \mdoubleplus i_0)$ and $(i_2 \mdoubleplus i_3)$, finding the assignment $\{i_0 \gets \mathrm{0x80}, i_1 \gets \mathrm{0x06}, i_2 \gets \mathrm{0x84}, i_3 \gets \mathrm{0x01}\}$ which %is not a global minimum but 
makes the condition satisfied as $(\mathrm{0x80} \mdoubleplus \mathrm{0x06}) - 10 = 32764 > -31748 = (\mathrm{0x84} \mdoubleplus \mathrm{0x01}) - 5$.
\vspace{-0.5mm}
}
\vspace{-1mm}

\medskip\noindent
{\bf Deterministic and non-deterministic mutations.} These two sets of input transformations are inspired by the two mutation stages from \afl\ (\cref{se:related}). Deterministic mutations include bit or byte flips, replacing bytes with interesting {\em well-known} constants (e.g., {\tt MAX\_INT}), adding or subtracting small constants from some input bytes. Non-deterministic mutations instead involve also transformations such as flipping of random bits inside randomly chosen input bytes, setting randomly chosen input bytes to randomly chosen interesting constants, subtracting or adding random values to randomly chosen bytes, and several others~\cite{AFL}.
%
%
%A crucial different with \afl\ is that \fuzzysat\ restricts mutations only to input bytes involved in $e$ and applies the multi-byte transformations only in the presence of multi-byte input groups.
%
%\medskip\noindent
%{\bf Non-deterministic mutations.} 
%As for the previous set of transformations, the non-deterministic mutations in \fuzzysat\ are inspired by their counterpart in \afl~\cite{AFL} and includes transformations such as flipping of a random bit inside one randomly chosen input byte, setting one randomly chosen input byte to one randomly chosen interesting constant, subtracting or adding a random value to one randomly chosen input byte, and several others~\cite{AFL}. 
%
The main differences with respect to \afl\ are: (a) mutations are applied only on the input bytes involved in the expression $e$, (b) multi-byte mutations are considered only in the presence of multi-byte input groups, (c) for non-deterministic mutations, \fuzzysat\ generates $k$ distinct assignments, with $k$ equal to $\max\{100,n_{i}\cdot 20\}$ where $n_i$ is the number of inputs involved in $e$, and for each assignment it applies a sequence (or stack) of $n$ mutations ($n = 1 \ll (1 + rand(0,7))$ as in \afl).

\iffalse
\subsubsection{Reasoning}

$mutate()$ executes different phases. Each phase attempts to apply one or more transformations on the testcase $i$ based on the information collected on $e$ during the analysis phase. If a transformation satisfies condition $e$, then the phase generates an assignment $a$ and it returns it back to $mutate()$. If a phase does not return any assignment or the assignment generated by a phase does not satisfy $\pi$ as well, $mutate()$ moves on to the next phase (possibly saving the assignment in $SA$). In some cases, a phase can determine that there is a contradiction between $e$ and the conditions in $\pi$, notifying $mutate()$ that the query is unsatisfiable and leading to an early termination without performing the successive phases. $mutate()$ performs the following phases:
\fi

\iffalse
\begin{enumerate}

\item {\bf input-to-state}: if $e$ contains an input-to-state relation~\cite{redqueen} it tries to replace in the input group the constant value. Before determining whether $e$ is satisfiable, it checks whether the transformation of the testcase is consistent with the range intervals known for the modified bytes. For instance, if the relation is $input[0:1] ==$ 0x0000, it speculates the assignments $input[0] ==$ 0x0 and $input[1] ==$ 0x0. If, however, we know that $input[0]$ must be greater than 0x0 due to constraints in $\pi$, then the assignment is discarded and we move on to the next phases. If the input-to-state relation involves an equality, then the query is deemed unsatisfiable. Otherwise (e.g., $>$, $<$), then the constant of the input-to-state relation is modified accordingly, e.g., $input[0] > $ 0x5 leads to the assignment $input[0] ==$ 0x6.

\item {\bf brute force}: it performs brute force on input groups on which \fuzzysat\ has defined a validity interval (different from the default one that has no constraints but the domain, e.g., 2 bytes have 65536 possible values). Akin to the input-to-state transformation, we evaluate whether an assignment contradicts the known intervals on the bytes modified by the transformation. More precisely:

\begin{enumerate}

\item {\em Input group with interval}: if $e$ contains exactly one input group on which a validity interval is defined then: i) if the interval is less than 2048 then we brute force on the possible values assignable to the group, notifying unsatisfiability of the query in case no value leads to satisfy $\pi$; ii) otherwise we try the minimum and the maximum values of the interval.

\item {\em First input group with interval}: like the previous phase but considers the first group of $e$ that has an interval of size less than 1024.

\item {\em Input byte}: if $e$ involves a single byte we brute force on its 256 values. % Brute force on input group as defined above may have failed to consider the input group linked to the byte due to the lack of a validity interval attached to it.

\end{enumerate}

\item {\bf try constants}: for each constant found by $findConstants()$ and for each input group in $e$, tries to replace the constant of the group. Validity intervals are used to discard invalid transformations. We also consider variants of constants (+/-1) and different encodings (little endian, big endian).

\item {\bf gradient descent}: given an expression $e$, it is analyzed as if is were a function $f(x)$ to be minimized. To transform $e$ in $f(x)$ we use a strategy similar to what is done in Angora~\cite{angora}. If the expression $e$ has input groups that involve distinct input bytes, gradient descent can reason on ``input elements'' that have granularity equivalent to input groups, while if input groups have shared bytes, then gradient descent reasons on ``input elements'' with byte granularity. Reason on ``input elements'' with a granularity larger than a single byte makes the minimization process more efficient and effective. For instance, given the expression input[0:1] $<$ 0 it is easier to minimize a 2-byte object made of input[0:1] rather that separately minimizing the two objects input[0] and input[1]. Angora adopts a similar reasoning via a type inference heuristics: the main difference is that we analyze the input groups of the formula, while Angora aggregates in the same element contiguous bytes when read by the same instruction. Once established the granularity for the gradient descent, \fuzzysat\ computes the gradient for the different ``input elements'' and descends considering the ``input elements'' that have non-zero gradient. After a descent, \fuzzysat\ evaluates whether the current transformation satisfies $e\wedge \pi$. If so, it accepts the transformation returning the assignement relative to $mutate()$. Otherwise it performs another descent unless a local minimum has been reached.

\item {\bf deterministic mutations}: transformations inspired by the deterministic mutations of AFL~\cite{AFL}. Compared to AFL, our mutations are performed only on input bytes present in $e$, applying multi-byte transformations only in the presence of multi-byte input groups. Mutations are “walking” bitflips, bitflips, replacing of input groups with interesting “well-known” bit constants, and arithmetic operations~\cite{AFL}. 

\item {\bf non-deterministic mutations:} transformations inspired by non-deterministic mutations (havoc) in AFL~\cite{AFL}. The main differences with AFL are: i) they are applied only on the input bytes involved in the formula; (ii) multi-byte mutations are considered only in the presence of multi-byte input groups: (iii) \fuzzysat\ applies $k$ cascading mutations, with $k$ even and equal to $\max\{100,$ number of input bytes in $e\cdot 100\}$, and after applying a mutation it checks whether the transformation satisfies $e\wedge \pi$. Applied mutations include: flip random bit inside one randomly chosen input byte, set one randomly chosen input byte to one randomly chosen interesting constants, subtract a random value to one one randomly chosen input byte, and many others. If $e$ does not contain an input group with $q$ bytes, mutations that work with input groups with at least $q$ bytes are ignored.

\end{enumerate} 
\fi


\iffalse
\subsubsection{Multi-goal Strategy}

The multi-goal strategy implemented in \fuzzysat\ works as follows. If a solving phase could solve the branch condition but without satisfying $\pi$, it executes the solving phase on the conditions of $\pi$ that involve the same inputs of the branch conditions but are unsatisfied. The algorithm is greedy: it attempts to satisfy one condition at a time, without backtracking.

\subsubsection{Optimistic Solving}

\fuzzysat\ returns the assignment that makes $e$ satisfied for most expressions in $\pi$. It may happen that \fuzzysat\ finds no assignent for $e$ due to constraints arising during the analysis of $\pi$ that make some transformations on $e$ unnecessary. In this case, \fuzzysat\ re-execute the transformations ignoring those constraints.
\fi
approach.tex
% !TEX root = paper.tex
\section{Approach}
\label{se:approach}

% In this section we present the design of \fuzzysat, an approximate solver that can reason over the symbolic expressions generated by a concolic executor using techniques borrowed from the fuzzing domain.


%We know that $\pi$ is satisfied by the current input $i$ that led the engine to follow the path. $\pi$ may grow large and complex along the way, imposing a heavy burden on a classic solver. However, by ``fuzzing'' $\neg b$ on $i$ we may find a new test case $i'$ that satisfies $\neg b$ and is similar enough to $i$ so that $\pi$ remains satisfied by $i'$. Fuzzing is done by performing small mutations to $i$ on the portion that appears in $b$. Hence, we do not need to run any solver on $\pi$, but just check if $\pi$ is satisfied by $i'$. Clearly, this is tailored to scenarios where $i$ is known such as in concolic execution. We use a timeout on fuzzing $\neg b$ to declare unsatisfiability.

%Most concolic executors build symbolic expressions while exploring a program and outsource completely the reasoning over them to a SMT solver, which is treated mainly as a black-box component without any rich feedback from the knowledge that it has acquired over these expressions. In this paper, we explore the idea that a concolic engine can extract valuable knowledge from analyzing the symbolic expressions that it has built. In particular, we focus on how this knowledge can be exploited to solve queries by guiding a reasoning stage that performs simple input transformations,  which have been proved to be effective in the context of software fuzzing techniques. 

Recent coverage-guided fuzzers perform input mutations based of a knowledge on the program behavior that goes beyond the simple code coverage. Concolic executors by design build an accurate description of the program behavior, i.e., symbolic expressions, but outsource completely the reasoning to a powerful but expensive SMT solver, which is typically treated as a black box. In this paper, we explore the idea that a concolic executor can learn from the symbolic expressions that it has built and use the acquired knowledge to apply simple but fast input transformations, possibly solving queries without resorting to an SMT solver. The key insight is that given a query $\neg b \wedge \pi$, the input $i$ that has driven the concolic exploration satisfies by design $\pi$. Hence, we propose to build using input mutations a new test case $i'$ that satisfies $\neg b$ and is similar enough to $i$ so that $\pi$ remains satisfied by $i'$.  In the remainder of this section, we present the design of \fuzzysat, an approximate solver that explores this direction by borrowing ideas from the fuzzing domain to efficiently solve queries generated by concolic execution. %, possibly improving the scalability of concolic execution.


% to make concolic execution more scalable by reducing the solving time while still generate valuable inputs for a program.

%it could be enough in several cases to solve $e \wedge \pi$ by focusing mutations on the input bytes involved in $e$, similarly as fuzzers do when they restrict mutations to a few bytes of an input. Given an input $i'$, the concolic executor can test $e \wedge \pi$ by simply evaluating concretely the query. 


%\subsection{Preliminaries}
\subsection{Reasoning primitives for concolic execution}
\label{ss:primitives}

%Before discussing the main ideas behind \fuzzysat, we discuss which reasoning primitives should be exposed to a concolic executor to allow it to effectively explore the paths of the program under test. Additionally, we define a few notations that will be used in the remainder of the section.

%\smallskip
%{\bf Reasoning primitives for concolic execution.} 

%While SMT solvers typically offer a rich set of reasoning primitives, supporting a wide range of theories as they are designed for solving formulas generated from quite different application contexts, concolic executors such as \qsym\ are instead built on top of a few but essential primitives. In this paper, we focus on these primitives without claiming that \fuzzysat\ can replace a full-fledged SMT solver in a general application context. In particular, \fuzzysat\ exposes the following primitives:

While SMT solvers typically offer a rich set of solving primitives, enabling reasoning on formulas generated from quite different application contexts, concolic executors such as \qsym\ are instead built on top of a few but essential primitives. In this paper, we focus on these primitives without claiming that \fuzzysat\ can replace a full-fledged SMT solver in a general context. \fuzzysat\ exposes the following primitives:

\begin{itemize}

\item {\sc Solve}$(e, \pi, i, opt)$: returns an assignment for the symbolic inputs in $e\wedge\pi$ such that the expression $e\wedge\pi$ is satisfiable. %, where $e$ is a Boolean expression, $\pi$ is a conjunction of Boolean expressions, and $i$ is the input test case that was used by the concolic executor when generating these expressions. 
The flag $opt$ indicates whether optimistic solving should be performed in case of failure. 
%When no assignment is found, {\sc Solve} returns an invalid assignment. 
This primitive is used by concolic engines when negating a branch condition $b$, hence $e=\neg b$.

\item {\sc SolveMax}$(e, \pi, i)$ (resp. {\sc SolveMin}$(e, \pi, i)$): returns an assignment that maximizes (resp. minimizes) $e$ while making $\pi$ satisfiable. Concolic executors use these primitives before concretizing a symbolic memory address $e$ to keep the exploration scalable. These functions are thus used to generate alternative inputs that steer the program to read/write at boundary addresses.

%in the presence of a symbolic memory access, whose address is described by $e$, and the executor concretizes its value to keep the exploration scalable. These functions are thus used to generate inputs that steer the program to read/write at boundary addresses.

%where $e$ is a bitvector expression (and not a Boolean expression as in {\sc Solve}). The function returns an assignment that maximize (resp. minimize) $e$ while making $\pi$ satisfiable. These primitives can be used by a concolic executor in the presence of a symbolic memory access, whose address is described by expression $e$, and the executor opts to concretize its value to keep the exploration scalable. These functions are thus used to generate inputs that steer the program to read/write at boundary addresses.

\item {\sc SolveAll}$(e, \pi, i)$: combines {\sc SolveMin} and {\sc SolveMax}, yielding intermediate assignments identified during the reasoning process as well. This primitive is valuable in the presence of symbolic memory addresses accessing a jump table or when the instruction pointer becomes symbolic during the exploration.

\end{itemize}

Two main aspects differentiate these primitives in \fuzzysat\ with respect to their counterpart from an SMT solver. 

First, \fuzzysat\ is an approximate solver and thus it cannot guarantee that no valid assignment exists in case of failure of {\sc Solve}, i.e., \fuzzysat\ cannot prove that an expression $e\wedge\pi$ is unsatisfiable. Similarly, given an expression $e$, \fuzzysat\ may fail to find its global minimum/maximum value or to enumerate assignments for all its possible values.

Another crucial difference is that \fuzzysat\ requires that the concolic engine provides the input test case $i$ that was used to steer the symbolic exploration of the program under test. This is essential as \fuzzysat\ builds assignments by mutating the test case $i$ based on facts that are learned when analyzing $e$ and $\pi$. Given an assignment $a$ returned by \fuzzysat, a new input test case $i'$ can be built by patching the bytes in $i$ that are assigned by $a$.

%\smallskip
%{\bf Notation and terminologies.}

\subsection{Overview}
\label{ss:overview}

\begin{figure}[t]
\centerline{\includegraphics[height=2.7cm]{figures/structure-4}}\vspace{-2mm}
\caption{Internal architecture of \fuzzysat.\label{fig:structure}}
\end{figure}

% \paragraph{Architecture}
%\medskip\noindent
{\bf Architecture.} To support the primitives presented in Section~\ref{ss:primitives}, the architecture of \fuzzysat\ (Figure~\ref{fig:structure}) has been structured around three main building blocks: the {\em analysis stage}, the {\em expression metadata}, and the {\em reasoning stage}.

The analysis stage (\cref{ss:analysis}) is designed to analyze symbolic expressions, extracting valuable knowledge to use during the reasoning stage. It starts by identifying which input bytes $i_k$ from the input $i$ are involved in an expression and how they are grouped.
%i.e., concatenated (operator $\mdoubleplus$ in our notation), when part of a multi-byte operation, e.g., a 2-byte comparison such as $i_0 \mdoubleplus i_1 == 0x5566$. 
It detects input-to-state relations (\cref{se:related}) and collects constants appearing in the expression for later use in the mutation phase. Expressions that constrain the interval of admissible values for a set of inputs, dubbed {\em range constraints}, such as $i_0 < 10$, are identified to keep track of the {\em range intervals} over the symbolic inputs. Finally, this stage detects whether the current expression shares input bytes with other expressions previously processed by the analysis component, possibly pinpointing {\em conflicts} that may result when mutating these bytes during the reasoning stage.

The expression metadata maintains the knowledge of \fuzzysat\ on the expressions processed by the analysis stage over time. Internally, it is implemented as a set of data structures optimized for fast lookup of different kinds of properties related to an expression (and its subexpressions).
%Internally, it is implemented as a set of data structures that compactly  store the metadata, allowing fast lookup of different kinds of properties related to an expression (and its subexpressions). 
It is updated by the analysis stage and queried by both stages. %Indeed, since an expression $e$ can appear in many other expressions later generated by a concolic engine, it is crucial to cache knowledge to keep the analysis stage scalable, avoiding to repeat any work that was already performed in previous runs.

Finally, the reasoning stage is where \fuzzysat\ exploits the knowledge over the expressions to effectively fuzz the input test case and possibly generate valid assignments. To reach this goal, a mutation engine (\cref{ss:reasoning}) is used to perform a set of transformations over the input bytes involved in an expression $e$ looking for an assignment that satisfies $e$ and $\pi$ ({\sc Solve}) or maximizes/minimizes $e$ while satisfying $\pi$ (other primitives). When this step finds assignments for $e$, but none of them satisfies $\pi$, then \fuzzysat\ performs a multi-goal strategy, which is not limited to changing the input bytes involved in $e$, but attempts to alter other input bytes that are involved in conflicting expressions present in $\pi$. 

\input{algorithms/solve_one}

%\paragraph{Solver}

{\bf Implementing the reasoning primitives.}
Algorithm~\ref{alg:solve-one} shows the interplay of these three components in \fuzzysat\ when considering the primitive {\sc Solve}. Lines 1 and 2 execute the analysis stage by invoking the {\sc Analyze} function on $\pi$ and $e$, respectively. {\sc Analyze} updates the expression metadata M, adding any information that could be valuable during the reasoning stage. Since concolic engines would typically call {\sc Solve} several times during the symbolic exploration, providing each time a $\pi$ that is the conjunction of branch conditions met along the path and which have been already analyzed by \fuzzysat\ in previous runs of {\sc Solve},
%\footnote{A branch condition $b$ is first negated by the concolic engine to generate an input steering the program execution towards the opposite branch, and then added to $\pi$ when negating subsequent branches.}, 
the call at line 1 does not lead \fuzzysat\ to perform any work in most scenarios as the expression metadata M already has a cache containing knowledge about expressions in $\pi$.

Lines 3-18 instead comprise the reasoning stage and can be divided into three main phases. First, the {\sc Mutate} function is called at line 3 to run the mutation engine, restricting the transformations on input bytes that are involved in the expression $e$. When {\sc Mutate} finds an assignment $a$ that satisfies both $e$ and $\pi$, {\sc Solve} returns it at line 4 without any further work. On the other hand, when $a$ is invalid but some assignments SA found by {\sc Mutate} make at least $e$ satisfiable, then {\sc Solve} starts the multi-goal phase (lines 5-15). To this end, \fuzzysat\ uses function {\sc PickBestAssignment} to select the best candidate assignment $a$  from SA% using a heuristic
%\footnote{The current implementation picks the assignment that maximizes the number of expressions from $\pi$ that are satisfied.}
\footnote{We pick an $a$ that maximizes the number of expressions satisfied in $\pi$.}
 and then {\em fixes} the input bytes 
assigned by $a$ using function {\sc FixInputBytes} to prevent further calls of {\sc Mutate} from altering these bytes. It then reruns the mutation engine considering an expression $e'$ which has been marked as in conflict with $e$ during the analysis stage. This process is repeated as long as three conditions hold: (a) $e \wedge \pi$ is not satisfied (line 11), (b) {\sc Mutate} returns at least one assignment in SA for $e'$ (line 13), and (c) there is still a conflicting expression left to consider (condition at line 9). % loop

The multi-goal strategy in \fuzzysat\ employs a greedy approach without ever performing backtrack (e.g., reverting the effects of {\sc FixInputBytes} in case of failure) as it trades accuracy for scalability. Indeed, %although backtracking may help to solve additional queries,
%\fuzzysat\ could potentially solve more queries by backtracking, %or extending the set of conflicting expression at each iteration, 
\fuzzysat\ builds on the intuition that by altering a {\em few} bytes from the input test case $i$%that was used to generate the symbolic expressions $e$ and $\pi$
, it is possible in several cases to generate valid assignments. Additionally, %as shown in the evaluation section, 
since many queries generated by a concolic engine are unsatisfiable, increasing the complexity of this strategy would impose a large burden on \fuzzysat.

The last phase of {\sc Solve} (lines 16-18) has been devised to support optimistic solving in \fuzzysat. When the Boolean $opt$ is true, \fuzzysat\ returns the last candidate assignment found by the mutation engine, which by design satisfies the expression $e$. However, since the previous calls to the mutation engine in {\sc Solve} may have failed to find an assignment $a$ for $e$ due to the constraints resulting from the analysis of expressions from $\pi$, \fuzzysat\ as last resort uses a variant of the function {\sc Mutate}, called {\sc MutateOpt}, that ignores these constraints and exploits only knowledge resulting from $e$ when performing transformations over the input bytes.

The other reasoning primitives ({\sc SolveMin}, {\sc SolveMax}, and {\sc SolveAll}, respectively) follow a workflow similar to {\sc Solve} and we do not present their pseudocode due to lack of space. In the remainder of this section, we focus on the internal details of functions {\sc Analyze} (\cref{ss:analysis}) and {\sc Mutate} (\cref{ss:reasoning}), which are crucial core elements of \fuzzysat.

%%%%%%%%%%%%%%%%%%%%%%
\iffalse
\fuzzysat\ exposes functions similar to those offered by a SMT solver:

\begin{itemize}

\item $Solve(e, \pi, i)$: returns an assignment for the inputs in $e\wedge\pi$ such that the expression $e\wedge\pi$ is satisfiable, where $e$ is a Boolean expression, $\pi$ is a list of Boolean expressions, and $i$ is an input test case. Differently from a SMT solver, if \fuzzysat\ does not find a valid assignment, it cannot prove that $e\wedge\pi$ is unsatisfiable. We use $Solve$ in a concolic engine to negate a certain branch $b$, hence $e=\neg b$.

\item $SolveMax(e, \pi, i)$ (resp. $SolveMin(e, \pi, i)$): where $e$ is a bitvector expression (and not a Boolean expression as in $Solve$). The function returns (if possible) an assignment that maximize (resp. minimize) $e$ making $\pi$ satisfiable. It is not guaranteed that maximum and minimum be global. Functions $SolveMax$ and $SolveMin$ are used by concolic executors in the presence of a symbolic memory access, whose address is described by expression $e$, and that must be concretized. The functions attempt to generate inputs that steer the program to read/write at boundary addresses.

\item $SolveAll(e, \pi, i)$: combines $SolveMin$ and $SolveMax$ by returning different assignments obtained by attempting to minimize/maximize $e$, yielding intermediate assignments identified during the reasoning process as well. There are no guarantees on finding global minima/maxima as well as on the enumeration of all possible assignments.

\end{itemize}

\noindent These functions take as input, in addition to expression $e$, also the test case $i$ that has generated the symbolic expression in a concolic engine. \fuzzysat\ applies transformations (mutations) to $i$ to obtain an assignment that satisfies $e$ and $\pi$, or maximizes/minimizes $e$ while satisfying $\pi$. Each assignment $a$ identified by \fuzzysat\ is returned as a test case $i'$, i.e., $i$ properly modified based on $a$.

Given $e$, $\pi$, and $i$, \fuzzysat\ performs the following phases in the context of a concolic execution to implement $Solve$, $SolveMin$, $SolveMax$ and $SolveAll$:

\begin{enumerate}

\item Analysis: 

\begin{enumerate}

\item expression $e$: identifies groups of the input involved in $e$, identifies constants (e.g., magic numbers), analyzes relations (equalities, inequalities, other comparisons) between groups and constants (e.g., $input[0:3]== 0xABCD$) and between multi-groups and constants (e.g., $input[0:3] + input[4:7] == 0xABCD$, where $input$ denotes a formula input group);

\item expressions in $\pi$: similar to the previous point. If a concolic engine submits branch conditions incrementally based on the order of exploration, this phase can be omitted as $\pi$ contains expressions that have already been analyzed, so it is enough to perform caching.

\end{enumerate}

\item Reasoning: 

\begin{enumerate}

\item perfoms transformations on $i$ to generate one or more assignments that make expression $e$ satisfiable ($Solve$) or minimize/maximize $e$ ($SolveMin$, $SolveMax$ and $SolveAll$). If a candidate satisfies $\pi$ as well, it is returned by \fuzzysat\ to the client;

\item if the previous step finds assignments, but none of them satisfies $\pi$, then \fuzzysat\ performs a multi-goal strategy, which is not limited to changing the input given to $e$, but attempts to alter the input that is linked to $i$ via relations present in $\pi$. For instance, if $e$ involves $input[0:3]$ and $\pi$ contains the expression $input[0:3] + input[4:7] == 0xABCD$ then \fuzzysat, given an assignment that satisfies $e$ for $input[0:3]$, attempts to apply transformations also on $input[4:7]$. The multi-goal approach is greedy: it tries to satisfy one assignment at a time, without backtracking.

\end{enumerate}

\end{enumerate}

\fi
%%%%%%%%%%%%%%%%%%%%%%

\input{approach-analysis}
\input{approach-reasoning}

\subsection{Discussion}

%largely
%While \fuzzysat\ is inspired by previous approaches (\cref{se:related}), it applies them to a novel context along with fresh new ideas. 
Similarly to fuzzers using dynamic taint analysis, %, or any approximation of it, 
\fuzzysat\ restricts mutations over the bytes that affect branch conditions during the program execution. However, it does not only understand {\em which} bytes influence the branch conditions but also reasons on {\em how} they affect them, possibly devising more effective mutations. 

\fuzzysat\ shares traits with \angora, \slf, and \eclipser\ by integrating mutations based on gradient descent, a multi-goal strategy, and range intervals, respectively. Nevertheless, these techniques have been revisited and refined to work over symbolic constraints, which accurately describe the program state and are not available to these fuzzers.

\fuzzysat\ exposes primitives that are needed by concolic executors and that are typically offered by SMT solvers but it implements them in a fundamentally different way inspired by fuzzing techniques, trading accuracy for scalability.
%Nonetheless, the reasoning strategy in \fuzzysat\ is inspired by fuzzing techniques, trading accuracy for scalability, hence giving up on queries with too complex interdependent checks but also aiming at a large throughput that on the long run may produce benefits in the context of concolic execution when additional queries are processed by \fuzzysat\ with respect to the SMT solver.

Finally, \fuzzysat\ shares the same spirit of \jfs\ but takes a rather different approach. While \jfs\ builds a bridge between symbolic execution and fuzzers by turning expressions into a program to fuzz, \fuzzysat\ is designed to merge these two worlds, possibly devising {\em informed} mutations that are driven by
%making fuzzing techniques more effective thanks to 
the knowledge 
%resulting from the analysis of the symbolic expressions. 
acquired by analyzing the expressions.

%As \slf, it integrates a multi-goal strategy to cope with interdependent constraints, but it works by reasoning over symbolic expressions, which are very accurate and are not available to \slf. Similarly to \eclipser, \fuzzysat\ uses range intervals to make the fuzzing process more efficient and effective, but it computes them using accurate


% similar to several state-of-the-art approaches (\cref{se:related}) from which it takes inspiration, it provides a unique and novel combinations of their ideas.

%%%%%%%%%%%%%%%%%%%%%%
\iffalse
Comparison with competitors:
\begin{itemize}
    \item {\em Mutations target input bytes that affect branch condition.} \fuzzysat\ restricts mutations to bytes involved in the symbolic expressions, hence is similar to fuzzers that use taint analysis, or approximations of it (e.g., differential analysis), to identify interesting bytes for a branch conditions. However, when running the multi-goal strategy, \fuzzysat\ does not restrict mutations only to bytes involved in a branch condition, but targets on bytes of expressions that are not satisfied. 
    \item {\em Mutations can exploit knowledge resulting from the analysis of expressions.} Although several input transformations in \fuzzysat\ are inspired by fuzzing techniques, they have been revisited to benefit from the knowledge resulting from the analysis of the symbolic expressions. For instance, most mutations can benefit from the availability of range intervals over the input groups. Additionally, while several fuzzers can detect whether a piece of input influences a branch condition, they do not know which computation has been performed by the program over that data. On the other hand, \fuzzysat\ knows the exact computation and can use this information to perform effective mutations. For instance, non input-to-state relations can be easily rule out without wasting fuzzing attempts, and some mutations can be driven by the semantics of the computation (e.g., variants of constants dynamically generated based on the computation).
    \item {\em Concretely evaluating a query typically takes a short time.} While running a program under a concolic executor is typically way slower than when running the same program under a coverage-guided fuzzer, the symbolic expressions can provide the mean to amortize this cost over thousands of program executions. Indeed, while a fuzzer has to run the the full program for each mutated test case, a concolic executor equipped with \fuzzysat\ requires to only evaluate the symbolic expressions (that {\em compactly} represent the essence of the computation) over an assignment, possibly requiring a time that is smaller than the program running time under a fuzzer. Hence, the initial large cost for building the symbolic expressions can be {\em amortized} over thousands of {\em cheap} evaluations.
    \item {\em \fuzzysat\ is expected to be effective in application contexts where fuzzing is known to be effective.} \fuzzysat\ is not a replacement for a full-fledged SMT solver, as its reasoning cannot cope with expressions generated from an application context different from concolic execution. Indeed, most of the input transformations \fuzzysat\ have been inspired by fuzzing techniques, which quite different from the reasoning from a SMT solver, but has been proved to be effective when testing a large body of real-world applications.
    \item {\em Bringing fuzzing into concolic execution.} \fuzzysat\ shares the same spirit of \jfs\ but takes a different design approach. Indeed, \jfs\ mainly targets floating-point applications (where SMT solvers may struggle to reason on) and uses the symbolic expressions to generate a synthesized program that reflects the original computation, which can then be fuzzed using standard fuzzing tools. On the other hand, \fuzzysat\ targets standard applications and aims at making the fuzzing process more effective by exploiting knowledge extracted when analyzing the symbolic expressions. Hence, \fuzzysat\ attempts to integrate fuzzing techniques into symbolic execution, while \jfs\ only builds a bridge between these two worlds, without transferring knowledge among them. Additionally, \jfs\ is not designed for concolic execution, as it does not solve a query starting from the input test case used for generating the symbolic expressions and it currently works as standalone component, which takes as input the query in the SMTLIB2 format and cannot be seamlessly integrated into a concolic executor without incurring a large overhead\footnote{A query may contain thousands of expressions, making the generation of the SMTLIB file representing the query for a branch quite expensive.}.
\end{itemize}
\fi
%%%%%%%%%%%%%%%%%%%%%%

conclusions.tex
% !TEX root = paper.tex

\edits{
\section{Threats to validity and limitations}

{\bf Floating-point arithmetic.} Our current implementation of \fuzzolic\ and \fuzzysat\ does not handle symbolic expressions involving floating-point operations. In case of floating-point instructions during program execution, \fuzzolic\ concretizes the symbolic expressions. Although this is the same strategy adopted by \qsym, we acknowledge that it may harm the effectiveness of the concolic executor on programs heavily based on floating-point computations.  

\smallskip
{\bf Order of the mutations in \bfseries{{\scshape Fuzzy-Sat}}.} The current implementation of \fuzzysat\ applies mutations using a specific order and stops as soon as one of the mutations is successful in finding a valid assignment for a query. In particular, \fuzzysat\ runs first the {\em cheapest} rules that are more {\em likely} able to succeed: e.g., given an input-to-state relation, trying the input-to-state rule first makes sense as it requires a few attempts and has high chances to succeed~\cite{redqueen}. Hence, results reported in Section~\ref{se:evaluation} are based on the order currently adopted by \fuzzolic. An interesting experiment would be to evaluate how \fuzzysat\ would perform when changing the order of the mutations.

\smallskip
{\bf Impact of \bfseries{{\scshape Fuzzy-Sat}} in hybrid fuzzing}. In Section~\ref{se:evaluation}, we have investigated the impact of \fuzzysat\ inside two concolic executors: \fuzzolic\ and \qsym. Our results are promising and suggest that \fuzzysat\ can be beneficial in the context of hybrid fuzzing. However, we believe it would be interesting to integrate \fuzzysat\ in other frameworks to have additional insights on its effect. For instance, the benefit from using \fuzzysat\ inside a concolic executor that is slow at building symbolic expression would be marginal as most of the analysis time would be spent in the emulation phase and not in the solving one. On the other hand, an efficient concolic executor should benefit from \fuzzysat\ as long as the number of queries submitted to the solver during an experiment is very high: if the number of queries is low, then a slower but more accurate traditional SMT solver would likely perform better than \fuzzysat.

}

\smallskip
\section{Conclusions}

\edits{

\fuzzysat\ is an approximate solver that uses fuzzing techniques to efficiently solve queries generated by concolic execution, helping hybrid fuzzers scale better on several real-world programs. 

We have currently identified two interesting future directions. First, we plan to integrate \fuzzysat\ in the concolic execution framework \symcc, which has been shown to be very efficient at building symbolic expressions and thus should benefit from using an efficient approximate solver. Second, we would like to devise an effective heuristic for dynamically switching during the exploration between \fuzzysat\ and a traditional SMT solver depending on the workload generated by the concolic executor on the solver backend.

}

\iffalse
% When paired with \fuzzolic, they can reach higher coverage than state-of-the-art fuzzers on several real-world benchmarks.
 %When integrated into \fuzzolic\ or \qsym, it reduce significantly the solving time during the exploration, allowing these executors to reach higher coverage than state-of-the-art fuzzers on several real-world benchmarks. 
We are currently integrating \fuzzysat\ into \symcc~(\cref{se:related}): although the results are promising, %we detected %on some benchmarks 
%that 
\symcc\ can %sometimes 
make the symbolic state inconsistent in some benchmarks~\cite{symcc-pi-unsat}, preventing \fuzzysat\ from working correctly. %As a future direction, we would like to devise an effective heuristic for dynamically switching during the exploration between \fuzzysat\ and an SMT solver.

%we plan to explore {\em mixed} solving approaches that dynamically switch between \fuzzysat\ and SMT solvers during the exploration, trying to maximize the number of solved queries while still drastically reducing the solving time. 

\fi

\balance
eval.tex
% !TEX root = paper.tex
\section{Evaluation}
\label{se:evaluation}

\noindent In this section we %experimentally 
address the following research questions:
%In our experiments we tackle the following research questions:

\begin{itemize}

\item {\bf RQ1}: How effective and efficient is \fuzzysat\ at solving queries generated by concolic executors?
\item {\bf RQ2}: How do different kinds of mutations help \fuzzysat\ in solving queries?
\item {\bf RQ3}: How does \fuzzolic\ with \fuzzysat\ compare to state-of-the-art fuzzers on real-world programs?
%\item {\bf RQ2}: How does \fuzzolic\ with \fuzzysat\ compare to state-of-the-art fuzzers on real-world programs?
%\item {\bf RQ3}: Can \fuzzysat\ be used in other hybrid fuzzers?

\end{itemize}

{\bf Benchmarks.} Throughout our evaluation, we consider the following 12 programs: advmng 2.00, bloaty rev {\tt 7c6fc}, bsdtar rev. {\tt f3b1f}, djpeg v9d, jhead 3.00-5, libpng 1.6.37, lodepng-decode rev. {\tt 5a0dba}, objdump 2.34, optipng 0.7.6, readelf 2.34, tcpdump 4.9.3 (libpcap 1.9.1), and tiff2pdf 4.1.0. These targets have been heavily fuzzed by the community~\cite{google-oss-fuzz}, and used in previous evaluations of state-of-the-art fuzzers~\cite{SYMCC,QSYM,ECLIPSER-ICSE19,WEIZZ,redqueen}. As seeds, we use the AFL test cases~\cite{AFL}, or when missing, %for a program, 
minimal syntactically valid files~\cite{small-files-project}.

%In our experiments, we consider the following programs (version, seed): advmng (2.00, {\tt mappy.png}), bloaty (rev. {\tt 7c6fc}, {\tt small\_exec.elf}), bsdtar (rev. {\tt f3b1f}, {\tt tar.tar}), djpeg (v9d, {\tt not\_kitty.jpg}), jhead (3.00-5, {\tt not\_kitty.jpg}) libpng (1.6.37, {\tt not\_kitty.png}), lodepng-decode (rev. 5a0dba, {\tt not\_kitty.png}), objdump (2.34, {\tt small\_exec.elf}), optipng (0.7.6, {\tt not\_kitty.png}), readelf (2.34, {\tt small\_exec.elf}), tcpdump (4.9.3 with libpcap 1.9.1, {\tt small\_capture.pcap}), and tiff2pdf (4.1.0, {\tt not\_kitty.tiff}).
%These have been selected by considered targets used in previous evaluations of state-of-the-art fuzzers~\cite{}. As seeds, we use the AFL test cases, or when missing for a program, minimal syntactically valid files~\cite{}.

 % provides details on their setup.
\vspace{0.2mm}
{\bf Experimental setup.} We ran our tests in a Docker container based on the Ubuntu 18.04 image, using a server with two Intel Xeon E5-4610v2@2.30 GHz CPUs and 256 GB of RAM. %, running Debian 9.2 x86\_64. % As we consider 16 configurations and 2 scenarios, our tests add up to $\sim2300$ CPU hours.

\subsection{RQ1: Solving effectiveness of \fuzzysat}

To evaluate how effective and efficient is \fuzzysat\ at solving queries generated by concolic execution, we discuss an experimental comparison of \fuzzysat\ against the SMT solver Z3 and the approximate solver \jfs. We first focus on {\sc Solve} queries, collected by running the 12 programs under QSYM on their initial seed with optimistic solving disabled, comparing the solving time and the number of queries successfully proved as satisfiable when using these three solvers. Then, we analyze the performance of \qsym\ at finding bugs on the LAVA-M dataset~\cite{LAVAM} when using \fuzzysat\ with respect to when using Z3, implicitly considering the impact also of other reasoning primitives (e.g., {\sc SolveMax}) and from enabling optimistic solving in {\sc Solve}. In these experiments, we consider \qsym\ instead of \fuzzolic\ to avoid any bias resulting from its expression generation phase that could benefit \fuzzysat\ and impair the other solvers.

%In particular, we evaluate the solving time and the number of queries successfully proved as satisfiable from these solvers, considering queries generated by the concolic executor from \qsym\footnote{We use \qsym\ instead of \fuzzolic\ to avoid any bias resulting from the expression generation phase that could favor \fuzzysat.} when running each benchmark on one seed. Finally, we compare the performance of \qsym\ at finding bugs on the LAVA-M dataset~\cite{LAVAM} when using \fuzzysat\ with respect to when using Z3.

\input{table-fuzzy-vs-z3}

\medskip
{\bf \bfseries{{\scshape Fuzzy-Sat} vs Z3}.}
Table~\ref{tab:z3-vs-fuzzy} provides an overview of the comparison between \fuzzysat\ and Z3 on the queries generated %by \qsym\ 
when running the 12 benchmarks. %To obtain more significant results, we repeated the experiment 5 times and show the average across the runs in the table. 

The first interesting insight is that only a small subset of the queries, i.e., less than 10\%, has been proved satisfiable (even when considering together both solvers). The remaining queries are either proved unsatisfiable or make the solvers run out of the time budget (10 seconds for Z3, as in \qsym). %\footnote{We consider a timeout of 10 seconds for Z3, as in \qsym.}. 

The second insight is that, when focusing on the queries that are satisfiable, \fuzzysat\ is able to solve the majority of them and can even perform better than Z3 on a few benchmarks: for instance, \fuzzysat\ solves $301$ ($236.7+64.3$) queries on average on advmng, while Z3 stops at $243.7$ ($236.7+7$). Although this may seem unexpected, this result is consistent with past evaluations from state-of-the-art fuzzers~\cite{ECLIPSER-ICSE19,redqueen} that have shown that a large number of branch conditions %in several real-world programs 
can be solved even without SMT solvers. Nonetheless, there are still a few queries were \fuzzysat\ is unable to find a valid assignment while Z3 is successful, e.g., \fuzzysat\ misses 7 queries on bloaty (but solves one query that makes Z3 run out of time). Assessing the impact of {\em solving} or {\em not solving} a query in concolic execution is a hard problem, especially when bringing into the picture hybrid fuzzing and its non-deterministic behavior. Hence, we only try to indirectly speculate on this impact by later discussing the results on the LAVA-M dataset and the experiments in Section~\ref{ss:eval-coverage}.

%We later try to evaluate the impact of {\em not solving} a query through .

Lastly, we can see in Table~\ref{tab:z3-vs-fuzzy} that on average \fuzzysat\ requires $31\times$ less time than Z3 to reason over the queries from the 12 benchmarks. When putting together this result with the previous experimental insights, we could speculate why \fuzzysat\ could be beneficial in the context of concolic execution: it can significantly reduce the solving time during the concolic exploration while still be able to generate a large number of (possibly valuable) inputs.

One natural question is whether one could get the same benefits of \fuzzysat\ by drastically reducing the time budget given to Z3. To tackle this observation, Figure~\ref{fig:fuzzy-sat-vs-z3-jsf}a reports the number of queries solved by Z3 when using a timeout of 1 second and Figure~\ref{fig:fuzzy-sat-vs-z3-jsf}b shows how the speedup from \fuzzysat\ is reduced in this setup. \fuzzysat\ is still $9.5\times$ faster than Z3 and the gap between the two %solvers 
in terms of solved queries increases significantly ($+12\%$ in \fuzzysat), suggesting that this setup of Z3 is not as effective as one may expect.

\medskip
{\bf \bfseries{{\scshape Fuzzy-Sat} vs {\scshape JSF}.}} One solver that shares the same spirit of \fuzzysat\ is \jfs\ (\cref{se:related}), which however is based on a different design. When considering the queries collected on the 12 benchmarks, it can be seen in Figure~\ref{fig:fuzzy-sat-vs-z3-jsf}a that \jfs\ is able to solve only 1106 queries, significantly less than the 1534 from \fuzzysat. On 127 out of the 325 queries from bsdtar, \jfs\ has failed to generate the program to fuzz due to the large number of nested expressions contained in the queries, %contributing at 
yielding a gap of $95$ solved queries between two solvers. The remaining missed queries can be likely explained by considering that: (a) it is not currently possible to provide the input test case $i$ used for generating the queries to the fuzzer executed by \jfs~\cite{jfs-custom-seeds}, as \jfs\ generates a program that takes an input that is different (in terms of size and structure) from $i$ and builds its own set of seeds, (b) \jfs\ does not provide specific insights to the fuzzer on how to mutate the input, and (c) \jfs\ uses {\sc LibFuzzer}~\cite{libfuzzer}, which does not integrate several fuzzing techniques that have inspired \fuzzysat.  

When considering the solving time, \fuzzysat\ is $1.5\times$ faster than \jfs\ (Figure~\ref{fig:fuzzy-sat-vs-z3-jsf}b). However, 
%\fuzzysat\ when used inside a concolic executor during the exploration can avoid to fully repeat the analysis stage for each query, as it can reuse cached learned facts from previous calls of the reasoning primitives. When enabling the cache, \fuzzysat\ is significant faster than \jfs, reaching a speedup of $4.7\times$. 
when enabling analysis cache in \fuzzysat, the speedup increases up to $4.8\times$.

\jfs\ does not currently provide a C interface~\cite{jfs-c-interface}, requiring concolic executors to dump the queries on disk: as this operation can take a long time in presence of large queries, we do not consider \jfs\ further in the other experiments.

\begin{figure}[!t]
    \centering
    \begin{minipage}{.03\textwidth}
        \centering
        {\scriptsize (a)}\hspace*{-5mm}
    \end{minipage}%
    \begin{minipage}{.23\textwidth}
        \centering
        \includegraphics[width=0.75\linewidth]{charts/queries/chart}
    \end{minipage}%
    \begin{minipage}{.03\textwidth}
        \centering
        {\scriptsize (b)}\hspace*{-5.0mm}
    \end{minipage}%
    \begin{minipage}{0.23\textwidth}
        \centering
        \includegraphics[width=0.75\linewidth]{charts/speedup/chart}
    \end{minipage}
    \vspace{-3mm}
    \caption{\fuzzysat\ vs other solvers on the 12 benchmarks: (a) number of queries proved satisfiable and (b) speedup on the solving time.\label{fig:fuzzy-sat-vs-z3-jsf}}
\end{figure}

\smallskip
{\bf \bfseries{{\scshape Fuzzy-Sat} on LAVA-M.}} %
%\fuzzysat\ cannot solve the {\em same} set of queries as Z3 but can solve a large fraction of them in a smaller amount of time, while also solving in some cases a few additional queries that makes Z3 fail due to timeouts. Hence, given a query and a large budget of time, Z3 is still a better choice to \fuzzysat. However, a concolic executor typically sets a (short) timeout to each query to allow progress during the exploration and thus \fuzzysat\ can be beneficial in this context as although it may miss some queries along the road, it allows the concolic executor to process a larger set of queries over time, possibly bringing a positive outcome at end of the experiment compared to when using an SMT solver.
%
To test %this hypothesis, 
whether \fuzzysat\ can solve queries that are valuable for a concolic executor,
we repeated the experiment on the LAVA-M dataset from the \qsym\ paper~\cite{QSYM}, % using a similar setup, 
looking for bugs within the four benchmarks base64, md5sum, uniq, and who. Table~\ref{tab:fuzzy-lava-m} reports the average and max number of bugs found during 5-hour experiments across 5 runs. \qsym\ with \fuzzysat\ finds on average more bugs than \qsym\ with Z3 on 3 out of 4 programs. In particular, the improvement is rather significant on who, where \fuzzysat\ allows \qsym\ to find $3\times$ more bugs compared to Z3, suggesting that trading performance for accuracy can be valuable in the context of hybrid fuzzing.

Interestingly, \fuzzysat\ was able to reveal bugs that the original authors from LAVA-M were unable to detect~\cite{LAVAM}, % reproduce
e.g., \fuzzysat\ has revealed 136 new bugs on who. Since other works~\cite{ECLIPSER-ICSE19,redqueen} reported a similar experimental observation, the additional bugs are likely not false positives.


 %similar experimental observation was pointed out also in prior works~\cite{ECLIPSER-ICSE19,redqueen}, suggesting that our additional bugs were not false positives. 


\input{table-lava-m}

\subsection{RQ2: Impact of different kinds of mutations in \fuzzysat}
\label{ss:mutation-stats}


\input{table-fuzzy-stats}

An interesting question is which mutations contribute at making \fuzzysat\ effective. Table~\ref{tab:fuzzy-mutations-stats} reports which transformations have been crucial to solve the queries from the 12 benchmarks%under \qsym\ on their seed,
, assigning a query to the multi-goal strategy when \fuzzysat\ had to reason over conflicting expressions from $\pi$ to solve the query. \fuzzysat\ was able to solve more than $51\%$ of the queries by applying input-to-state transformations, and an additional $17\%$ was solved by exploiting the interesting constants collected during the analysis stage. Range interval brute-force was helpful on around $10\%$ of the queries, while mutations inspired by AFL were beneficial in $8\%$ of them. Gradient descent solved just $1.5\%$ of the queries. However, two considerations must be taken into account: (a) the order of the mutations affect these numbers, as gradient descent is not used when previous (cheaper) mutations are successful, and (b) gradient descent is crucial for solving queries in {\sc SolveMin}, {\sc SolveMax}, and {\sc SolveAll}, which are not considered in this experiment. %Hence, this transformation is still worth to be included in \fuzzysat. 
Finally, the multi-goal strategy of \fuzzysat\ was essential for solving around $11\%$ of the queries.

\subsection{RQ3: \fuzzysat\ in \fuzzolic}
\label{ss:eval-coverage}

\begin{figure*}[!t]
    \centering
    \begin{minipage}{.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/bsdtar}
    \end{minipage}%
    \begin{minipage}{0.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/djpeg}
    \end{minipage}
    \begin{minipage}{0.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/libpng}
    \end{minipage}
    \begin{minipage}{0.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/objdump}
    \end{minipage}
    \\\vspace{-2mm}
    \begin{minipage}{.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/optipng}
    \end{minipage}%
    \begin{minipage}{0.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/readelf}
    \end{minipage}
    \begin{minipage}{0.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/tcpdump}
    \end{minipage}
    \begin{minipage}{0.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/tiff2pdf}
    \end{minipage}%\vspace{-1mm}
    \caption{Coverage map density % over time 
    reached by \fuzzolic\ with \fuzzysat\ vs other state-of-the-art fuzzers. The shaded areas are the 95\% confidence intervals.\label{fig:coverage-fuzzolic}} % (8 hours, 5 runs)
\end{figure*}

To further assess the effectiveness of \fuzzysat, we compare \fuzzolic, which is built around this solver, against state-of-the-art binary open-source fuzzers on the 12 benchmarks, tracking the code coverage reached during 8-hour experiments (10 runs). Besides \fuzzolic, we consider: (a) \aflpp~\cite{AFLPP} rev. {\tt 3f128} in QEMU mode, which integrates~\cite{aflpp-colorization} the colorization technique from \redqueen, as well as other improvements to \afl\ proposed by the fuzzing community during the last years~\cite{AFLPP-WOOT20}, (b) \eclipser\ rev. {\tt b072f}, %which computes $\pi$ as a set of range intervals, devising 
which devises one of the most effective {\em approximations} of concolic execution in literature, and (c) \qsym\ rev. {\tt 89a76} with Z3. As both \fuzzolic\ and \qsym\ are hybrid fuzzers that are designed to run in parallel with two instances ($F_m$, $F_s$) of a coverage-guided fuzzer, we consider for a fair comparison \aflpp\ and \eclipser\ in a similar setup, running them in parallel to ($F_m$, $F_s$) and allowing the tools to sync their input queues~\cite{aflpp-parallel-mode}. Hence, each run takes $8\times3=24$ CPU hours. For $F_m$ we use \aflpp\ in {\em master mode}, which performs deterministic mutations, while for $F_s$ we use \aflpp\ in {\em slave mode} that only executes non-deterministic mutations. Since \eclipser\ does not support a parallel mode, we extended it to allow \aflpp\ to correctly pick inputs from its queue. 
%As previous works~\cite{SYMCC,QSYM}, we consider the coverage map density in $F_s$ as an indirect indicator for the code coverage reached by the different fuzzers. As bitmap collisions may occur~\cite{COLL-AFL}, we validated the trends by computing the number of basic blocks using a QEMU-based tool~\cite{AFL-COV}.

% \footnote{The first instance runs in master mode, performing deterministic mutations, while the second one runs in slave mode, performing non deterministic mutations.}

Figure~\ref{fig:coverage-fuzzolic} shows the code coverage reached by the different fuzzers on 8 out of 12 programs. On the remaining four benchmarks, the fuzzers reached soon a very similar coverage, making it hard to detect any significant trend and thus we omit their charts due to lack of space. Similar to other works~\cite{QSYM,SYMCC}, we plot the density of the coverage map from $F_s$ and depict the 95\% confidence interval using a shaded area. As bitmap collisions may occur~\cite{COLL-AFL}, we validated the trends by also computing the number of basic blocks~\cite{AFL-COV}. %  using a QEMU-based tool

% Interestingly, during these experiments \fuzzolic\ identified a bug (invalid free) in objdump 2.34, that however was reported by other users few weeks earlier and fixed in release 2.35.

\begin{figure}[!t]
    \centering
    \begin{minipage}{.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage2/tcpdump}
    \end{minipage}%
    \begin{minipage}{0.245\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage2/objdump}
    \end{minipage}%\vspace{-1mm}
    \caption{Coverage map density%reached 
    : impact of \fuzzysat\ in \qsym.\label{fig:coverage-qsym-symcc}}
\end{figure}

\fuzzolic\ reaches a higher code coverage than other solutions on 6 programs, i.e., bsdtar, djpeg, objdump, readelf, tcpdump, and tiff2pdf. In particular, tcpdump is the program where \fuzzolic\ shines better, consistently showing over time an increase in the map density of $5\%$ with respect to the second-best fuzzer (\aflpp).  On optipng, although \fuzzolic\ appears to have an edge at the beginning of the experiment, it then reaches a coverage that is comparable to other fuzzers, which are all very close in performance. Finally, \fuzzolic\ falls behind other approaches on libpng, pinpointing one case where \fuzzysat\ seems to underperform compared to Z3, as \qsym\ dominates on this benchmark. 

%: when debugging, we identified a few queries that Z3 in \qsym\ (the best one in this experiment) is able to solve, while \fuzzysat\ fails at reasoning over them due to extremely complex constraints. 

When comparing closely \fuzzolic\ to \qsym, the improvement in the coverage is likely due to the better scalability of the former with respect to the latter. For instance, on tcpdump \fuzzolic\ performs concolic execution on $11089$ inputs ($1.8$ secs/input), generating $14415$ alternative inputs, while \qsym\ only analyzes $376$ inputs ($71.4$ secs/input) and generates $786$ alternative inputs. When considering libpng, \fuzzolic\ is still faster than \qsym\ ($8.8$ secs/input vs $43.6$ secs/input) but the number of inputs available in the queue from $F_s$ (from which \fuzzolic\ and \qsym\ pick inputs) over time is very low. %, and thus \fuzzolic\ spends most of its time waiting for new inputs without performing any valuable work. 
Hence, the difference between \fuzzolic\ and \qsym\ on libpng is due to a few but essential queries that Z3 is able to solve while \fuzzysat\ fails to reason on.

The better scalability of \fuzzolic\ with respect to \qsym\ is given by the combination of an efficient solver (\fuzzysat) and an efficient tracer (\fuzzolic). Indeed, when replacing Z3 with \fuzzysat\ in \qsym, this concolic executor improves its performance but still falls behind \fuzzolic. Figure~\ref{fig:coverage-qsym-symcc} compares the coverage of \qsym\ with the two solvers and \fuzzolic\ on two benchmarks. On tcpdump, \qsym\ with \fuzzysat\ is able to analyze $2111$ inputs ($10.1$ secs/input) and generate $3690$ alternative inputs, improving the coverage by 4$\%$ on average with respect to Z3 but still performing worse than \fuzzolic. Similarly, on objdump the improvement in \qsym\ due to \fuzzysat\ is even more noticeable
 but still \qsym\ cannot match the coverage reached by \fuzzolic.

%\qsym\ with \fuzzysat\ is slower than \fuzzolic\ (15.9 secs/input vs 6 secs/input) but slowly catches up it in terms of coverage. % at the end of the experiment.

When comparing \fuzzolic\ to \eclipser\ and \aflpp, the results suggest that % although \fuzzysat\ is inspired by ideas from the CGF domain, 
the integration of fuzzing techniques into a solver provides a positive impact. Indeed, while these fuzzers scales better than \fuzzolic, processing hundreds of inputs per second, they lack the knowledge that \fuzzysat\ extracts from the symbolic expressions, which is used to perform effective mutations. Overall, colorization from \aflpp\ and approximate concolic execution from \eclipser\ seem to generate similar inputs on several benchmarks, yielding often a similar coverage in our parallel fuzzing setup.
Moreover, despite \fuzzolic\ may spend several seconds over a single input, it collects information that allows it to fuzz a large number of branch conditions, paying on average only a few microseconds when testing an input assignment. Hence, the time spent building the symbolic expressions can be amortized over thousands of (cheap) query evaluations, reducing the gap between the efficiency of a fuzzer and a concolic executor. Nonetheless, \fuzzolic\ is still a hybrid fuzzer and it needs to run in parallel to a traditional fuzzer to provide good results, since some non-deterministic mutations, such as randomly combining inputs, are not performed by \fuzzolic.

%While fuzzing the 12 benchmarks, as well as other real-world programs, \fuzzolic\ has identified several bugs. In particular, \fuzzolic\ has revealed unknown bugs~\cite{jhead-1,jhead-2,grep-1,grep-2} in jhead and GNU grep. We refer the reviewers to the supplementary material for a detailed list of the bugs.

 %While some of them are already known to the developers, 


% \subsection{RQ3: \fuzzysat\ in other hybrid fuzzers}

%\fuzzysat\ can be integrated into other hybrid fuzzers besides \fuzzolic. 

\iffalse
When replacing Z3 with \fuzzysat\ in \qsym, this hybrid fuzzer is often able to improve its code coverage on the 12 benchmarks. For instance, on tcpdump \qsym\ reveals an improvement of $4\%$ on the coverage map density as shown by the left side of Figure~\ref{fig:coverage-qsym-symcc}. \fuzzysat\ is able to speedup significantly \qsym\ on this benchmark, allowing it to analyze $2111$ inputs ($10.1$ secs/input) and generate $3690$ alternative inputs. Nonetheless, \qsym\ with \fuzzysat\ still scales worser than \fuzzolic\ for two main reasons: (a) the tracer of \fuzzolic\ is faster than \qsym\ at building symbolic expressions, and (b) \qsym\ performs expression optimizations that helps an SMT solver but can make harder the life of \fuzzysat, slowing it down.


Recently, \symcc\ has proposed a concolic executor that drastically reduces the time needed for building the symbolic expression during the exploration. The key idea is to perform source-instrumentation instead of dynamic binary instrumentation (as in \qsym\ and \fuzzolic). The downside of this approach is that it requires to recompile the program, as well as any library, using a custom toolchain. Since this operation can be very complex in practice, \symcc\ also provides some {\em models} to deal with standard libraries, such as the C library, that make it possible to reason symbolically on them even without recompilation. When running \fuzzysat\ in \symcc\ on the 12 programs, we could not observe a large improvement in the coverage compared to when using Z3. After debugging, we identified two main issues: (a) \symcc\ does not perform {\sc SolveMax}, {\sc SolveMin}, and {\sc SolveAll} queries, and (b) \symcc\ lacks models for several functions of the C library\footnote{The authors of \symcc\ do not recompile the C library in their experiments.}, leading even to inconsistent path constraints in some cases. Hence, although \fuzzysat\ can significantly reduce the solving time in \symcc\ (e.g., speedup of $3.8\times$ on tcpdump), \symcc\ when using it spends most of its time waiting for new inputs, exacerbating the scenario observed with \fuzzolic\ on libpng. To mitigate these problems, we added new models to \symcc~\cite{}, which however are very hard to write and easy to get wrong, and devised a {\em fallback} strategy in the concolic executor: whenever no new inputs to process are available from $F_s$, it temporarily starts an additional \aflpp\ slave.  The right side of Figure~\ref{fig:coverage-qsym-symcc} shows the improvement in the coverage map density achieved by \symcc\ on tcpdump when enabling the fallback strategy: the speedup on the solving time due to \fuzzysat\ can be beneficial to the hybrid fuzzer as it can perform additional fuzzing attempts with \aflpp, leading to overall higher code coverage.
\fi

\iffalse
\begin{figure}[!t]
    \centering
    \begin{minipage}{0.24\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/libpng}
        %\caption{$dt =$}
        %\label{fig:prob1_6_1}
    \end{minipage}
    \begin{minipage}{0.24\textwidth}
        \centering
        \includegraphics[width=0.99\linewidth]{charts/coverage/objdump}
        %\caption{$dt =$}
        %\label{fig:prob1_6_1}
    \end{minipage}
    \caption{Density of the AFL++ map density over time (8 hours, 5 runs) reached by QSYM with \fuzzysat\ vs \qsym with Z3.}
\end{figure}
\fi
implem.tex
% !TEX root = paper.tex
\section{Implementation}
\label{se:implem}

\fuzzysat\ is written in C (10K LoC) and evaluates queries in the language used by the Z3 Theorem Prover~\cite{Z3-TACS08}. To efficiently evaluate an expression given a concrete assignment %for the symbolic inputs, 
\fuzzysat\ uses a fork of Z3 where  the {\tt Z3\_model\_eval} function has been optimized to deal with full concrete models.
    %\item We forked Z3 to optimize the cost of evaluating an expression given a concrete assignment for the symbolic inputs.   

\fuzzolic\ is a new concolic executor based on {\sc QEMU} 4.0 (user-mode), written in C (20K LoC), that currently supports Linux x86\_64 binaries. Its design overcomes one of the major problems affecting \qsym: \fuzzolic\ decouples the tracer component, which builds the symbolic expressions, from the solving component, which reasons over them. This is required as recent releases of most DBI frameworks, such as {\sc PIN}~\cite{Pin-PLDI05} on which \qsym\ is based on, do not allow an analysis tool to use external libraries (as the Z3 solver in case of \qsym) when they may produce side effects on the program under analysis~\cite{DCNPC-ASIACCS19}. This implementation constraint has made it very complex to port QSYM to newer releases of PIN, limiting its compatibility with recent software and hardware configurations\footnote{QSYM has been recently removed from the Google project FuzzBench due to its instability on recent Linux releases~\cite{qsym-removed-fuzzbench}.}. To overcome this issue, the two components are executed into distinct processes in \fuzzolic. In particular, the tracer runs under QEMU and generates symbolic expressions in a compact language, storing them into a shared memory that is also attached to the memory space of the solving component, which in turn %translates the expressions into the Z3 language, 
submits queries to \fuzzysat\ to generate alternative inputs. Similarly to \qsym, \fuzzolic\ runs in parallel with two coverage-guided fuzzers.


%is optimized for hybrid fuzzing, where the concolic executor 


intro.tex
% !TEX root = paper.tex
\section{Introduction}
\label{se:intro}

The automatic analysis of modern software, seeking for high coverage and bug detection is a complex endeavor. %In addition to a plethora of static methods~\cite{Jihyun12}, two main orthogonal 
Two popular approaches have been widely explored in the literature: on one end of the spectrum, {\em coverage-guided fuzzing} starts from an input seed and applies simple transformations (mutations) to the input, re-executing the program to be analyzed to increase the portion of explored code. The approach works particularly well when the process is guided and informed by code coverage, with a nearly-native execution time per explored path~\cite{AFL,AFLPP}. On the other end of the spectrum, {\em symbolic execution} (SE) assigns symbolic values to input bytes and builds expressions that describe how the program manipulates them, resorting to satisfiability modulo theories (SMT)~\cite{Barrett2018} solver queries to reason over the program, e.g., looking for bug conditions. A popular variant of SE is {\em concolic execution} (CE), which concretely runs one path at a time akin to a fuzzer, collecting branch conditions along the way~\cite{QSYM, SYMCC}. By systematically negating these conditions, it steers the analysis to take different paths, aiming to increase code coverage. The time per executed path is 
%substantially 
higher than fuzzing but the aid of a solver allows for a smaller number of runs. %A concolic engine is based on two parts: tracing, which executes one path at a time by collecting symbolic expressions and solving, which negates branch conditions.

%Fuzzing~\cite{afl} proved itself to be a scalable an effective technique to identify bugs in real-world software. The idea is to apply simple transformations (mutations) to the input and re-execute the program to be analyzed to increase the portion of explored code. The approach works very well when the process is guided and informed by code coverage.

Different ideas have been proposed to improve the effectiveness of analysis tools by combining ideas from both fuzzing and SE somewhere in the middle of the spectrum. As a prominent example, {\em hybrid fuzzing} couples a fuzzer with a symbolic executor to enable the exploration of complex branches~\cite{stephens2016driller, QSYM}. Compared to base fuzzing, this idea adds a heavy burden due to the lack of scalability of symbolic execution. It is therefore of paramount importance to speed up the symbolic part of the exploration.

%{\em Taint analysis} within a fuzzer attempts to identify which input bytes impact on branch conditions and deserve exploration \cite{VUZZER, ANGORA}. While being less heavy than symbolic execution, taint analysis is still costly in the context of fuzzing. {\em Approximate taint tracking} within a fuzzer based on differential analysis~\cite{WEIZZ,REDQUEEN} identifies input bytes with dependencies and a notion of input-to-state (I2S) to determine which transformations to apply.

%The complexity of analyses performed by modern fuzzers is growing over time, slowly and gradually moving from grey-box to white-box.

While there is no clear winner in the software testing %various regions of the considered
spectrum, %testing 
tools that hinge upon an SMT solver get a high price to pay in terms of running time, limiting their throughput.

\medskip
\noindent{\bf Contributions.} As a main contribution, this paper addresses the following research question:

%This paper proposes novel techniques to speed up the symbolic portion of a hybrid fuzzer. To this aim, we address two main research questions:

\begin{quote} {\em can we avoid using accurate but costly SMT solvers, replacing them with an approximate solver to test satisfiability in the context of software testing?}
\end{quote}

%\noindent We positively answer this question, devising \fuzzysat, an approximate solver that uses ideas borrowed from the fuzzing domain. Our solver is tailored to the symbolic formulas generated by concolic engines and can replace classic SMT solvers in this context.
\noindent We attempt to positively answer this question, devising \fuzzysat, an approximate solver that borrows ideas from the fuzzing domain. Our solver is tailored to the symbolic expressions generated by concolic engines and can replace classic SMT solvers in this context. By analyzing the expressions contained in symbolic queries, \fuzzysat\ performs {\em informed} mutations to possibly generate new valuable inputs.
% 
To demonstrate the potential behind \fuzzysat, we present \fuzzolic, a new hybrid fuzzer based on QEMU. To show that \fuzzysat\ can be used in other frameworks, we integrate it also in QSYM~\cite{QSYM}.
%We also show that \fuzzysat\ can be easily integrated in other frameworks, such as QSYM~\cite{QSYM} and SymCC~\cite{SYMCC}. 
In our experimental evaluation:

%Our experimental results can be summarized as follows:

\begin{enumerate}
\item we compare \fuzzysat\ to the SMT solver Z3~\cite{Z3-TACS08} and the approximate solver \jfs~\cite{JFS} on queries issued by QSYM, which we use as a mature baseline. Our results suggest that \fuzzysat\ can provide a nice tradeoff between speed and solving effectiveness, i.e., the number of queries found satisfiable by a solver.

%We address speed and effectiveness, i.e., the number of queries found satisfiable by a solver, showing that \fuzzysat\ provides a nice tradeoff between 
%vs. Z3, showing speedups up to $1000\times$ at the cost of a mean accuracy of 90\%;

\item we show that \fuzzysat\ allows \qsym\ to find more bugs on the LAVA-M dataset~\cite{LAVAM} compared to Z3.% We also show that \fuzzolic\ can find previously unknown bugs in real-world programs (e.g., GNU grep).

%can find more bugs on the LAVA-M dataset~\cite{LAVAM} when using \fuzzysat with respect to when using Z3;

%compare QSYM with Z3 and with \fuzzysat\ on the LAVA-M benchmarks, showing that \fuzzysat\ can help \qsym\ find more bugs than Z3;

\item we evaluate \fuzzolic\ on 12 real-world programs against state-of-the-art fuzzers including \aflpp~\cite{AFLPP}, \eclipser~\cite{ECLIPSER-ICSE19}, and \qsym, showing that it can reach higher code coverage than the competitors. %We also investigate whether \fuzzysat\ can bring similar benefits when integrated into \qsym\ and \symcc.
%
%using different tools: AFL++~\cite{AFLPP} (state-of-the-art in fuzzing), QSYM with AFL++ (state-of-the-art in hybrid fuzzing), Eclipser~\cite{ECLIPSER-ICSE19} with AFL++ (state-of-the-art in approximate fuzzing), and \fuzzolic, our own tool. We also compare Z3 with \fuzzysat\ in SymCC. The results show that \fuzzysat\ is both competitive with and complementary to state-of-the-art solvers such as Z3.
\end{enumerate}


To facilitate extensions of our approach, we make our contributions available at:
\begin{center}
{\tt \url{https://season-lab.github.io/fuzzolic/}}
\end{center}
\iffalse
We make \fuzzolic available as open source at:
\begin{center}
{\tt \url{}}
\end{center}
\fi

\iffalse
\medskip

We experimentally show that our approximate solver is competitive with accurate SMT solvers such as Z3 
%%in the context of concolic and hybrid fuzzing testing tools, 
and can deliver better performance on a variety of benchmarks.

To perform our experiments, we integrated \fuzzysat\ in QSYM~\cite{QSYM} and in SymCC~\cite{SYMCC}, showing that it can be the back-end of different tools. We also devise our own hybrid fuzzing engine, \fuzzolic, which we wrote from scratch as a playground for testing \fuzzysat.

Our experimental results can be summarized as follows:

\begin{enumerate}
\item we compare \fuzzysat\ with Z3 on queries issued by QSYM, which we use as a mature baseline. We address speed and accuracy, i.e., the number of SAT queries found using \fuzzysat\ vs. Z3, showing speedups up to $1000\times$ at the cost of a mean accuracy of 90\%;
\item we compare QSYM with Z3 and with \fuzzysat\ on the LAVA-M benchmarks, showing that they find the same bugs;
\item we show coverage using different tools: AFL++~\cite{AFLPP} (state-of-the-art in fuzzing), QSYM with AFL++ (state-of-the-art in hybrid fuzzing), Eclipser~\cite{ECLIPSER-ICSE19} with AFL++ (state-of-the-art in approximate fuzzing), and \fuzzolic, our own tool. We also compare Z3 with \fuzzysat\ in SymCC. The results show that \fuzzysat\ is both competitive with and complementary to state-of-the-art solvers such as Z3.
\end{enumerate}
\fi
\iffalse
\medskip
\noindent{\bf Intuition Behind our Approach.}  Our approach applies to {\em concolic} methods, which given a concrete input $i$, analyzes symbolically only the execution path taken by the program when running over $i$. To generate new inputs, the concolic executor can query an SMT solver using $\neg b \wedge \pi$, where $b$ is the branch condition taken by the program in the current path while $\pi$ is the set of constraints resulting from the branches previously met along the path. 
%To negate the branch so that a different path is taken, a traditional engine queries a SMT solver checking whether $\neg b$ and all previously collected branch conditions are satisfied, in short: $\neg b\wedge\pi$. 
We know that $\pi$ is satisfied by the current input $i$ that led the engine to follow the path. $\pi$ may grow large and complex along the way, imposing a heavy burden on a classic solver. However, by ``fuzzing'' $\neg b$ on $i$ we may find a new test case $i'$ that satisfies $\neg b$ and is similar enough to $i$ so that $\pi$ remains satisfied by $i'$. Fuzzing is done by performing small mutations to $i$ on the portion that appears in $b$. Hence, we do not need to run any solver on $\pi$, but just check if $\pi$ is satisfied by $i'$. Clearly, this is tailored to scenarios where $i$ is known such as in concolic execution. We use a timeout on fuzzing $\neg b$ to declare unsatisfiability.
\fi

%L'idea dovrebbe essere: se hai "B and PI" con PI molto complesso un SMT potrebbe spendere molto tempo per trovare una soluzione, mentre fuzzando B si trova una soluzione che va bene anche per PI se si parte da testcase (che di base soddisfa PI e una modifica minimale forse non rompe la SATness di PI)

%The remainder of this paper is organized as follows. [...]
paper.tex
%\documentclass[conference]{IEEEtran}
\documentclass[10pt,conference,final]{IEEEtran}
\IEEEoverridecommandlockouts

% The preceding line is only needed to identify funding in the first footnote. If that is unneeded, please comment it out.

\usepackage{cite}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{algorithmic}
\usepackage{graphicx}
\usepackage{textcomp}
\usepackage{xcolor}
\def\BibTeX{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em
    T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}

\iftrue
\usepackage{hyperref}

\hypersetup{
  colorlinks   = true, %Colours links instead of ugly boxes
  urlcolor     = blue, %Colour for external hyperlinks
  linkcolor    = black, %Colour of internal links
  citecolor   = black %Colour of citations
}
\fi

\usepackage[utf8]{inputenc}
\usepackage{cleveref}
\crefname{section}{§}{§§}
\Crefname{section}{§}{§§}

\usepackage{pifont}
\usepackage{setspace}
\usepackage{algorithmic}
%\usepackage{algorithm2e} % [linesnumbered]
\usepackage{algorithm2e} % [ruled] http://www.ctan.org/pkg/algorithm2e

\usepackage{bold-extra}

\usepackage{balance}

\usepackage{adjustbox,multirow}

\newcommand{\nextnr}{\stepcounter{AlgoLine}\ShowLn}
\makeatletter
\newcommand{\removelatexerror}{\let\@latex@error\@gobble}
\makeatother

% KTSM algorithm2e
\newlength{\textfloatsepsave}
\setlength{\textfloatsepsave}{\textfloatsep} 
\newlength{\floatsepsave}
\setlength{\floatsepsave}{\floatsep} 

\usepackage{xcolor} % http://www.ctan.org/tex-archive/macros/latex/contrib/xcolor
\usepackage{tikz}
\usetikzlibrary{fit,calc}
%define a marking command
\newcommand*{\tikzmk}[1]{\tikz[remember picture,overlay,] \node (#1) {};\ignorespaces}
%define a boxing command, argument = colour of box
\newcommand{\boxit}[1]{\tikz[remember picture,overlay]{\node[yshift=1pt,fill=#1,opacity=.20,fit={(A)($(B)+(.80\linewidth,0.9\baselineskip)$)}] {};}\ignorespaces}
%define some colours according to algorithm parts (or any other method you like)
\colorlet{pink}{red!40}
\colorlet{blue4}{cyan!30}
\colorlet{blue2}{cyan!60}
\colorlet{blue3}{cyan!90}

\colorlet{gray1}{gray!45}
\colorlet{gray2}{gray!90}

\newcommand*{\everymodeprime}{\ensuremath{\prime}}

\usepackage{framed}
\definecolor{shadecolor}{gray}{0.9}
\newcommand{\boxedspit}[1]{
\vspace{-2mm}
\begin{shaded*}
\vspace{-2mm}
#1 % \noindent{\bf\small Example.}
\vspace{-2mm}
\end{shaded*}
\vspace{-2mm}
}

\begin{document}

% macros
\newcommand{\fuzzysat}{{\sc Fuzzy-Sat}}
\newcommand{\fuzzolic}{{\sc Fuzzolic}}
\newcommand{\qsym}{{\sc Qsym}}
\newcommand{\redqueen}{{\sc RedQueen}}
\newcommand{\angora}{{\sc Angora}}
\newcommand{\afl}{{\sc AFL}}
\newcommand{\aflpp}{{\sc AFL++}}
\newcommand{\jfs}{{\sc JFS}}
\newcommand{\angr}{{\sc Angr}}
\newcommand{\binsec}{{\sc BinSec}}
\newcommand{\fuzzball}{{\sc FuzzBall}}
\newcommand{\klee}{{\sc Klee}}
\newcommand{\stwoe}{{\sc S2E}}
\newcommand{\symcc}{{\sc SymCC}}
\newcommand{\slf}{{\sc SLF}}
\newcommand{\eclipser}{{\sc Eclipser}}

%\def\rem#1{{\marginpar{\raggedright\scriptsize #1}}}
\def\rem#1{}
\newcommand\mdoubleplus{\mathbin{+\mkern-10mu+}}

\newcommand{\edits}[1]{#1}

\title{
Fuzzing Symbolic Expressions\\ % for Concolic Execution
\thanks{This paper is supported in part by European Union's Horizon 2020 research and innovation 
programme (grant agreement No. 830892, project SPARTA).}
}

\author{
\IEEEauthorblockN{Luca Borzacchiello}
\IEEEauthorblockA{\textit{DIAG Department} \\
\textit{Sapienza University of Rome}\\
Rome, Italy \\
borzacchiello@diag.uniroma1.it}
\and
\IEEEauthorblockN{Emilio Coppa}
\IEEEauthorblockA{\textit{DIAG Department} \\
\textit{Sapienza University of Rome}\\
Rome, Italy \\
coppa@diag.uniroma1.it}
\and
\IEEEauthorblockN{Camil Demetrescu}
\IEEEauthorblockA{\textit{DIAG Department} \\
\textit{Sapienza University of Rome}\\
Rome, Italy \\
demetres@diag.uniroma1.it}
}

\maketitle

\begin{abstract}
%Finding bugs in software is of paramount importance for its reliability. 
Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, \fuzzysat, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid fuzzers.
%by concolic and hybrid fuzzing engines.
\end{abstract}

\begin{IEEEkeywords}
concolic execution, fuzzing testing, SMT solver%, software testing
\end{IEEEkeywords}

\input{intro}
\input{related}
\input{approach}
\input{implem}
%\newpage
\input{eval}
\input{conclusions}

%\section*{Acknowledgment}
%\newpage
\bibliographystyle{IEEEtran}
\bibliography{IEEEabrv,mybibfile}
\balance


\end{document}

related.tex
% !TEX root = paper.tex
\section{Background}
\label{se:related}

%\rem{Why is SE behind \fuzzysat?}
\fuzzysat\ takes inspiration from
%arises from the combination of 
two popular software testing techniques~\cite{art-software-testing}: symbolic execution~\cite{SurveySymbolic} and coverage-based grey-box fuzzing~\cite{fuzzing-book}. We now review the inner-workings of these two approaches, focusing on recent works that are tightly related to the ideas explored in this paper.
%are essential for evaluating the contributions from \fuzzysat.

\iffalse
In the last decade, several %innovative 
approaches have been %proposed and 
explored in the context of software testing~\cite{art-software-testing}. In this paper, we focus our discussion mainly 
on two popular %and well-known 
techniques, symbolic execution~\cite{SurveySymbolic} and coverage-based grey-box fuzzing~\cite{fuzzing-book}, which are strictly related to the ideas explored in \fuzzysat. 
\fi

%tante tecniche, negli ultimi anni coverage-guided fuzzing e symbolic execution hanno dimostrare molto efficaci per trovare bug in real-world applications. In questo paper, ci focalizziamo su quest'ultime anche le lo stato dell'arte è molto più articolato.

{\bf Symbolic execution.} The key idea behind this technique is to execute a program over {\em symbolic}, rather than {\em concrete}, inputs. Each symbolic input can, for instance, represent a byte read by the program under test from an input file and initially evaluate to any value admissible for its data type (e.g., $[0, 255]$ for an unsigned byte). SE builds expressions to describe how the program manipulates the symbolic inputs, resorting to SMT solver queries to reason over the program state. In particular, when a branch condition $b$ is met during the exploration, SE  checks using the solver whether both directions can be taken by the program for some values of the inputs, forking the execution state in case of a positive answer. When forking, SE updates the list of {\em path constraints} $\pi$ that must hold true in each state: $b$ is added in the state for the {\em true} branch, while $\neg b$ is added to the state for the {\em false} branch. At any time, the symbolic executor can generate concrete inputs, able to reproduce the program execution related to one state, by asking the solver an assignment for the inputs given $\pi$.

%\rem{drop sentence?}
SE can be performed on binary code (e.g., \angr~\cite{ANGR-SSP16}, S$^{2}$E~\cite{S2E-TOCS12}) or on more high-level representations of a program (e.g., LLVM IR in \klee~\cite{KLEE-OSDI08}, Java bytecode in SPF~\cite{SPF}). %While most frameworks focus only on the code from the application, executors such as \stwoe\ are able to analyze symbolically the full software stack.
\edits{Besides software testing, SE has been extensively used during the last decade in the context of cybersecurity~\cite{MAYHEM,BCDD-CSCML17,BCDD-CSCML19}.}

\iffalse
Among several issues that may limit the scalability of symbolic execution over real-world programs~\cite{SurveySymbolic}, {\em path explosion} and {\em hard constraints} are two of the most crucial. The former is caused by the large number of paths that a complex program may have, which in turn result in a large number of states to keep track in parallel during the symbolic exploration. The latter instead is due the high reasoning times of the solver in presence of very complex constraints (e.g., resulting from non-linear computations).
\fi

% Per ragionare sulle espressioni simboliche generate durante l'esplorazione, symbolic execution usa un SMT solver, un oggetto matematico che data un espressione è in grado di trovare (se esiste) un assegnamento per gli input simbolici tale per cui l'espressione risulta soddisfatta. Gli SMT solver sono molto potenti e hanno fatto grandi passi avanti negli ultimi decenni, ma in caso di espressioni molto complesse (es. computazioni crittografiche) possono impiegare un tempo molto lungo e per tale motivo nel contesto di symbolic execution sono normalmente interrogati impostando un budget di tempo massimo su ogni query. 

% L'esecuzione simbolica può essere fatta analizzando una rappresentazione ad alto livello del programma (LLVM IR in KLEE) o una sua rappresentazione binaria (angr, SAGE, binsec, FuzzBALL). Mentre la maggior parte dei framework ragiona su una singola applicazione, esistono esecutori simbolici come S2E in grado di analizzare l'intero stack software.
%\vspace{1mm}
{\bf Concolic execution.} A twist of SE designed with scalability in mind
%that has proved to scale even over real-world programs in the last years 
is concolic execution~\cite{SAGE-NDSS08}, %which we have already sketched at the end of Section~\ref{se:intro}.
%which given a concrete input $i$, analyzes symbolically only the execution path taken by the program when running over $i$. To generate new inputs, the concolic executor can query the solver using $\neg b \wedge \pi$, where $b$ is the branch condition taken by the program in the current path while $\pi$ is the set of constraints resulting from the branches previously met along the path.
%
%Our approach applies to {\em concolic} methods, 
which given a concrete input $i$, analyzes symbolically only the execution path taken by the program when running over $i$. To generate new inputs, the concolic executor can query an SMT solver using $\neg b \wedge \pi$, where $b$ is a branch condition taken by the program in the current path while $\pi$ is the set of constraints from the branches previously met along the path. 
%To negate the branch so that a different path is taken, a traditional engine queries a SMT solver checking whether $\neg b$ and all previously collected branch conditions are satisfied, in short: $\neg b\wedge\pi$. 
%We know that $\pi$ is satisfied by the current input $i$ that led the engine to follow the path. $\pi$ may grow large and complex along the way, imposing a heavy burden on a classic solver. However, by ``fuzzing'' $\neg b$ on $i$ we may find a new test case $i'$ that satisfies $\neg b$ and is similar enough to $i$ so that $\pi$ remains satisfied by $i'$. Fuzzing is done by performing small mutations to $i$ on the portion that appears in $b$. Hence, we do not need to run any solver on $\pi$, but just check if $\pi$ is satisfied by $i'$. Clearly, this is tailored to scenarios where $i$ is known such as in concolic execution. We use a timeout on fuzzing $\neg b$ to declare unsatisfiability.
%
%Numerose sfide limitano la scalabilità di symbolic execution [survey]. Una variante di symbolic execution che ha dimostrato di poter scalare su programmi complessi è concolic execution, che dato un input del programma, analizza simbolicamente il path del programma determinato da quel singolo input, cercando di generare input che portano il programma a visitare i rami alternative dei branch rispetto a quanto fatto dal programma nel path corrente. In altre parole, un esecutore concolico, arrivato su un ramo di una branch condition $b$ preso dal programma, nega la condizione del branch e chiedo al solver di generare un input che soddisfi $!b \wedge \pi$, dove $\pi$ è la congiunzione delle branch condition incontrate lungo il path fino a quel momento.
%
A benefit from this approach is that the concolic executor only needs to query the solver for one of the two branch directions, as the other one is taken by the path under analysis. Additionally, if the program is actually executed concretely in parallel during the analysis, the concolic engine can at any time trade accuracy for scalability, by concretizing some of the input bytes and make progress in the execution using the concrete state. For instance, %\rem{drop entire sentence, or at least from "without"?} 
 when analyzing a complex library function, the concolic engine may {\em concretize} the arguments for the function and execute it concretely, without issuing any query or making $\pi$ more complex due to the library code but possibly giving up on some alternative inputs due to the performed concretizations.

%Un vantaggio di questo approccio è che non occorre eseguire query per entrambi i rami di un  branch (uno dei due è preso dall'input corrente). Inoltre, se l'esecuzione concolica viene fatta parallelamente all'esecuzione concreta de programma, allora risulta possibile utilizzare ove necessario informazioni dello stato concreto nell'analisi simbolica, aumentando la scalabilitá dell'approccio seppur rinunciando ad accuratezza nell'analisi. Ad esempio, se un programma esegue una libreria di sistema, che l'esecutore simbolica non può (limiti implementativi) o non vuole analizzare (path explosion), un esecutore concolico può ragionare concretamente su quella parte dell'esecuzione, e poi riprendere il ragionamento simbolico su altre parti, rinunciando tuttavia ad analizzare alcuni possibile path a causa delle concretizzazioni effettuate.

A downside of most concolic executors is that they restart from scratch for each input driving the exploration, thus
repeating analysis work across different runs. %While state snapshotting techniques~\cite{} may mitigate this problem,
To mitigate this problem, \qsym~\cite{QSYM} has proposed a concolic executor built through dynamic binary instrumentation (DBI) that cuts down the time spent for running the program by maintaining only the symbolic state and offloads completely the concrete state to the native CPU. Additionally, it simplifies the symbolic state %in case of symbolic memory accesses 
by concretizing symbolic addresses~\cite{CDD-ASE17,BCE-STVR19} but also generates inputs that can lead the program to access alternative memory locations. More recently, \symcc~\cite{SYMCC} has improved the design of \qsym\ by proposing a source-based instrumentation approach that further reduces the emulation time.

%Uno svantaggio di molti esecutori concolici è che per ogni path (input) devono ricostruire da zero l'intero stato su cui ragionano, ripetendo lavoro già effettuato per i path analizzati in precedenza. QSYM riduce questo tempo di "emulazione" proponenendo un approccio basato su DBI che mantiene solo lo stato simbolico del programma, lasciando interamente alla CPU l'onere di mantenere lo stato concreto. Per semplificare ulteriormente lo stato simbolico, QSYM inoltre concretizza eventuali indirizzi simbolici, limitandosi a generare input in grado di far leggere o scrivere al programma indirizzi alternativi, senza utilizzare approcchi più robusti (es. basati su teoria degli array) in grado di ragionare sugli effetti degli accessi simbolici. Più recedentemente, SymCC ha raffinato ulteriormente l'idea di abbattere il tempo di emulazione, proponendo un approccio simile a QSYM ma basato su source-instrumentation.

\smallskip
{\bf Approximate constraint solving.} %Solving a query may take a very long time. To make the analysis scalable, concolic executors typically sets a maximum time budget when submitting a query to a solver, deeming it unsatisfiable in case of timeout. 
Many queries generated by concolic executors are either unsatisfiable or cannot be solved within a limited amount of time~\cite{QSYM}. This often is due to the complex constraints contained in $\pi$, which can impact the reasoning time even when the negated branch condition is quite simple. For this reason, \qsym\ has introduced {\em optimistic solving} that, in case of failure over $\neg b \wedge \pi$ due to unsatness or solving timeout, submits to the solver an additional query containing only $\neg b$: by patching the input $i$ (used to drive the exploration) in a way that makes $\neg b$ satisfied, the executor is often able to generate valuable inputs for a program.

% Una parte consistente del tempo speso durante l'esecuzione simbolica è impiegata a ragionare sulle espressione simboliche, utilizzando un SMT solver. Oltre tutta una serie di ottimizzazioni orientate ad ottimizzare le query sottomesse al solver, o ridurne il loro numero, alcuni lavori nell'ambito di software testing hanno cercato di proporre approssimazioni per ragionare sulle espressioni simboliche. 

%QSYM ha introdotto il concetto di optimistic solving, che in caso di fallimento del solver nel ragionare entro il time budget su una query $!b \wedge \pi$, chiede al solver di ragionare solo su l'espressione $!b$, ignorando tutte le condizione presenti in $\pi$. Tale approccio ha dimostrato di essere efficace, in quanto in molti casi vincoli presenti in $\pi$ (ad esempio via di concretizzazioni), rendono la query completa non soddisfacibile, ma l'input usato dall'esecutore concolico per generare la query, opportunatamente modificato per render $!b$ soddisfacibile, porta ad ottenere input significativi per il programma.

A different direction is instead taken by \jfs~\cite{JFS}, which builds on the experimental observation that SMT solvers can struggle on queries that involve floating-point values. \jfs\ thus proposes to turn the query into a program, which is then analyzed using coverage-based grey-box fuzzing. More precisely, the constructed program has a point that is reachable if and only if the program's input satisfies the original query. The authors show that \jfs\ is quite effective on symbolic expressions involving floating-point values but it struggles on integer values when compared to traditional SMT solvers.

Two very recent works, {\sc Pangolin}~\cite{PANGOLIN-SP20} and {\sc Trident}~\cite{TRIDENT-ISSTA20}, devise techniques to reduce the solving time in CE. {\sc Pangolin} transforms constraints into a {\em polyhedral path abstraction}, modeling the solution space as a polyhedron and using, e.g., sampling to find assignments. {\sc Trident} instead exploits interval analysis to reduce the solution space in the SMT solver. Their implementations have not been released yet.

% reasoning on symbolic expressions models floating-point computations. Quindi, data un query simbolica di questa tipologia, la utilizza per generare un programma minimale che replica la computazione e utilizza un fuzzer tradizionale per ottenere possibilmente un input che soddisfa la query originale.

\iffalse
Our work shares some similarities with~\cite{10.1145/3338906.3338921}, which focuses on solving queries that involve floating-point values. The authors turn a formula into a program, which is then analyzed using coverage-guided fuzzing. More precisely, the constructed program has a point that is reachable if and only if the program's input satisfies the original formula. Conversely, we directly apply fuzzing to solving queries, mutating the content of symbolic values in a formula until it is satisfied, or a timeout occurs that is interpreted as unsatisfiability. 
\fi

\smallskip
{\bf Coverage-based grey-box fuzzing.} An orthogonal approach to SE is coverage-based grey-box fuzzing (CGF). Given an input queue $q$ (initialized with some input seeds) and a program $p$, CGF picks an input $i$ from $q$, randomly mutates some of its bytes to generate $i'$ and then runs $p$ over $i'$: if new code is executed (covered) by $p$ compared to previous runs on other inputs, then CGF deems the input {\em interesting} and adds it to $q$. This process is then repeated endlessly, looking for crashes and other errors during the program executions.

%Un approccio ortogonale a symbolic execution che sta avendo molto successo negli ultimi anni è coverage-guided grey-box fuzzing.  Idea di base: dato un seed, effettua delle mutazioni all'input, riesegue il programma: se programma crasha salva l'input, altrimenti se non crasha ma la code coverage è aumentata rispetto alle precedenti esecuzioni salva input, eventualmente continuando a mutarlo. 

American Fuzzy Lop (\afl)~\cite{AFL} is the most prominent example of CGF. %and several recent proposals have built on top of it~\cite{}. 
To track the coverage, it can dynamically instrument at runtime a binary or add source-based instrumentation at compilation time. The fuzzing process for each input is split into two main stages. In the first one, \afl\ scans the input and {\em deterministically} applies for each position a set of mutations, testing the effect of each mutation on the program execution in isolation. In the second stage, %dubbed {\em havoc}, 
\afl\ instead 
performs several mutations in sequence, i.e., {\em stacking} them, over the input, {\em non deterministically} choosing which mutations to apply and at which positions. The mutations in the two stages involve simple and fast to apply transformations such as flipping bits, adding or subtracting constants, removing  bytes, combining different inputs, and several others~\cite{AFL}. %Although, \afl\ has found thousands of bugs in the last years~\cite{}.

%American Fuzzy Lop (\afl) e' stato uno dei precursori di questo approccio, e per tracciare la coverage instrumenta dinamicamnte un binario via QEMU, o richiede di ricompilare il programma per effettura source instrumentation (ma garantisce un minor overhead a runtime). Il processo di fuzzing in AFL si divide in due stage: mutazioni determinstiche e mutazioni non deterministiche. Nel primo stage, AFL scansiona l'input e per ogni porzione di esso effettua un'insieme di mutazioni (es. ....), applicandone una sola per volta sull'input. Il secondo stage invece è pensato per applicare più mutazione contemporaneamente in cascata, scegliendo quali e dove applicarle in modo non deterministico.

\smallskip
{\bf Hybrid fuzzing.} Although CGF fuzzers have found thousands of bugs in the last years~\cite{aflsmart-tse,google-oss-fuzz}, there are still scenarios where  their mutation strategy is not effective. For instance, they may struggle on checks against magic numbers, whose value is unlikely to be generated with random mutations. As these checks may appear early in the %program 
execution, fuzzers may soon {\em get stuck} and stop producing interesting inputs. For this reason, a few works have explored combinations of fuzzing with symbolic execution, proposing {\em hybrid fuzzing}. {\sc Driller}~\cite{DRILLER-NDSS16} alternates \afl\ and \angr, temporarily switching to the latter when the former is unable to generate new interesting inputs for a specific budget of time. %, hoping that \angr\ is able to generate inputs that can help the fuzzer bypass complex checks. 
\qsym\ proposes instead to run a concolic executor in parallel with \afl, allowing the two components to share their input queues and continuously benefit from the work done by each other.  

%CGF e SE sono complementari tra loro, in quanto la prima tecnica risulta molto efficiente e scalabile ma inefficace in presenza branch condition complesse, mentre la seconda può ragionare anche su query complesse grazie ad un SMT solver ma risulta poco scalabile su real-world programs, sono state proposte diverse strategie di hydrid fuzzing, che vanno ad utilizzare entrambe le tecniche. DRILLER propone di alternare AFL e angr, attivando temporaneamente l'esecuzione simbolica (angr) solo in caso di stallo del fuzzer AFL, cercando di generare input in grado sbloccare branch complessi, e permettendo ad AFL di riprendere il processo di fuzzing concentrandosi su parti di codice a valle dei branch complessi. QSYM propone invece di eseguire le due tecniche in parallelo, affiancando ad AFL perennemente un esecutore concolico, permettendo ai due componenti di scambiarsi tra loro gli input generati.

\smallskip
{\bf Recent improvements in coverage-guided fuzzing.} During the last years, a large body of works has extended CGF, trying to make it more effective without resorting to heavyweight analyses such as symbolic execution. {\sc Laf-Intel}~\cite{lafintel} splits multi-byte checks into single-byte comparisons, helping the fuzzer track the intermediate progress when reasoning on a branch condition. {\sc Vuzzer}~\cite{vuzzer} integrates dynamic taint analysis (DTA)~\cite{debray-scam14} into the fuzzer to identify which bytes influence the operands in a branch condition, allowing it to bypass, e.g., checks on magic numbers. \angora~\cite{angora} further improves this idea by performing multi-byte DTA and using gradient descent to effectively mutate the tainted input bytes.

%. For instance, \aflsmart, \nautilus, and \grimoire proposed mutations that are aware of the input format processed by an application, while 

%Negli ultimi anni molti lavori hanno construito sulle spalle di AFL, cercando di apportare miglioramenti in grado di rendere il processo di fuzzing più efficace, senza richiedere l'utilizzo di una tecnica costosa come symbolic execution. LAF-Intel spezza multi-byte comparison in single-byte comparison, per aiutare il fuzzer a valutare il progresso intermedio su un branch. VUZZER ha proposto di utlizzare dynamic taint analysis (DTA) per identificare durante il processo di fuzzing quali parte dell'input influenzano gli operandi di una branch condition, permettendo di superare facilmente magic numbers e di poter focalizzare le mutazioni sui byte rilevanti dell'input. ANGORA migliora VUZZER, effettuando DTA in modo più accurato (ma richiede source-instrumentation) e utilizzando gradient descent per mutare in modo efficace i byte che influenzano una branch condition.

As DTA can still put a high burden on the fuzzing strategy, some works have recently explored lightweight approximate analyses that can replace it. \redqueen~\cite{redqueen} introduces the concept of {\em input-to-state correspondence}, which captures the idea that input bytes often flow directly, or after a few simple encodings (e.g., byte swapping), into comparison operands during the program execution. To detect this kind of input dependency, \redqueen\ uses {\em colorization} that inserts random bytes into the input and then checks whether some of these bytes appear, as is or after few simple transformations, in the comparison operands when running the program. %\rem{Drop sentence?}
Input-to-state relations can be exploited to devise effective mutations and bypass several kinds of validation checks.

%Essendo DTA una tecnica comunque costosa, alcuni lavori hanno recentemente proposto approssimazioni leggere di questa analisi. \redqueen\ utilizza una tecnica, chimata colorization, che inserendo random bytes all'interno dell'input e tracciando gli operandi delle branch condition, identifica una dipendenza tra un operando e una porzione di input se il valore dell'operando riflette (uguale o a valle di alcune comuni transformationi) i byte random inseriti in quella porzione di input. Tale dipendenze vengono definite input-to-state correspondence e sono utilizzate per effettuare mutazioni efficaci in \redqueen (es., per bypassare magic number). 

{\sc Weizz}~\cite{WEIZZ} explores instead a different approach that flips one bit at a time on the entire input, checking after each bit flip which comparison operands have changed during the program execution, possibly suggesting a dependency between the altered bit and the affected branch conditions. While more accurate than colorization, this approach may incur a large overhead, especially in presence of large inputs. % on which the bit flipping strategy can take a long time. 
%\rem{Drop sentence?}
Nonetheless, {\sc Weizz} is willing to pay this price as the technique allows it to also heuristically locate fields and chunks within an input, supporting {\em smart mutations}~\cite{aflsmart-tse} to effectively fuzz applications processing structured input formats.

%Weizz propone una tecnica alternativa, che invece di usare random byte, esegue bitflip sull'intero input osservano se e come gli operandi delle comparison sono impattati. Sebbene la tecnica sia più accurata di colorization, ha un costo superiore che tuttavia è giustificato in Weizz in quanto esso usa le informazioni sulle dipendenze anche per ragionare sull'input format usato da un'applicazione ed effettuare mutazioni in grado di generare input significative per il formato. 

\slf~\cite{SLF} exploits a bit flipping strategy similar to {\sc Weizz} to generate valid inputs for an application even when no meaningful seeds are initially available for it. Thanks to the input dependency analysis, \slf\ can identify fields into the input and then resort to a gradient-based multi-goal search heuristic to deal with interdependent checks in the program.

%L'idea di utilzzare bitflips è stata parallelamente anche esplorata da SLF per generare input significativi per un applicazione in assenza di seed iniziali. Esso utilizza informazioni sulle dipendenze per identificare validation checks di diverse categorie, proponendo mutazioni specializzate per ogni categoria. SLF inoltre propone una gradient-based multi goal search per gestire check interdipendenti. 

\eclipser~\cite{ECLIPSER-ICSE19} identifies a dependency between an input byte $i_k$ and a branch condition $b$ whenever the program decision on $b$ is affected when running the program on inputs containing different values for $i_k$. \eclipser\ builds approximate path constraints by modeling each branch condition met along the program execution as an interval. In particular, given a branch $b$, it generates a new input using a strategy similar to concolic execution, by looking for input values that satisfy the interval from $\neg b$ as well as any other interval from previous branches met along a path. %\rem{a bit too generic by the paper's standards}
To find input assignments, \eclipser\ does not use an SMT solver but resorts to lightweight techniques that work well in presence of intervals generated by linear or monotonic functions.

%Eclipser rileva dipendenze tra un input i\_k e una branch condition, valutando come cambia l'esito del branch al cambiare di i\_k. Eclipser sfrutta le informazioni sulle dipendenze per costruire un'approssimazione di $\pi$, defininendo per ogni byte dell'input un intervallo di validità e utilizzando una strategia simile ad un concolic executor per generare nuovi input. In particolare, sceglie una branch condition (ossia un intervallo) da negare e genera un input che rispetta sia l'intervalli del branch negato che gli intervalli definiti dalle condizioni presenti in $\pi$. Per costruire l'input non fa uso di SMT solver, ma usa tecniche lightweight che gestiscono constraint lineari o monotoni.





table-fuzzy-stats.tex
% !TEX root = paper.tex

\begin{table}[t]
  \centering
  \caption{Effectiveness of the different mutations from \fuzzysat: I2S (Input-to-State), BF (R.I. Brute Force), IC (Interesting Constants), GD (Gradient Descent), D+ND (Deterministic and Non-Deterministic mutations), MGS (Multi-Goal Strategy).\label{tab:fuzzy-mutations-stats}} % 
  \vspace{-1.5mm}
  \begin{adjustbox}{width=0.88\columnwidth,center}
  %\small
  \begin{tabular}{ |l||c|c|c|c|c|c| }
    \hline
    {\sc Program} 
    & {\sc I2S}
    & {\sc BF} 
    & {\sc IC}  
    & {\sc GD}
    & {\sc D+ND}
    & {\sc MGS}
    \\\hline\hline

advmng & 176 & 31 & 74 & 2 & 18 & 0 \\ 
bloaty & 43 & 5 & 20 & 5 & 19 & 4 \\ 
bsdtar & 14 & 8 & 11 & 0 & 0 & 91 \\ 
djpeg & 98 & 29 & 28 & 6 & 14 & 25 \\ 
jhead & 27 & 5 & 41 & 6 & 8 & 0 \\ 
libpng & 14 & 8 & 7 & 1 & 1 & 0 \\ 
lodepng & 61 & 6 & 16 & 1 & 21 & 0 \\ 
objdump & 91 & 21 & 18 & 1 & 10 & 5 \\ 
optipng & 28 & 7 & 6 & 0 & 1 & 0 \\ 
readelf & 96 & 10 & 22 & 0 & 22 & 0 \\ 
tcpdump & 28 & 7 & 11 & 1 & 11 & 29 \\ 
tiff2pdf & 107 & 25 & 6 & 0 & 2 & 24 \\ 

\hline\hline

{\sc Perc. on total} & 51.04\% & 10.56\% & 17.01\% & 1.50\% & 8.28\% & 11.60\% \\

    \hline
  \end{tabular}
  \end{adjustbox}
\end{table}
table-fuzzy-vs-z3.tex
% !TEX root = paper.tex

\begin{table}[t]
  \centering
  \caption{Number of queries proved satisfiable by \fuzzysat\ w.r.t. {\sc Z3} (timeout 10 secs). Numbers show the average of 5 runs. The speedup considers the solving time on the full set of  queries. \label{tab:z3-vs-fuzzy}} % 
  \vspace{-1.5mm}
  \begin{adjustbox}{width=0.97\columnwidth,center}
  %\small
  \begin{tabular}{ |l||c|c|c|c|c||c| }
    \hline
    \multirow{2}{*}{{\sc Program}} 
    & {\sc \#}%\multirow{2}{*}{{\sc \# queries}} 
    & \multicolumn{3}{c|}{{\sc \# queries proved SAT by}} 
    & {\sc \# SAT \fuzzysat}  
    & {\sc Solv. Time}
    \\\cline{3-5}

    & {\sc queries} 
    & {\sc both} & {\sc Z3} & {\sc } \fuzzysat 
    & {\sc Div. by \# SAT Z3} 
    & {\sc Speedup}\\
    \hline\hline

advmng & 1481 & 236.7 & +7.0 & +64.3 & 1.24 & 17.1$\times$ \\ 
bloaty & 2085 & 95.0 & +7.0 & +1.0 & 0.94 & 47.8$\times$ \\ 
bsdtar & 325 & 124.0 & +6.0 & 0 & 0.95 & 1.8$\times$ \\ 
djpeg & 1245 & 189.0 & +6.0 & +11.0 & 1.03 & 34.3$\times$ \\ 
jhead & 405 & 88.0 & 0 & 0 & 1.00 & 21.7$\times$ \\ 
libpng & 1673 & 31.0 & 0 & 0 & 1.00 & 70.9$\times$ \\ 
lodepng & 1531 & 100.3 & +6.3 & +4.7 & 0.98 & 75.6$\times$ \\ 
objdump & 992 & 146.0 & +4.0 & 0 & 0.97 & 30.6$\times$ \\ 
optipng & 1740 & 42.0 & 0 & 0 & 1.00 & 67.3$\times$ \\ 
readelf & 1055 & 150.0 & +8.0 & 0 & 0.95 & 69.5$\times$ \\ 
tcpdump & 409 & 58.3 & +9.7 & +28.7 & 1.28 & 37.3$\times$ \\ 
tiff2pdf & 3084 & 164.0 & +9.0 & 0 & 0.95 & 28.1$\times$ \\ 

\hline\hline

{\sc G. Mean} & 1335.4 & 118.7 & +5.3 & +9.1 & 1.02 & 31.2$\times$ \\ 

    \hline
  \end{tabular}
  \end{adjustbox}
\end{table}
table-lava-m.tex
% !TEX root = paper.tex

\begin{table}[t]
  \vspace{-3mm}
  \centering
  \caption{Bugs found %by QSYM 
  on LAVA-M in 5H: avg (max) number over 5 runs.
  \label{tab:fuzzy-lava-m}} % 
  \vspace{-2mm}
  \begin{adjustbox}{width=0.85\columnwidth,center}
  %\small
  \begin{tabular}{ |l||c|c|c|c| }
    \hline
    %{\sc Avg} ({\sc Max})
    &
    base64 &
    md5sum &
    uniq &
    who
    \\
    \hline
    {\sc QSYM with Z3} & 48 (48) & 58 (58) & 19 (29) &  743 (795) \\
    {\sc QSYM with Fuzzy-Sat} & 48 (48) & 61 (61) & 19.7 (29) & 2256.5 (2268) \\
    \hline 
  \end{tabular}
  \end{adjustbox}
\end{table}
IEEEabrv.bib

IEEEabrv.bib
V1.12 (2007/01/11)
Copyright (c) 2002-2007 by Michael Shell
See: http://www.michaelshell.org/
for current contact information.

BibTeX bibliography string definitions of the ABBREVIATED titles of
IEEE journals and magazines and online publications.

This file is designed for bibliography styles that require 
abbreviated titles and is not for use in bibliographies that
require full-length titles.

Support sites:
http://www.michaelshell.org/tex/ieeetran/
http://www.ctan.org/tex-archive/macros/latex/contrib/IEEEtran/
and/or
http://www.ieee.org/

Special thanks to Laura Hyslop and ken Rawson of IEEE for their help
in obtaining the information needed to compile this file. Also,
Volker Kuhlmann and Moritz Borgmann kindly provided some corrections
and additions.

*************************************************************************
Legal Notice:
This code is offered as-is without any warranty either expressed or
implied; without even the implied warranty of MERCHANTABILITY or
FITNESS FOR A PARTICULAR PURPOSE! 
User assumes all risk.
In no event shall IEEE or any contributor to this code be liable for
any damages or losses, including, but not limited to, incidental,
consequential, or any other damages, resulting from the use or misuse
of any information contained here.

All comments are the opinions of their respective authors and are not
necessarily endorsed by the IEEE.

This work is distributed under the LaTeX Project Public License (LPPL)
( http://www.latex-project.org/ ) version 1.3, and may be freely used,
distributed and modified. A copy of the LPPL, version 1.3, is included
in the base LaTeX documentation of all distributions of LaTeX released
2003/12/01 or later.
Retain all contribution notices and credits.
** Modified files should be clearly indicated as such, including  **
** renaming them and changing author support contact information. **

File list of work: IEEEabrv.bib, IEEEfull.bib, IEEEexample.bib,
                   IEEEtran.bst, IEEEtranS.bst, IEEEtranSA.bst,
                   IEEEtranN.bst, IEEEtranSN.bst, IEEEtran_bst_HOWTO.pdf
*************************************************************************


USAGE:

\bibliographystyle{mybstfile}
\bibliography{IEEEabrv,mybibfile}

where the IEEE titles in the .bib database entries use the strings
defined here. e.g.,


   journal = IEEE_J_AC,


to yield "{IEEE} Trans. Automat. Contr."


IEEE uses abbreviated journal titles in their bibliographies -
this file is suitable for work that is to be submitted to the IEEE.


For work that requires full-length titles, you should use the full
titles provided in the companion file, IEEEfull.bib.


** NOTES **

 1. Journals have been grouped according to subject in order to make it
    easier to locate and extract the definitions for related journals - 
    as most works use references that are confined to a single topic.
    Magazines are listed in straight alphabetical order.

 2. String names are closely based on IEEE's own internal acronyms.
 
 3. Abbreviations follow IEEE's style.

 4. Older, out-of-print IEEE titles are included (but not including titles
    dating prior to IEEE's formation from the IRE and AIEE in 1963).

 5. The following NEW/current journal definitions have been disabled because
    their abbreviations have not yet been verified:
    
    STRING{IEEE_J_CBB        = "{IEEE/ACM} Trans. Comput. Biology Bioinformatics"}
    STRING{IEEE_J_CJECE      = "Canadian J. Elect. Comput. Eng."}
    STRING{IEEE_J_DSC        = "{IEEE} Trans. Dependable Secure Comput."}
    STRING{IEEE_O_DSO        = "{IEEE} Distrib. Syst. Online"}
    
 6. The following OLD journal definitions have been disabled because
    their abbreviations have not yet been found/verified:

    STRING{IEEE_J_BCTV       = "{IEEE} Trans. Broadcast Television Receivers"}
    STRING{IEEE_J_EWS        = "{IEEE} Trans. Eng. Writing Speech"}

If you know what the proper abbreviation is for a string in #5 or #6 above,
email me and I will correct them in the next release.





IEEE Journals 



aerospace and military
@STRING{IEEE_J_AES        = "{IEEE} Trans. Aerosp. Electron. Syst."}
@STRING{IEEE_J_ANE        = "{IEEE} Trans. Aerosp. Navig. Electron."}
@STRING{IEEE_J_ANNE       = "{IEEE} Trans. Aeronaut. Navig. Electron."}
@STRING{IEEE_J_AS         = "{IEEE} Trans. Aerosp."}
@STRING{IEEE_J_AIRE       = "{IEEE} Trans. Airborne Electron."}
@STRING{IEEE_J_MIL        = "{IEEE} Trans. Mil. Electron."}



autos, transportation and vehicles (non-aerospace)
@STRING{IEEE_J_ITS        = "{IEEE} Trans. Intell. Transp. Syst."}
@STRING{IEEE_J_VT         = "{IEEE} Trans. Veh. Technol."}
@STRING{IEEE_J_VC         = "{IEEE} Trans. Veh. Commun."}



circuits, signals, systems, audio and controls
@STRING{IEEE_J_SPL        = "{IEEE} Signal Process. Lett."}
@STRING{IEEE_J_ASSP       = "{IEEE} Trans. Acoust., Speech, Signal Process."}
@STRING{IEEE_J_AU         = "{IEEE} Trans. Audio"}
@STRING{IEEE_J_AUEA       = "{IEEE} Trans. Audio Electroacoust."}
@STRING{IEEE_J_AC         = "{IEEE} Trans. Autom. Control"}
@STRING{IEEE_J_CAS        = "{IEEE} Trans. Circuits Syst."}
@STRING{IEEE_J_CASVT      = "{IEEE} Trans. Circuits Syst. Video Technol."}
@STRING{IEEE_J_CASI       = "{IEEE} Trans. Circuits Syst. {I}"}
@STRING{IEEE_J_CASII      = "{IEEE} Trans. Circuits Syst. {II}"}
in 2004 CASI and CASII renamed part title to CASI_RP and CASII_EB, respectively.
@STRING{IEEE_J_CASI_RP    = "{IEEE} Trans. Circuits Syst. {I}"}
@STRING{IEEE_J_CASII_EB   = "{IEEE} Trans. Circuits Syst. {II}"}
@STRING{IEEE_J_CT         = "{IEEE} Trans. Circuit Theory"}
@STRING{IEEE_J_CST        = "{IEEE} Trans. Control Syst. Technol."}
@STRING{IEEE_J_SP         = "{IEEE} Trans. Signal Process."}
@STRING{IEEE_J_SU         = "{IEEE} Trans. Sonics Ultrason."}
@STRING{IEEE_J_SAP        = "{IEEE} Trans. Speech Audio Process."}
@STRING{IEEE_J_UE         = "{IEEE} Trans. Ultrason. Eng."}
@STRING{IEEE_J_UFFC       = "{IEEE} Trans. Ultrason., Ferroelectr., Freq. Control"}



communications
@STRING{IEEE_J_COML       = "{IEEE} Commun. Lett."}
@STRING{IEEE_J_JSAC       = "{IEEE} J. Sel. Areas Commun."}
@STRING{IEEE_J_COM        = "{IEEE} Trans. Commun."}
@STRING{IEEE_J_COMT       = "{IEEE} Trans. Commun. Technol."}
@STRING{IEEE_J_WCOM       = "{IEEE} Trans. Wireless Commun."}



components, packaging and manufacturing
@STRING{IEEE_J_ADVP       = "{IEEE} Trans. Adv. Packag."}
@STRING{IEEE_J_CHMT       = "{IEEE} Trans. Compon., Hybrids, Manuf. Technol."}
@STRING{IEEE_J_CPMTA      = "{IEEE} Trans. Compon., Packag., Manuf. Technol. {A}"}
@STRING{IEEE_J_CPMTB      = "{IEEE} Trans. Compon., Packag., Manuf. Technol. {B}"}
@STRING{IEEE_J_CPMTC      = "{IEEE} Trans. Compon., Packag., Manuf. Technol. {C}"}
@STRING{IEEE_J_CAPT       = "{IEEE} Trans. Compon. Packag. Technol."}
@STRING{IEEE_J_CAPTS      = "{IEEE} Trans. Compon. Packag. Technol."}
@STRING{IEEE_J_CPART      = "{IEEE} Trans. Compon. Parts"}
@STRING{IEEE_J_EPM        = "{IEEE} Trans. Electron. Packag. Manuf."}
@STRING{IEEE_J_MFT        = "{IEEE} Trans. Manuf. Technol."}
@STRING{IEEE_J_PHP        = "{IEEE} Trans. Parts, Hybrids, Packag."}
@STRING{IEEE_J_PMP        = "{IEEE} Trans. Parts, Mater., Packag."}



CAD
@STRING{IEEE_J_TCAD       = "{IEEE} J. Technol. Comput. Aided Design"}
@STRING{IEEE_J_CAD        = "{IEEE} Trans. Comput.-Aided Design Integr. Circuits Syst."}



coding, data, information, knowledge
@STRING{IEEE_J_IT         = "{IEEE} Trans. Inf. Theory"}
@STRING{IEEE_J_KDE        = "{IEEE} Trans. Knowl. Data Eng."}



computers, computation, networking and software
@STRING{IEEE_J_C          = "{IEEE} Trans. Comput."}
@STRING{IEEE_J_CAL        = "{IEEE} Comput. Archit. Lett."}
disabled till definition is verified
STRING{IEEE_J_DSC         = "{IEEE} Trans. Dependable Secure Comput."}
@STRING{IEEE_J_ECOMP      = "{IEEE} Trans. Electron. Comput."}
@STRING{IEEE_J_EVC        = "{IEEE} Trans. Evol. Comput."}
@STRING{IEEE_J_FUZZ       = "{IEEE} Trans. Fuzzy Syst."}
@STRING{IEEE_J_IFS        = "{IEEE} Trans. Inf. Forensics Security"}
@STRING{IEEE_J_MC         = "{IEEE} Trans. Mobile Comput."}
@STRING{IEEE_J_NET        = "{IEEE/ACM} Trans. Netw."}
@STRING{IEEE_J_NN         = "{IEEE} Trans. Neural Netw."}
@STRING{IEEE_J_PDS        = "{IEEE} Trans. Parallel Distrib. Syst."}
@STRING{IEEE_J_SE         = "{IEEE} Trans. Softw. Eng."}



computer graphics, imaging, and multimedia
@STRING{IEEE_J_JDT        = "{IEEE/OSA} J. Display Technol."}
@STRING{IEEE_J_IP         = "{IEEE} Trans. Image Process."}
@STRING{IEEE_J_MM         = "{IEEE} Trans. Multimedia"}
@STRING{IEEE_J_VCG        = "{IEEE} Trans. Vis. Comput. Graphics"}



cybernetics, ergonomics, robots, man-machine, and automation
@STRING{IEEE_J_ASE        = "{IEEE} Trans. Autom. Sci. Eng."}
@STRING{IEEE_J_JRA        = "{IEEE} J. Robot. Autom."}
@STRING{IEEE_J_HFE        = "{IEEE} Trans. Hum. Factors Electron."}
@STRING{IEEE_J_MMS        = "{IEEE} Trans. Man-Mach. Syst."}
@STRING{IEEE_J_PAMI       = "{IEEE} Trans. Pattern Anal. Mach. Intell."}
in 1989 JRA became RA
in August 2004, RA split into ASE and RO
@STRING{IEEE_J_RA         = "{IEEE} Trans. Robot. Autom."}
@STRING{IEEE_J_RO         = "{IEEE} Trans. Robot."}
@STRING{IEEE_J_SMC        = "{IEEE} Trans. Syst., Man, Cybern."}
@STRING{IEEE_J_SMCA       = "{IEEE} Trans. Syst., Man, Cybern. {A}"}
@STRING{IEEE_J_SMCB       = "{IEEE} Trans. Syst., Man, Cybern. {B}"}
@STRING{IEEE_J_SMCC       = "{IEEE} Trans. Syst., Man, Cybern. {C}"}
@STRING{IEEE_J_SSC        = "{IEEE} Trans. Syst. Sci. Cybern."}



earth, wind, fire and water
@STRING{IEEE_J_GE         = "{IEEE} Trans. Geosci. Electron."}
@STRING{IEEE_J_GRS        = "{IEEE} Trans. Geosci. Remote Sens."}
@STRING{IEEE_J_GRSL       = "{IEEE} Geosci. Remote Sens. Lett."}
@STRING{IEEE_J_OE         = "{IEEE} J. Ocean. Eng."}



education, engineering, history, IEEE, professional
disabled till definition is verified
STRING{IEEE_J_CJECE       = "Canadian J. Elect. Comput. Eng."}
@STRING{IEEE_J_PROC       = "Proc. {IEEE}"}
@STRING{IEEE_J_EDU        = "{IEEE} Trans. Educ."}
@STRING{IEEE_J_EM         = "{IEEE} Trans. Eng. Manag."}
disabled till definition is verified
STRING{IEEE_J_EWS         = "{IEEE} Trans. Eng. Writing Speech"}
@STRING{IEEE_J_PC         = "{IEEE} Trans. Prof. Commun."}



electromagnetics, antennas, EMI, magnetics and microwave
@STRING{IEEE_J_AWPL       = "{IEEE} Antennas Wireless Propag. Lett."}
@STRING{IEEE_J_MGWL       = "{IEEE} Microw. Guided Wave Lett."}
IEEE seems to want "Compon." here, not "Comp."
@STRING{IEEE_J_MWCL       = "{IEEE} Microw. Wireless Compon. Lett."}
@STRING{IEEE_J_AP         = "{IEEE} Trans. Antennas Propag."}
@STRING{IEEE_J_EMC        = "{IEEE} Trans. Electromagn. Compat."}
@STRING{IEEE_J_MAG        = "{IEEE} Trans. Magn."}
@STRING{IEEE_J_MTT        = "{IEEE} Trans. Microw. Theory Tech."}
@STRING{IEEE_J_RFI        = "{IEEE} Trans. Radio Freq. Interference"}
@STRING{IEEE_J_TJMJ       = "{IEEE} Transl. J. Magn. Jpn."}



energy and power
@STRING{IEEE_J_EC         = "{IEEE} Trans. Energy Convers."}
@STRING{IEEE_J_PEL        = "{IEEE} Power Electron. Lett."}
@STRING{IEEE_J_PWRAS      = "{IEEE} Trans. Power App. Syst."}
@STRING{IEEE_J_PWRD       = "{IEEE} Trans. Power Del."}
@STRING{IEEE_J_PWRE       = "{IEEE} Trans. Power Electron."}
@STRING{IEEE_J_PWRS       = "{IEEE} Trans. Power Syst."}



industrial, commercial and consumer
@STRING{IEEE_J_APPIND     = "{IEEE} Trans. Appl. Ind."}
@STRING{IEEE_J_BC         = "{IEEE} Trans. Broadcast."}
disabled till definition is verified
STRING{IEEE_J_BCTV        = "{IEEE} Trans. Broadcast Television Receivers"}
@STRING{IEEE_J_CE         = "{IEEE} Trans. Consum. Electron."}
@STRING{IEEE_J_IE         = "{IEEE} Trans. Ind. Electron."}
@STRING{IEEE_J_IECI       = "{IEEE} Trans. Ind. Electron. Contr. Instrum."}
@STRING{IEEE_J_IA         = "{IEEE} Trans. Ind. Appl."}
@STRING{IEEE_J_IGA        = "{IEEE} Trans. Ind. Gen. Appl."}
@STRING{IEEE_J_IINF       = "{IEEE} Trans. Ind. Informat."}
@STRING{IEEE_J_PSE        = "{IEEE} J. Product Safety Eng."}



instrumentation and measurement
@STRING{IEEE_J_IM         = "{IEEE} Trans. Instrum. Meas."}



insulation and materials
@STRING{IEEE_J_JEM        = "{IEEE/TMS} J. Electron. Mater."}
@STRING{IEEE_J_DEI        = "{IEEE} Trans. Dielectr. Electr. Insul."}
@STRING{IEEE_J_EI         = "{IEEE} Trans. Electr. Insul."}



mechanical
@STRING{IEEE_J_MECH       = "{IEEE/ASME} Trans. Mechatronics"}
@STRING{IEEE_J_MEMS       = "J. Microelectromech. Syst."}



medical and biological
@STRING{IEEE_J_BME        = "{IEEE} Trans. Biomed. Eng."}
Note: The B-ME journal later dropped the hyphen and became the BME.
@STRING{IEEE_J_B-ME       = "{IEEE} Trans. Bio-Med. Eng."}
@STRING{IEEE_J_BMELC      = "{IEEE} Trans. Bio-Med. Electron."}
disabled till definition is verified
STRING{IEEE_J_CBB         = "{IEEE/ACM} Trans. Comput. Biology Bioinformatics"}
@STRING{IEEE_J_ITBM       = "{IEEE} Trans. Inf. Technol. Biomed."}
@STRING{IEEE_J_ME         = "{IEEE} Trans. Med. Electron."}
@STRING{IEEE_J_MI         = "{IEEE} Trans. Med. Imag."}
@STRING{IEEE_J_NB         = "{IEEE} Trans. Nanobiosci."}
@STRING{IEEE_J_NSRE       = "{IEEE} Trans. Neural Syst. Rehabil. Eng."}
@STRING{IEEE_J_RE         = "{IEEE} Trans. Rehabil. Eng."}



 optics, lightwave and photonics
@STRING{IEEE_J_PTL        = "{IEEE} Photon. Technol. Lett."}
@STRING{IEEE_J_JLT        = "J. Lightw. Technol."}



physics, electrons, nanotechnology, nuclear and quantum electronics
@STRING{IEEE_J_EDL        = "{IEEE} Electron Device Lett."}
@STRING{IEEE_J_JQE        = "{IEEE} J. Quantum Electron."}
@STRING{IEEE_J_JSTQE      = "{IEEE} J. Sel. Topics Quantum Electron."}
@STRING{IEEE_J_ED         = "{IEEE} Trans. Electron Devices"}
@STRING{IEEE_J_NANO       = "{IEEE} Trans. Nanotechnol."}
@STRING{IEEE_J_NS         = "{IEEE} Trans. Nucl. Sci."}
@STRING{IEEE_J_PS         = "{IEEE} Trans. Plasma Sci."}



reliability
IEEE seems to want "Mat." here, not "Mater."
@STRING{IEEE_J_DMR        = "{IEEE} Trans. Device Mater. Rel."}
@STRING{IEEE_J_R          = "{IEEE} Trans. Rel."}



semiconductors, superconductors, electrochemical and solid state
@STRING{IEEE_J_ESSL       = "{IEEE/ECS} Electrochem. Solid-State Lett."}
@STRING{IEEE_J_JSSC       = "{IEEE} J. Solid-State Circuits"}
@STRING{IEEE_J_ASC        = "{IEEE} Trans. Appl. Supercond."}
@STRING{IEEE_J_SM         = "{IEEE} Trans. Semicond. Manuf."}



sensors
@STRING{IEEE_J_SENSOR     = "{IEEE} Sensors J."}



VLSI
@STRING{IEEE_J_VLSI       = "{IEEE} Trans. {VLSI} Syst."}






IEEE Magazines 



@STRING{IEEE_M_AES        = "{IEEE} Aerosp. Electron. Syst. Mag."}
@STRING{IEEE_M_HIST       = "{IEEE} Ann. Hist. Comput."}
@STRING{IEEE_M_AP         = "{IEEE} Antennas Propag. Mag."}
@STRING{IEEE_M_ASSP       = "{IEEE} {ASSP} Mag."}
@STRING{IEEE_M_CD         = "{IEEE} Circuits Devices Mag."}
@STRING{IEEE_M_CAS        = "{IEEE} Circuits Syst. Mag."}
@STRING{IEEE_M_COM        = "{IEEE} Commun. Mag."}
@STRING{IEEE_M_COMSOC     = "{IEEE} Commun. Soc. Mag."}
@STRING{IEEE_M_CIM        = "{IEEE} Comput. Intell. Mag."}
CSEM changed to CSE in 1999
@STRING{IEEE_M_CSE        = "{IEEE} Comput. Sci. Eng."}
@STRING{IEEE_M_CSEM       = "{IEEE} Comput. Sci. Eng. Mag."}
@STRING{IEEE_M_C          = "{IEEE} Computer"}
@STRING{IEEE_M_CAP        = "{IEEE} Comput. Appl. Power"}
@STRING{IEEE_M_CGA        = "{IEEE} Comput. Graph. Appl."}
@STRING{IEEE_M_CONC       = "{IEEE} Concurrency"}
@STRING{IEEE_M_CS         = "{IEEE} Control Syst. Mag."}
@STRING{IEEE_M_DTC        = "{IEEE} Des. Test. Comput."}
@STRING{IEEE_M_EI         = "{IEEE} Electr. Insul. Mag."}
@STRING{IEEE_M_ETR        = "{IEEE} ElectroTechnol. Rev."}
@STRING{IEEE_M_EMB        = "{IEEE} Eng. Med. Biol. Mag."}
@STRING{IEEE_M_EMR        = "{IEEE} Eng. Manag. Rev."}
@STRING{IEEE_M_EXP        = "{IEEE} Expert"}
@STRING{IEEE_M_IA         = "{IEEE} Ind. Appl. Mag."}
@STRING{IEEE_M_IM         = "{IEEE} Instrum. Meas. Mag."}
@STRING{IEEE_M_IS         = "{IEEE} Intell. Syst."}
@STRING{IEEE_M_IC         = "{IEEE} Internet Comput."}
@STRING{IEEE_M_ITP        = "{IEEE} {IT} Prof."}
@STRING{IEEE_M_MICRO      = "{IEEE} Micro"}
@STRING{IEEE_M_MW         = "{IEEE} Microw. Mag."}
@STRING{IEEE_M_MM         = "{IEEE} Multimedia"}
@STRING{IEEE_M_NET        = "{IEEE} Netw."}
IEEE's editorial manual lists "Pers. Commun.", 
but "Personal Commun. Mag." seems to be what is used in the journals
@STRING{IEEE_M_PCOM       = "{IEEE} Personal Commun. Mag."}
@STRING{IEEE_M_POT        = "{IEEE} Potentials"}
CAP and PER merged to form PE in 2003
@STRING{IEEE_M_PE         = "{IEEE} Power Energy Mag."}
@STRING{IEEE_M_PER        = "{IEEE} Power Eng. Rev."}
@STRING{IEEE_M_PVC        = "{IEEE} Pervasive Comput."}
@STRING{IEEE_M_RA         = "{IEEE} Robot. Autom. Mag."}
@STRING{IEEE_M_SAP        = "{IEEE} Security Privacy"}
@STRING{IEEE_M_SP         = "{IEEE} Signal Process. Mag."}
@STRING{IEEE_M_S          = "{IEEE} Softw."}
@STRING{IEEE_M_SPECT      = "{IEEE} Spectr."}
@STRING{IEEE_M_TS         = "{IEEE} Technol. Soc. Mag."}
@STRING{IEEE_M_VT         = "{IEEE} Veh. Technol. Mag."}
@STRING{IEEE_M_WC         = "{IEEE} Wireless Commun. Mag."}
@STRING{IEEE_M_TODAY      = "Today's Engineer"}






IEEE Online Publications 



@STRING{IEEE_O_CSTO        = "{IEEE} Commun. Surveys Tuts."}
disabled till definition is verified
STRING{IEEE_O_DSO          = "{IEEE} Distrib. Syst. Online"}





--
EOF

mybibfile.bib
@inproceedings{JFS,
author = {Liew, Daniel and Cadar, Cristian and Donaldson, Alastair F. and Stinnett, J. Ryan},
title = {Just Fuzz It: Solving Floating-Point Constraints Using Coverage-Guided Fuzzing},
year = {2019},
isbn = {9781450355728},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3338906.3338921},
doi = {10.1145/3338906.3338921},
booktitle = {Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering},
pages = {521–532},
numpages = {12},
keywords = {Constraint solving, feedback-directed fuzzing},
location = {Tallinn, Estonia},
series = {ESEC/FSE 2019}
}
  

@inbook{Barrett2018,
	author="Barrett, Clark and Tinelli, Cesare",
	editor="Clarke, Edmund M. and Henzinger, Thomas A. and Veith, Helmut 	and Bloem, Roderick",
	title="Satisfiability Modulo Theories",
	bookTitle="Handbook of Model Checking",
	year="2018",
	publisher="Springer International Publishing",
	pages="305--343",
	isbn="978-3-319-10575-8",
	doi="10.1007/978-3-319-10575-8_11",
}

@article{Jihyun12,
author = {Lee, Jihyun and Kang, Sungwon and Lee, D.},
year = {2012},
month = {06},
pages = {275-282},
title = {Survey on software testing practices},
volume = {6},
journal = {Software, IET},
doi = {10.1049/iet-sen.2011.0066}
}

@inproceedings{SYMCC-old,
  TITLE = {{Symbolic execution with SymCC: Don't interpret, compile!}},
  AUTHOR = {Poeplau, Sebastian and Francillon, Aur{\'e}lien},
  URL = {https://hal.inria.fr/hal-02874078},
  BOOKTITLE = {{USENIX Security Symposium 2020}},
  ADDRESS = {Boston, United States},
  YEAR = {2020},
  MONTH = Aug,
  HAL_ID = {hal-02874078},
  HAL_VERSION = {v1},
}

@inproceedings {SYMCC,
author = {Sebastian Poeplau and Aur{\'e}lien Francillon},
title = {Symbolic execution with SymCC: Don{\textquoteright}t interpret, compile!},
booktitle = {Proceedings of the 29th {USENIX} Security Symposium ({USENIX} Security 20)},
year = {2020},
isbn = {978-1-939133-17-5},
pages = {181--198},
url = {https://www.usenix.org/conference/usenixsecurity20/presentation/poeplau},
publisher = {{USENIX} Association},
month = aug,
}


@inproceedings{WEIZZ,
     author = {Fioraldi, Andrea and D'Elia, Daniele Cono and Coppa, Emilio},
     title= {{WEIZZ: Automatic Grey-Box Fuzzing for Structured Binary Formats}},
     booktitle = {Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA ’20)},
     year = {2020},
     doi = {10.1145/3395363.3397372},
     url = {https://doi.org/10.1145/3395363.3397372},
}

@inproceedings{tupni,
 author = {Cui, Weidong and Peinado, Marcus and Chen, Karl and Wang, Helen J. and Irun-Briz, Luis},
 title = {Tupni: Automatic Reverse Engineering of Input Formats},
 booktitle = {Proceedings of the 15th ACM Conference on Computer and Communications Security},
 series = {CCS '08},
 year = {2008},
 isbn = {978-1-59593-810-7},
 old_location = {Alexandria, Virginia, USA},
 pages = {391--402},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1455770.1455820},
 doi = {10.1145/1455770.1455820},
 acmid = {1455820},
 old_publisher = {ACM},
 old_address = {New York, NY, USA},
 keywords = {binary analysis, protocol reverse engineering},
}

@inproceedings{zeller-dta,
 author = {H\"{o}schele, Matthias and Zeller, Andreas},
 title = {Mining Input Grammars from Dynamic Taints},
 booktitle = {Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering},
 series = {ASE 2016},
 year = {2016},
 isbn = {978-1-4503-3845-5},
 old_location = {Singapore, Singapore},
 pages = {720--725},
 numpages = {6},
 url = {http://doi.acm.org/10.1145/2970276.2970321},
 doi = {10.1145/2970276.2970321},
 old_acmid = {2970321},
 old_publisher = {ACM},
 old_address = {New York, NY, USA},
 keywords = {Input formats, context-free grammars, dynamic tainting, fuzzing},
} 
 
@inproceedings{autogram,
 author = {H\"{o}schel{e}, Matthias and Zeller, Andreas},
 title = {Mining Input Grammars with {AUTOGRAM}},
 booktitle = {Proceedings of the 39th International Conference on Software Engineering Companion},
 series = {ICSE-C '17},
 year = {2017},
 isbn = {978-1-5386-1589-8},
 old_location = {Buenos Aires, Argentina},
 pages = {31--34},
 numpages = {4},
 url = {https://doi.org/10.1109/ICSE-C.2017.14},
 doi = {10.1109/ICSE-C.2017.14},
 old_acmid = {3098355},
 old_publisher = {IEEE Press},
 old_address = {Piscataway, NJ, USA},
 keywords = {context-free grammars, dynamic tainting, fuzzing, input formats},
} 
[

@inproceedings{Bellard:2005:QFP:1247360.1247401,
 author = {Bellard, Fabrice},
 title = {QEMU, a Fast and Portable Dynamic Translator},
 booktitle = {Proceedings of the Annual Conference on USENIX Annual Technical Conference},
 series = {ATEC '05},
 year = {2005},
 location = {Anaheim, CA},
 pages = {41--41},
 numpages = {1},
 url = {http://dl.acm.org/citation.cfm?id=1247360.1247401},
 acmid = {1247401},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 

@misc{qemu_tcg,
  title = {{Tiny Code Generator (TCG)}},
  howpublished = "\url{https://wiki.qemu.org/Documentation/TCG}",
  year = {2019}, 
  note = "[Online; accessed 10-Sep-2019]"
}

@article{hcct-spe16,
 author = {D'Elia, Daniele Cono and Demetrescu, Camil and Finocchi, Irene},
 title = {Mining Hot Calling Contexts in Small Space},
 journal = {Software: Practice and Experience},
 old_issue_date = {August 2016},
 volume = {46},
 old_number = {8},
 old_month = aug,
 year = {2016},
 issn = {0038-0644},
 pages = {1131--1152},
 numpages = {22},
 url = {https://doi.org/10.1002/spe.2348},
 doi = {10.1002/spe.2348},
 acmid = {3035090},
 publisher = {John Wiley \& Sons, Inc.},
 address = {New York, NY, USA},
 keywords = {data streaming algorithms, dynamic program analysis, frequent items, performance profiling, program instrumentation},
} 


% Related

@misc{afl,
  author = {Micha{\l} Zalewski},
  title = {{American Fuzzy Lop}},
  howpublished = "\url{https://github.com/Google/AFL}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@inproceedings{stephens2016driller,
	title={Driller: Augmenting Fuzzing Through Selective Symbolic Execution.},
	author={Stephens, Nick and Grosen, John and Salls, Christopher and Dutcher, Audrey and Wang, Ruoyu and Corbetta, Jacopo and Shoshitaishvili, Yan and Kruegel, Christopher and Vigna, Giovanni},
	booktitle={Proceeings of the 23th Annual Network and Distributed System Security Symposium, {NDSS}},
	old_volume={16},
	old_pages={1--16},
	year={2016},
  url={https://www.ndss-symposium.org/wp-content/uploads/2017/09/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf}
}

@inproceedings{QSYM,
 author = {Yun, Insu and Lee, Sangho and Xu, Meng and Jang, Yeongjin and Kim, Taesoo},
 title = {{QSYM}: A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing},
 booktitle = {Proceedings of the 27th USENIX Conference on Security Symposium},
 series = {SEC'18},
 year = {2018},
 isbn = {978-1-931971-46-1},
 old_location = {Baltimore, MD, USA},
 pages = {745--761},
 numpages = {17},
 url = {http://dl.acm.org/citation.cfm?id=3277203.3277260},
 old_acmid = {3277260},
 old_publisher = {USENIX Association},
 old_address = {Berkeley, CA, USA},
}

@article{SurveySymbolic,
 author = {Baldoni, Roberto and Coppa, Emilio and D'Elia, Daniele Cono and Demetrescu, Camil and Finocchi, Irene},
 title = {A Survey of Symbolic Execution Techniques},
 journal = {ACM Computing Surveys},
 issue_date = {July 2018},
 volume = {51},
 number = {3},
 old_month = may,
 year = {2018},
 issn = {0360-0300},
 pages = {50:1--50:39},
 articleno = {50},
 numpages = {39},
 url = {http://doi.acm.org/10.1145/3182657},
 doi = {10.1145/3182657},
 acmid = {3182657},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Symbolic execution, concolic execution, software testing, static analysis},
} 

@misc{makingsoftwaredumberer,
  author = {Tavis Ormandy},
  title = {{Making Software Dumberer}},
  howpublished = "\url{http://taviso.decsystem.org/making_software_dumber.pdf}",
  year = {2009}, 
  note = "[Online; accessed 10-Sep-2019]"
}

@misc{lafintel,
  title = {{Circumventing Fuzzing Roadblocks with Compiler Transformations}},
  howpublished = "\url{https://lafintel.wordpress.com/2016/08/15/circumventing-fuzzing-roadblocks-with-compiler-transformations/}",
  year = {2016}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{compcov,
  author = {Mateusz Jurczyk},
  title = {{CompareCoverage}},
  howpublished = "\url{https://github.com/googleprojectzero/CompareCoverage/}",
  year = {2019}, 
  note = "[Online; accessed 10-Sep-2019]"
}

@misc{hongg,
  author = {Robert Swiecki},
  title = {{honggfuzz}},
  howpublished = "\url{https://github.com/google/honggfuzz}",
  year = {2017}, 
  note = "[Online; accessed 10-Sep-2019]"
}

@misc{AFLPP,
  author = {Heuse, Marc and Ei{\ss}feldt, Heiko and Fioraldi, Andrea},
  title = {{AFL++}},
  howpublished = "\url{https://github.com/vanhauser-thc/AFLplusplus}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{objdump-1,
  author = {Bugzilla},
  title = {{Bug \#25447}},
  howpublished = "\url{https://sourceware.org/bugzilla/show_bug.cgi?id=25447}",
  year = {2020}, 
  note = "[Online; accessed 10-Sep-2019]"
}



@inproceedings{Li:2017:SPB:3106237.3106295,
 author = {Li, Yuekang and Chen, Bihuan and Chandramohan, Mahinthan and Lin, Shang-Wei and Liu, Yang and Tiu, Alwen},
 title = {Steelix: Program-state Based Binary Fuzzing},
 booktitle = {Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering},
 series = {ESEC/FSE 2017},
 year = {2017},
 isbn = {978-1-4503-5105-8},
 old_location = {Paderborn, Germany},
 pages = {627--637},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/3106237.3106295},
 doi = {10.1145/3106237.3106295},
 old_acmid = {3106295},
 old_publisher = {ACM},
 old_address = {New York, NY, USA},
 keywords = {binary fuzzing, binary instrumentation, coverage-based fuzzing},
} 

@inproceedings{vuzzer,
  author    = {Sanjay Rawat and
               Vivek Jain and
               Ashish Kumar and
               Lucian Cojocar and
               Cristiano Giuffrida and
               Herbert Bos},
  title     = {VUzzer: Application-aware Evolutionary Fuzzing},
  booktitle = {24th Annual Network and Distributed System Security Symposium, {NDSS}},
  year      = {2017},
  url       = {https://www.ndss-symposium.org/ndss2017/ndss-2017-programme/vuzzer-application-aware-evolutionary-fuzzing/},
  timestamp = {Tue, 16 Jan 2018 15:44:17 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/ndss/0001JKCGB17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{redqueen,
  author    = {Cornelius Aschermann and
               Sergej Schumilo and
               Tim Blazytko and
               Robert Gawlik and
               Thorsten Holz},
  title     = {{REDQUEEN:} Fuzzing with Input-to-State Correspondence},
  booktitle = {Proceedings of the 26th Annual Network and Distributed System Security Symposium, {NDSS}},
  year      = {2019},
  url       = {https://www.ndss-symposium.org/ndss-paper/redqueen-fuzzing-with-input-to-state-correspondence/},
  timestamp = {Thu, 02 May 2019 15:52:50 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ndss/AschermannSBGH19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{SLF,  
  author = {You, Wei and Liu, Xuwei and Ma, Shiqing and Perry, David and Zhang, Xiangyu and Liang, Bin},
  booktitle = {Proceedings of the 41st International Conference on Software Engineering},
  series = {ICSE '19},  
  title={{SLF}: Fuzzing without Valid Seed Inputs},   
  year={2019},  
  pages={712-723},
  numpages = {12},
  url = {https://doi.org/10.1109/ICSE.2019.00080},
  doi = {10.1109/ICSE.2019.00080}
}

@article{old_angora,
  author    = {Peng Chen and
               Hao Chen},
  title     = {Angora: Efficient Fuzzing by Principled Search},
  journal   = {CoRR},
  volume    = {abs/1803.01307},
  year      = {2018},
  url       = {http://arxiv.org/abs/1803.01307},
  archivePrefix = {arXiv},
  eprint    = {1803.01307},
  timestamp = {Mon, 13 Aug 2018 16:46:10 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1803-01307},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@INPROCEEDINGS{angora,
  author={P. {Chen} and H. {Chen}},
  booktitle={Proceedings of the 2018 IEEE Symposium on Security and Privacy (SP)},
  title={Angora: Efficient Fuzzing by Principled Search},
  year={2018},
  pages={711-725},
  doi={10.1109/SP.2018.00046},
  url={https://doi.org/10.1109/SP.2018.00046}
}

@inproceedings{ECLIPSER-ICSE19,
 author = {Choi, Jaeseung and Jang, Joonun and Han, Choongwoo and Cha, Sang Kil},
 title = {Grey-box Concolic Testing on Binary Code},
 booktitle = {Proceedings of the 41st International Conference on Software Engineering},
 series = {ICSE '19},
 year = {2019},
 old_location = {Montreal, Quebec, Canada},
 pages = {736--747},
 numpages = {12},
 url = {https://doi.org/10.1109/ICSE.2019.00082},
 doi = {10.1109/ICSE.2019.00082},
 old_acmid = {3339599},
 old_publisher = {IEEE Press},
 old_address = {Piscataway, NJ, USA},
 keywords = {concolic testing, fuzzing, software testing},
}

@inproceedings{KLEE-OSDI08,
 author = {Cadar, Cristian and Dunbar, Daniel and Engler, Dawson},
 title = {{KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs}},
 booktitle = {Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation},
 series = {OSDI'08},
 year = {2008},
 location = {San Diego, California},
 pages = {209--224},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=1855741.1855756},
 acmid = {1855756},
 publisher = {USENIX Association},
 address = {Berkeley, CA, USA},
} 

@inproceedings{Cha:2012:UMB:2310656.2310692,
 author = {Cha, Sang Kil and Avgerinos, Thanassis and Rebert, Alexandre and Brumley, David},
 title = {Unleashing Mayhem on Binary Code},
 booktitle = {Proceedings of the 2012 IEEE Symposium on Security and Privacy},
 series = {SP '12},
 year = {2012},
 isbn = {978-0-7695-4681-0},
 pages = {380--394},
 numpages = {15},
 url = {https://doi.org/10.1109/SP.2012.31},
 doi = {10.1109/SP.2012.31},
 acmid = {2310692},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 keywords = {hybrid execution, symbolic memory, index-based memory modeling, exploit generation},
} 

@INPROCEEDINGS{conf/sp/WangWGZ10,
  author={T. {Wang} and T. {Wei} and G. {Gu} and W. {Zou}},
  booktitle={2010 IEEE Symposium on Security and Privacy (SP)},
  title={TaintScope: A Checksum-Aware Directed Fuzzing Tool for Automatic Software Vulnerability Detection},
  year={2010},
  volume={},
  number={},
  pages={497-512},
  doi={10.1109/SP.2010.37},
  ISSN={},
  old_month={May},
  url={https://doi.org/10.1109/SP.2010.37}
}

@INPROCEEDINGS{t-fuzz,
  author={H. {Peng} and Y. {Shoshitaishvili} and M. {Payer}},
  booktitle={2018 IEEE Symposium on Security and Privacy (SP)},
  title={T-Fuzz: Fuzzing by Program Transformation},
  year={2018},
  volume={},
  number={},
  pages={697-710},
  doi={10.1109/SP.2018.00056},
  ISSN={2375-1207},
  month={May},
  doi={10.1109/SP.2018.00056},
  url={https://doi.org/10.1109/SP.2018.00056}
}

@misc{libfuzzer,
  author = {Kosta Serebryany},
  title = {{libFuzzer: a library for coverage-guided fuzz testing}},
  howpublished = "\url{http://llvm.org/docs/LibFuzzer.html}",
  year = {2015}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{jfs-c-interface,
  author = {Stinnett, Ryan J.},
  title = {{JFS: issue \#22}},
  howpublished = "\url{https://github.com/mc-imperial/jfs/issues/22}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{jfs-custom-seeds,
  author = {Liew, Dan},
  title = {{JFS: issue \#4}},
  howpublished = "\url{https://github.com/mc-imperial/jfs/issues/4}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@inproceedings{libfuzzer-paper,
  author    = {Kosta Serebryany},
  title     = {Continuous Fuzzing with libFuzzer and AddressSanitizer},
  booktitle = {2016 {IEEE} Cybersecurity Development},
  series    = {SecDev '16},
  pages     = {157},
  old_publisher = {{IEEE} Computer Society},
  year      = {2016},
  url       = {https://doi.org/10.1109/SecDev.2016.043},
  doi       = {10.1109/SecDev.2016.043},
}

@misc{qsym-removed-fuzzbench,
  author = {Google},
  title = {{FuzzBench: issue \#131}},
  howpublished = "\url{https://github.com/google/fuzzbench/issues/131}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{peach,
  author = {M. Eddington},
  title = {{Peach fuzzing platform}},
  howpublished = "\url{http://community.peachfuzzer.com/WhatIsPeach.html}",
  note = "[Online; accessed 10-Sep-2019]",
  year = {}
}

@article{aflsmart-tse,
author={V. {Pham} and M. {Boehme} and A. E. {Santosa} and A. R. {Caciulescu} and A. {Roychoudhury}},
journal={IEEE Transactions on Software Engineering},
title={Smart Greybox Fuzzing},
year={2019},
doi={10.1109/TSE.2019.2941681},
url       = {https://doi.org/10.1109/TSE.2019.2941681},
}

@misc{libproto,
  title = {{libprotobuf-mutator}},
  howpublished = "\url{https://github.com/google/libprotobuf-mutator}",
  note = "[Online; accessed 10-Sep-2019]"
}

@inproceedings{superion,
 author = {Wang, Junjie and Chen, Bihuan and Wei, Lei and Liu, Yang},
 title = {Superion: Grammar-aware Greybox Fuzzing},
 booktitle = {Proceedings of the 41st International Conference on Software Engineering},
 series = {ICSE '19},
 year = {2019},
 old_location = {Montreal, Quebec, Canada},
 pages = {724--735},
 numpages = {12},
 url = {https://doi.org/10.1109/ICSE.2019.00081},
 doi = {10.1109/ICSE.2019.00081},
 acmid = {3339598},
 old_publisher = {IEEE Press},
 old_address = {Piscataway, NJ, USA},
 old_keywords = {ASTs, greybox fuzzing, structured inputs},
}

@inproceedings{nautilus,
  author    = {Cornelius Aschermann and
               Tommaso Frassetto and
               Thorsten Holz and
               Patrick Jauernig and
               Ahmad{-}Reza Sadeghi and
               Daniel Teuchert},
  title     = {{NAUTILUS:} Fishing for Deep Bugs with Grammars},
  booktitle = {26th Annual Network and Distributed System Security Symposium, {NDSS}},
  year      = {2019},
  url       = {https://www.ndss-symposium.org/ndss-paper/nautilus-fishing-for-deep-bugs-with-grammars/},
  timestamp = {Thu, 02 May 2019 15:52:50 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ndss/AschermannFHJST19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Holler:2012:FCF:2362793.2362831,
 author = {Holler, Christian and Herzig, Kim and Zeller, Andreas},
 title = {Fuzzing with Code Fragments},
 booktitle = {Proceedings of the 21st USENIX Conference on Security Symposium},
 series = {SEC'12},
 year = {2012},
 odl_location = {Bellevue, WA},
 pages = {38--38},
 numpages = {1},
 url = {http://dl.acm.org/citation.cfm?id=2362793.2362831},
 acmid = {2362831},
 old_publisher = {USENIX Association},
 old_address = {Berkeley, CA, USA},
} 

@masterthesis{saelo,
  title={{FuzzIL: Coverage Guided Fuzzing for JavaScript Engines}},
  author={Samuel Gro{\ss}},
  year={2018},
  school={Karlsruhe Institute of Technology},
}



@inproceedings {grimoire,
author = {Tim Blazytko and Cornelius Aschermann and Moritz Schl{\"o}gel and Ali Abbasi and Sergej Schumilo and Simon W{\"o}rner and Thorsten Holz},
title = {{GRIMOIRE}: Synthesizing Structure while Fuzzing},
booktitle = {28th {USENIX} Security Symposium ({USENIX} Security 19)},
year = {2019},
isbn = {978-1-939133-06-9},
old_address = {Santa Clara, CA},
pages = {1985--2002},
url = {https://www.usenix.org/system/files/sec19-blazytko.pdf},
old_publisher = {{USENIX} Association},
old_month = aug,
}

@inproceedings{Bastani:2017:SPI:3062341.3062349,
 author = {Bastani, Osbert and Sharma, Rahul and Aiken, Alex and Liang, Percy},
 title = {Synthesizing Program Input Grammars},
 booktitle = {Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI 2017},
 year = {2017},
 isbn = {978-1-4503-4988-8},
 location = {Barcelona, Spain},
 pages = {95--110},
 numpages = {16},
 url = {http://doi.acm.org/10.1145/3062341.3062349},
 doi = {10.1145/3062341.3062349},
 acmid = {3062349},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {fuzzing, grammar synthesis},
} 

@article{DBLP:journals/corr/GodefroidPS17,
  author    = {Patrice Godefroid and
               Hila Peleg and
               Rishabh Singh},
  title     = {Learn{\&}Fuzz: Machine Learning for Input Fuzzing},
  journal   = {CoRR},
  volume    = {abs/1701.07232},
  year      = {2017},
  url       = {http://arxiv.org/abs/1701.07232},
  archivePrefix = {arXiv},
  eprint    = {1701.07232},
  timestamp = {Mon, 13 Aug 2018 16:47:21 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/GodefroidPS17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Jain:2018:TUI:3274694.3274746,
 author = {Jain, Vivek and Rawat, Sanjay and Giuffrida, Cristiano and Bos, Herbert},
 title = {TIFF: Using Input Type Inference To Improve Fuzzing},
 booktitle = {Proceedings of the 34th Annual Computer Security Applications Conference},
 series = {ACSAC '18},
 year = {2018},
 isbn = {978-1-4503-6569-7},
 location = {San Juan, PR, USA},
 pages = {505--517},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/3274694.3274746},
 doi = {10.1145/3274694.3274746},
 acmid = {3274746},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Fuzzing, Taint-flow analysis, data-structure Identification, security, type inference, vulnerability/bug detection},
}

@inproceedings{sok-DTA,
 author = {Schwartz, Edward J. and Avgerinos, Thanassis and Brumley, David},
 title = {All You Ever Wanted to Know About Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)},
 booktitle = {Proceedings of the 2010 IEEE Symposium on Security and Privacy},
 series = {SP 2010},
 year = {2010},
 isbn = {978-0-7695-4035-1},
 pages = {317--331},
 numpages = {15},
 url = {http://dx.doi.org/10.1109/SP.2010.26},
 doi = {10.1109/SP.2010.26},
 old_acmid = {1849981},
 old_publisher = {IEEE Computer Society},
 old_address = {Washington, DC, USA},
 keywords = {taint analysis, symbolic execution, dynamic analysis},
}

@inproceedings{sok-DBI,
 author = {D'Elia, Daniele Cono and Coppa, Emilio and Nicchi, Simone and Palmaro, Federico and Cavallaro, Lorenzo},
 title = {SoK: Using Dynamic Binary Instrumentation for Security (And How You May Get Caught Red Handed)},
 booktitle = {Proceedings of the 2019 ACM Asia Conference on Computer and Communications Security},
 series = {Asia CCS '19},
 year = {2019},
 isbn = {978-1-4503-6752-3},
 old_location = {Auckland, New Zealand},
 pages = {15--27},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/3321705.3329819},
 doi = {10.1145/3321705.3329819},
 old_acmid = {3329819},
 old_publisher = {ACM},
 old_address = {New York, NY, USA},
 keywords = {dynamic binary instrumentation, dynamic binary translation, escape, evasion, interposition, transparent monitoring},
} 

@article{shoshitaishvili2016state,
  title={SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis},
  author={Shoshitaishvili, Yan and Wang, Ruoyu and Salls, Christopher and Stephens, Nick and Polino, Mario and Dutcher, Audrey and Grosen, John and Feng, Siji and Hauser, Christophe and Kruegel, Christopher and Vigna, Giovanni},
  booktitle={Proceedings of the 2016 IEEE Symposium on Security and Privacy},
  year={2016}
}

@inproceedings {profuzzer,
  author = {W. You and X. Wang and S. Ma and J. Huang and X. Zhang and X. Wang and B. Liang},
  booktitle = {2019 2019 IEEE Symposium on Security and Privacy (SP)},
  title = {ProFuzzer: On-the-fly Input Type Probing for Better Zero-Day Vulnerability Discovery},
  year = {2019},
  volume = {},
  issn = {2375-1207},
  pages = {882-899},
  keywords = {fuzzing;probing;input-type;vulnerability-discovery},
  doi = {10.1109/SP.2019.00057},
  url = {https://doi.ieeecomputersociety.org/10.1109/SP.2019.00057},
  publisher = {IEEE Computer Society},
  address = {Los Alamitos, CA, USA},
  month = {may}
}

@INPROCEEDINGS{debray-sp15,
author={B. {Yadegari} and B. {Johannesmeyer} and B. {Whitely} and S. {Debray}},
booktitle={2015 IEEE Symposium on Security and Privacy (SP)},
title={A Generic Approach to Automatic Deobfuscation of Executable Code},
year={2015},
pages={674-691},
doi={10.1109/SP.2015.47},
ISSN={},
old_month={May},
url={http://dx.doi.org/10.1109/SP.2015.47}
}

@INPROCEEDINGS {debray-scam14,
author = {B. Yadegari and S. Debray},
booktitle = {2014 IEEE 14th International Working Conference on Source Code Analysis and Manipulation (SCAM)},
title = {Bit-Level Taint Analysis},
year = {2014},
volume = {},
issn = {},
pages = {255-264},
keywords = {algorithm design and analysis;semantics;registers;standards;heuristic algorithms;data handling;performance analysis},
doi = {10.1109/SCAM.2014.43},
url = {https://doi.ieeecomputersociety.org/10.1109/SCAM.2014.43},
old_publisher = {IEEE Computer Society},
old_address = {Los Alamitos, CA, USA},
old_month = {sep}
}

@misc{kinaSUR,
    author = "{Ministry for Primary Industries}",
    title = {{Kina sea urchin regions in NZ}},
    howpublished = {\url{http://fs.fish.govt.nz/Page.aspx?pk=7&sc=SUR}},
    note = {Online; accessed 29 January 2014} ,
    year=2013,
}

@misc{small-files-project,
  author = {Mathias Bynens},
  title = {{Smallest possible syntactically valid files of different types}},
  howpublished = "\url{https://github.com/mathiasbynens/small}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{google-oss-fuzz,
  title = {{Google OSS-Fuzz: continuous fuzzing of open source software}},
  howpublished = "\url{https://github.com/google/oss-fuzz}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{house-of-spirit,
  author = {Blackngel},
  title = {{MALLOC DES-MALEFICARUM}},
  howpublished = "\url{http://phrack.org/issues/66/10.html}",
  year = {2019}, 
  note = "[Online; accessed 10-Sep-2019]"
}

@misc{fuzzing-book,
  author = {Zeller, A. and Gopinath, R. and B\"{o}hme,  M. and Fraser, G.  and Holler, C.},
  title = {{The Fuzzing Book}},
  howpublished = "\url{https://www.fuzzingbook.org/}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@book{fuzzing-intro,
 author = {Takanen, Ari and Demott, Jared D. and Miller, Charles},
 title = {Fuzzing for Software Security Testing and Quality Assurance},
 year = {2018},
 isbn = {1608078507, 9781608078509},
 edition = {2nd},
 publisher = {Artech House, Inc.},
 address = {Norwood, MA, USA},
} 

@misc{libpng_example,
  title = {{A simple libpng example program}},
  howpublished = "\url{http://zarb.org/~gc/html/libpng.html}",
  note = "[Online; accessed 10-Sep-2019]"
}

@InProceedings{wrapped-intervals,
author="Navas, Jorge A.
  and Schachte, Peter
  and S{\o}ndergaard, Harald
  and Stuckey, Peter J.",
odl_editor="Jhala, Ranjit and Igarashi, Atsushi",
title="Signedness-Agnostic Program Analysis: Precise Integer Bounds for Low-Level Code",
booktitle="Proceedings of the 10th Asian Symposium on Programming Languages and Systems",
url = {https://doi.org/10.1007/978-3-642-35182-2\_9},
year="2012",
series={APLAS '12},
old_publisher="Springer Berlin Heidelberg",
old_address="Berlin, Heidelberg",
pages="115--130",
old_isbn="978-3-642-35182-2",
doi=10.1007/978-3-642-35182-2\_9,
}

@book{art-software-testing,
  address = {Hoboken and N.J},
  author = {Myers, Glenford J. and Sandler, Corey and Badgett, Tom},
  edition = {3rd ed},
  publisher = {John Wiley \& Sons},
  title = {The art of software testing},
  year = 2012,
  isbn = {1118031962},
}

@InProceedings{LAVAM,
  author={B. {Dolan-Gavitt} and P. {Hulin} and E. {Kirda} and T. {Leek} and A. {Mambretti} and W. {Robertson} and F. {Ulrich} and R. {Whelan}},
  booktitle={Proceedings of the 2016 IEEE Symposium on Security and Privacy},
  series={SP '16},
  doi={10.1109/SP.2016.15}, 
  title={{LAVA: Large-Scale Automated Vulnerability Addition}}, 
  year={2016},
  pages={110-121},
  url = {https://doi.org/10.1109/SP.2016.15},
}


@inproceedings{Z3-TACS08,
 author = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
 title = {Z3: An Efficient SMT Solver},
 booktitle = {Proceedings of 14th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems},
 series = {TACAS'08/ETAPS'08},
 year = {2008},
 isbn = {3-540-78799-2, 978-3-540-78799-0},
 old_location = {Budapest, Hungary},
 pages = {337--340},
 oldNumpages = {4},
 doi = {10.1007/978-3-540-78800-3_24},
 oldUrl = {http://dl.acm.org/citation.cfm?id=1792734.1792766},
 old_acmid = {1792766},
 old_AddressSpringer = {Berlin Heidelberg},
 url = {https://doi.org/10.1007/978-3-540-78800-3_24},
} 

@inproceedings{SPF,
  author = {Pasareanu, Corina S. and Mehlitz, Peter C. and Bushnell, David H. and Gundy-Burlet, Karen and Lowry, Michael and Person, Suzette and Pape, Mark},
  title = {Combining Unit-Level Symbolic Execution and System-Level Concrete Execution for Testing Nasa Software},
  year = {2008},
  url = {https://doi.org/10.1145/1390630.1390635},
  doi = {10.1145/1390630.1390635},
  booktitle = {Proceedings of the 2008 International Symposium on Software Testing and Analysis},
  pages = {15–26},
  numpages = {12},
  series = {ISSTA '08}
}

@inproceedings{ANGR-SSP16,
  author    = {Yan Shoshitaishvili and
               Ruoyu Wang and
               Christopher Salls and
               Nick Stephens and
               Mario Polino and
               Andrew Dutcher and
               John Grosen and
               Siji Feng and
               Christophe Hauser and
               Christopher Kruegel and
               Giovanni Vigna},
  title     = {{SOK:} (State of) The Art of War: Offensive Techniques in Binary Analysis},
  booktitle = {Proceedings of the 2016 {IEEE} Symposium on Security and Privacy},
  series    = {SP'16},
  pages     = {138--157},
  year      = {2016},
  url       = {http://dx.doi.org/10.1109/SP.2016.17},
  doi       = {10.1109/SP.2016.17},
}

@article{S2E-TOCS12,
  author    = {Vitaly Chipounov and
               Volodymyr Kuznetsov and
               George Candea},
  title     = {The {S2E} Platform: Design, Implementation, and Applications},
  journal   = {ACM Trans. on Computer Systems (TOCS)},
  series  = {TOCS 2011},
  volume    = {30},
  number    = {1},
  pages     = {2:1--2:49},
  year      = {2012},
  url       = {http://doi.acm.org/10.1145/2110356.2110358},
  doi       = {10.1145/2110356.2110358},
  timestamp = {Wed, 07 Mar 2012 18:02:27 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/tocs/ChipounovKC12},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{DRILLER-NDSS16,
  author    = {Nick Stephens and
               John Grosen and
               Christopher Salls and
               Andrew Dutcher and
               Ruoyu Wang and
               Jacopo Corbetta and
               Yan Shoshitaishvili and
               Christopher Kruegel and
               Giovanni Vigna},
  title     = {Driller: Augmenting Fuzzing Through Selective Symbolic Execution},
  booktitle = {Proceeings of the 23nd Annual Network and Distributed System Security Symposium},
  series  = {NDSS'16},
  year      = {2016},
  url       = {http://www.internetsociety.org/sites/default/files/blogs-media/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf},
  timestamp = {Wed, 06 Jul 2016 15:51:39 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ndss/StephensGSDWCSK16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@inproceedings{AFLPP-WOOT20,
  author    = {Fioraldi, Andrea and Maier, Dominik and Ei{\ss}feldt, Heiko and Heuse, Marc},
  title     = {{AFL++: Combining incremental steps of fuzzing research}},
  booktitle = {Proceedings of the 14th USENIX Workshop on Offensive Technologies},
  series  = {WOOT '20},
  year      = {2020},
  url       = {http://www.internetsociety.org/sites/default/files/blogs-media/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf},
}

@misc{AFL-COV,
  author    = {Fioraldi, Andrea},
  title = {{afl-qemu-cov}},
  howpublished = "\url{https://github.com/andreafioraldi/afl-qemu-cov}",
  note = "[Online; accessed 20-Aug-2020]"
}

@inproceedings{COLL-AFL,
  author={S. {Gan} and C. {Zhang} and X. {Qin} and X. {Tu} and K. {Li} and Z. {Pei} and Z. {Chen}},
  booktitle={2018 IEEE Symposium on Security and Privacy},
  series = {SP '18},
  doi = {10.1109/SP.2018.00040}, 
  title={CollAFL: Path Sensitive Fuzzing}, 
  year={2018},
  pages={679-696},
  url       = {http://dx.doi.org/10.1109/SP.2018.00040},
}

@inproceedings{TRIDENT-ISSTA20,
  author = {Yao, Peisen and Shi, Qingkai and Huang, Heqing and Zhang, Charles},
  title = {Fast Bit-Vector Satisfiability},
  year = {2020},
  old_publisher = {Association for Computing Machinery},
  old_address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3395363.3397378},
  doi = {10.1145/3395363.3397378},
  booktitle = {Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis},
  pages = {38–50},
  numpages = {13},
  series = {ISSTA '20}
}


@inproceedings{PANGOLIN-SP20,
  author = {H. Huang and P. Yao and R. Wu and Q. Shi and C. Zhang},
  booktitle = {Proceedings of the 2020 IEEE Symposium on Security and Privacy (SP)},
  title = {Pangolin: Incremental Hybrid Fuzzing with Polyhedral Path Abstraction},
  year = {2020},
  pages = {1613-1627},
  doi = {10.1109/SP40000.2020.00063},
  url = {https://doi.ieeecomputersociety.org/10.1109/SP40000.2020.00063},
  old_publisher = {IEEE Computer Society},
}

@inproceedings{Pin-PLDI05,
 author = {Luk, Chi-Keung and Cohn, Robert and Muth, Robert and Patil, Harish and Klauser, Artur and Lowney, Geoff and Wallace, Steven and Reddi, Vijay Janapa and Hazelwood, Kim},
 title = {Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation},
 old_booktitle = {Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series = {PLDI '05},
 year = {2005},
 isbn = {1-59593-056-6},
 old_location = {Chicago, IL, USA},
 old_pages = {190--200},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1065010.1065034},
 old_doi = {10.1145/1065010.1065034},
 acmid = {1065034},
 publisher = {ACM},
 old_address = {New York, NY, USA},
 keywords = {dynamic compilation, instrumentation, program analysis tools},
}

@inproceedings{SAGE-NDSS08,
  author    = {Patrice Godefroid and
               Michael Y. Levin and
               David A. Molnar},
  title     = {{Automated Whitebox Fuzz Testing}},
  booktitle = {Proceedings of the 2008 Network and Distributed System Security Symposium},
  series = {NDSS'08},
  year      = {2008},
  url       = {http://www.isoc.org/isoc/conferences/ndss/08/papers/10_automated_whitebox_fuzz.pdf},
  timestamp = {Thu, 18 Jun 2009 21:33:57 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/ndss/GodefroidLM08},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@misc{symcc-pi-unsat,
  title = {{SymCC: issue \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{aflpp-parallel-mode,
  title = {{Single-system parallelization}},
  howpublished = "\url{https://aflplus.plus/docs/parallel_fuzzing/}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}


@misc{aflpp-colorization,
  title = {{CmpLog instrumentation for QEMU inspired by Redqueen}},
  howpublished = "\url{https://aflplus.plus/features/}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{antiword-1,
  title = {{Debian Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{antiword-2,
  title = {{Debian Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{antiword-3,
  title = {{Debian Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{jhead-1,
  title = {{Debian Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{jhead-2,
  title = {{Debian Bug \#967924}},
  howpublished = "\url{https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=967924}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{jhead-3,
  title = {{Debian Bug \#967971}},
  howpublished = "\url{https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=967971}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{jhead-4,
  title = {{Debian Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{grep-1,
  title = {{GNU Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{grep-2,
  title = {{GNU Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{sleuthkit-1,
  title = {{Sleuth Kit GitHub issue \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{sleuthkit-2,
  title = {{Sleuth Kit GitHub issue \#1264}},
  howpublished = "\url{https://github.com/sleuthkit/sleuthkit/issues/1264}",
  year = {2018}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{sleuthkit-3,
  title = {{Sleuth Kit GitHub issue \#1902}},
  howpublished = "\url{https://github.com/sleuthkit/sleuthkit/issues/1902}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{sleuthkit-4,
  title = {{Sleuth Kit GitHub issue \#912}},
  howpublished = "\url{https://github.com/sleuthkit/sleuthkit/issues/912}",
  year = {2017}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{xfpt-1,
  title = {{Debian Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{xfpt-2,
  title = {{Debian Bug \#XYZ (anonymized)}},
  howpublished = "\url{http://anonymized.url}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{bento-1,
  title = {{Bento4 GitHub issue \#204}},
  howpublished = "\url{https://github.com/axiomatic-systems/Bento4/issues/204}",
  year = {2017}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{bento-2,
  title = {{Bento4 GitHub issue \#353}},
  howpublished = "\url{https://github.com/axiomatic-systems/Bento4/issues/353}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{bento-3,
  title = {{Bento4 GitHub issue \#546}},
  howpublished = "\url{https://github.com/axiomatic-systems/Bento4/issues/546}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{bento-4,
  title = {{Bento4 GitHub issue \#509}},
  howpublished = "\url{https://github.com/axiomatic-systems/Bento4/issues/509}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{bento-5,
  title = {{Bento4 GitHub issue \#534}},
  howpublished = "\url{https://github.com/axiomatic-systems/Bento4/issues/534}",
  year = {2020}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{bento-6,
  title = {{Bento4 GitHub issue \#386}},
  howpublished = "\url{https://github.com/axiomatic-systems/Bento4/issues/386}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@misc{bento-7,
  title = {{Bento4 GitHub issue \#361}},
  howpublished = "\url{https://github.com/axiomatic-systems/Bento4/issues/361}",
  year = {2019}, 
  note = "[Online; accessed 20-Aug-2020]"
}

@inproceedings{DCNPC-ASIACCS19,
 author={D'Elia, Daniele Cono and Coppa, Emilio and Nicchi, Simone and Palmaro, Federico and Cavallaro, Lorenzo},
 title={{SoK: Using Dynamic Binary Instrumentation for Security (And How You May Get Caught Red Handed)}},
 booktitle={Proceedings of the 14th ACM ASIA Conference on Computer and Communications Security},
 series={ASIACCS '19},
 year={2019},
 url = {https://doi.org/10.1145/3321705.3329819},
  doi = {10.1145/3321705.3329819},
}

@article{BCE-STVR19,
 author={Borzacchiello, Luca and Coppa, Emilio and D'Elia, Daniele Cono and Demetrescu, Camil},
 title={{Memory models in symbolic execution: key ideas and new thoughts}},
 journal={Software Testing, Verification and Reliability},
 doi={10.1002/stvr.1722},
 number={8},
 url={https://doi.org/10.1002/stvr.1722},
 volume={29},
 year={2019},
}

@inproceedings{CDD-ASE17,
 author={Coppa, Emilio and D'Elia, Daniele Cono and Demetrescu, Camil},
 title={{Rethinking Pointer Reasoning in Symbolic Execution}},
 booktitle={Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering},
 series={ASE '17},
 doi={10.1109/ASE.2017.8115671},
 numpages={6},
 url={https://doi.org/10.1109/ASE.2017.8115671},
 pages={613--618},
 year={2017},
}

@inproceedings{BCDD-CSCML19,
 author={Borzacchiello, Luca and Coppa, Emilio and D'Elia, Daniele Cono and Demetrescu, Camil},
 title={{Reconstructing C2 Servers for Remote Access Trojans with Symbolic Execution}},
 booktitle={Proceedings of the 2019 Cyber Security Cryptography and Machine Learning},
 series={CSCML '19},
 publisher={Springer International Publishing},
 old_editor={Dolev, Shlomi and Lodha, Sachin},
 doi={10.1007/978-3-030-20951-3_12},
 url={https://doi.org/10.1007/978-3-030-20951-3_12},
 year={2019},
}

@inproceedings{BCDD-CSCML17,
 author={Baldoni, Roberto and Coppa, Emilio and D'Elia, Daniele Cono and Demetrescu, Camil},
 title={{Assisting Malware Analysis with Symbolic Execution: A Case Study}},
 booktitle={Proceedings of the 2017 Cyber Security Cryptography and Machine Learning},
 series={CSCML '17},
 doi={10.1007/978-3-319-60080-2_12},
 isbn={978-3-319-60080-2},
 publisher={Springer International Publishing},
 url={https://doi.org/10.1007/978-3-319-60080-2_12},
 old_address={Cham},
 old_editor={Dolev, Shlomi and Lodha, Sachin},
 pages={171--188},
 year={2017},
}

@INPROCEEDINGS{MAYHEM,
  author={S. K. {Cha} and T. {Avgerinos} and A. {Rebert} and D. {Brumley}},
  booktitle={Proceedings of the 2012 IEEE Symposium on Security and Privacy}, 
  series={SP '12},
  title={Unleashing Mayhem on Binary Code}, 
  year={2012},
  pages={380-394},
  doi={10.1109/SP.2012.31},
  url={https://doi.org/10.1109/SP.2012.31}
}
paper.bbl
% Generated by IEEEtran.bst, version: 1.12 (2007/01/11)
\begin{thebibliography}{10}
\providecommand{\url}[1]{#1}
\csname url@samestyle\endcsname
\providecommand{\newblock}{\relax}
\providecommand{\bibinfo}[2]{#2}
\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
\providecommand{\BIBentryALTinterwordstretchfactor}{4}
\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
  \fontdimen4\font\relax}
\providecommand{\BIBforeignlanguage}[2]{{%
\expandafter\ifx\csname l@#1\endcsname\relax
\typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
\typeout{** loaded for the language `#1'. Using the pattern for}%
\typeout{** the default language instead.}%
\else
\language=\csname l@#1\endcsname
\fi
#2}}
\providecommand{\BIBdecl}{\relax}
\BIBdecl

\bibitem{AFL}
M.~Zalewski, ``{American Fuzzy Lop},'' \url{https://github.com/Google/AFL},
  2019, [Online; accessed 20-Aug-2020].

\bibitem{AFLPP}
M.~Heuse, H.~Ei{\ss}feldt, and A.~Fioraldi, ``{AFL++},''
  \url{https://github.com/vanhauser-thc/AFLplusplus}, 2019, [Online; accessed
  20-Aug-2020].

\bibitem{Barrett2018}
C.~Barrett and C.~Tinelli, \emph{Satisfiability Modulo Theories}.\hskip 1em
  plus 0.5em minus 0.4em\relax Springer International Publishing, 2018, pp.
  305--343.

\bibitem{QSYM}
\BIBentryALTinterwordspacing
I.~Yun, S.~Lee, M.~Xu, Y.~Jang, and T.~Kim, ``{QSYM}: A practical concolic
  execution engine tailored for hybrid fuzzing,'' in \emph{Proceedings of the
  27th USENIX Conference on Security Symposium}, ser. SEC'18, 2018, pp.
  745--761. [Online]. Available:
  \url{http://dl.acm.org/citation.cfm?id=3277203.3277260}
\BIBentrySTDinterwordspacing

\bibitem{SYMCC}
\BIBentryALTinterwordspacing
S.~Poeplau and A.~Francillon, ``Symbolic execution with symcc:
  Don{\textquoteright}t interpret, compile!'' in \emph{Proceedings of the 29th
  {USENIX} Security Symposium ({USENIX} Security 20)}.\hskip 1em plus 0.5em
  minus 0.4em\relax {USENIX} Association, Aug. 2020, pp. 181--198. [Online].
  Available:
  \url{https://www.usenix.org/conference/usenixsecurity20/presentation/poeplau}
\BIBentrySTDinterwordspacing

\bibitem{stephens2016driller}
\BIBentryALTinterwordspacing
N.~Stephens, J.~Grosen, C.~Salls, A.~Dutcher, R.~Wang, J.~Corbetta,
  Y.~Shoshitaishvili, C.~Kruegel, and G.~Vigna, ``Driller: Augmenting fuzzing
  through selective symbolic execution.'' in \emph{Proceeings of the 23th
  Annual Network and Distributed System Security Symposium, {NDSS}}, 2016.
  [Online]. Available:
  \url{https://www.ndss-symposium.org/wp-content/uploads/2017/09/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf}
\BIBentrySTDinterwordspacing

\bibitem{Z3-TACS08}
\BIBentryALTinterwordspacing
L.~De~Moura and N.~Bj{\o}rner, ``Z3: An efficient smt solver,'' in
  \emph{Proceedings of 14th Int. Conf. on Tools and Algorithms for the
  Construction and Analysis of Systems}, ser. TACAS'08/ETAPS'08, 2008, pp.
  337--340. [Online]. Available:
  \url{https://doi.org/10.1007/978-3-540-78800-3_24}
\BIBentrySTDinterwordspacing

\bibitem{JFS}
\BIBentryALTinterwordspacing
D.~Liew, C.~Cadar, A.~F. Donaldson, and J.~R. Stinnett, ``Just fuzz it: Solving
  floating-point constraints using coverage-guided fuzzing,'' in
  \emph{Proceedings of the 2019 27th ACM Joint Meeting on European Software
  Engineering Conference and Symposium on the Foundations of Software
  Engineering}, ser. ESEC/FSE 2019.\hskip 1em plus 0.5em minus 0.4em\relax New
  York, NY, USA: Association for Computing Machinery, 2019, p. 521–532.
  [Online]. Available: \url{https://doi.org/10.1145/3338906.3338921}
\BIBentrySTDinterwordspacing

\bibitem{LAVAM}
\BIBentryALTinterwordspacing
B.~{Dolan-Gavitt}, P.~{Hulin}, E.~{Kirda}, T.~{Leek}, A.~{Mambretti},
  W.~{Robertson}, F.~{Ulrich}, and R.~{Whelan}, ``{LAVA: Large-Scale Automated
  Vulnerability Addition},'' in \emph{Proceedings of the 2016 IEEE Symposium on
  Security and Privacy}, ser. SP '16, 2016, pp. 110--121. [Online]. Available:
  \url{https://doi.org/10.1109/SP.2016.15}
\BIBentrySTDinterwordspacing

\bibitem{ECLIPSER-ICSE19}
\BIBentryALTinterwordspacing
J.~Choi, J.~Jang, C.~Han, and S.~K. Cha, ``Grey-box concolic testing on binary
  code,'' in \emph{Proceedings of the 41st International Conference on Software
  Engineering}, ser. ICSE '19, 2019, pp. 736--747. [Online]. Available:
  \url{https://doi.org/10.1109/ICSE.2019.00082}
\BIBentrySTDinterwordspacing

\bibitem{art-software-testing}
G.~J. Myers, C.~Sandler, and T.~Badgett, \emph{The art of software testing},
  3rd~ed.\hskip 1em plus 0.5em minus 0.4em\relax Hoboken and N.J: John Wiley \&
  Sons, 2012.

\bibitem{SurveySymbolic}
\BIBentryALTinterwordspacing
R.~Baldoni, E.~Coppa, D.~C. D'Elia, C.~Demetrescu, and I.~Finocchi, ``A survey
  of symbolic execution techniques,'' \emph{ACM Computing Surveys}, vol.~51,
  no.~3, pp. 50:1--50:39, 2018. [Online]. Available:
  \url{http://doi.acm.org/10.1145/3182657}
\BIBentrySTDinterwordspacing

\bibitem{fuzzing-book}
A.~Zeller, R.~Gopinath, M.~B\"{o}hme, G.~Fraser, and C.~Holler, ``{The Fuzzing
  Book},'' \url{https://www.fuzzingbook.org/}, 2019, [Online; accessed
  20-Aug-2020].

\bibitem{ANGR-SSP16}
\BIBentryALTinterwordspacing
Y.~Shoshitaishvili, R.~Wang, C.~Salls, N.~Stephens, M.~Polino, A.~Dutcher,
  J.~Grosen, S.~Feng, C.~Hauser, C.~Kruegel, and G.~Vigna, ``{SOK:} (state of)
  the art of war: Offensive techniques in binary analysis,'' in
  \emph{Proceedings of the 2016 {IEEE} Symposium on Security and Privacy}, ser.
  SP'16, 2016, pp. 138--157. [Online]. Available:
  \url{http://dx.doi.org/10.1109/SP.2016.17}
\BIBentrySTDinterwordspacing

\bibitem{S2E-TOCS12}
\BIBentryALTinterwordspacing
V.~Chipounov, V.~Kuznetsov, and G.~Candea, ``The {S2E} platform: Design,
  implementation, and applications,'' \emph{ACM Trans. on Computer Systems
  (TOCS)}, vol.~30, no.~1, pp. 2:1--2:49, 2012. [Online]. Available:
  \url{http://doi.acm.org/10.1145/2110356.2110358}
\BIBentrySTDinterwordspacing

\bibitem{KLEE-OSDI08}
\BIBentryALTinterwordspacing
C.~Cadar, D.~Dunbar, and D.~Engler, ``{KLEE: Unassisted and Automatic
  Generation of High-coverage Tests for Complex Systems Programs},'' in
  \emph{Proceedings of the 8th USENIX Conference on Operating Systems Design
  and Implementation}, ser. OSDI'08.\hskip 1em plus 0.5em minus 0.4em\relax
  Berkeley, CA, USA: USENIX Association, 2008, pp. 209--224. [Online].
  Available: \url{http://dl.acm.org/citation.cfm?id=1855741.1855756}
\BIBentrySTDinterwordspacing

\bibitem{SPF}
\BIBentryALTinterwordspacing
C.~S. Pasareanu, P.~C. Mehlitz, D.~H. Bushnell, K.~Gundy-Burlet, M.~Lowry,
  S.~Person, and M.~Pape, ``Combining unit-level symbolic execution and
  system-level concrete execution for testing nasa software,'' in
  \emph{Proceedings of the 2008 International Symposium on Software Testing and
  Analysis}, ser. ISSTA '08, 2008, p. 15–26. [Online]. Available:
  \url{https://doi.org/10.1145/1390630.1390635}
\BIBentrySTDinterwordspacing

\bibitem{MAYHEM}
\BIBentryALTinterwordspacing
S.~K. {Cha}, T.~{Avgerinos}, A.~{Rebert}, and D.~{Brumley}, ``Unleashing mayhem
  on binary code,'' in \emph{Proceedings of the 2012 IEEE Symposium on Security
  and Privacy}, ser. SP '12, 2012, pp. 380--394. [Online]. Available:
  \url{https://doi.org/10.1109/SP.2012.31}
\BIBentrySTDinterwordspacing

\bibitem{BCDD-CSCML17}
\BIBentryALTinterwordspacing
R.~Baldoni, E.~Coppa, D.~C. D'Elia, and C.~Demetrescu, ``{Assisting Malware
  Analysis with Symbolic Execution: A Case Study},'' in \emph{Proceedings of
  the 2017 Cyber Security Cryptography and Machine Learning}, ser. CSCML
  '17.\hskip 1em plus 0.5em minus 0.4em\relax Springer International
  Publishing, 2017, pp. 171--188. [Online]. Available:
  \url{https://doi.org/10.1007/978-3-319-60080-2_12}
\BIBentrySTDinterwordspacing

\bibitem{BCDD-CSCML19}
\BIBentryALTinterwordspacing
L.~Borzacchiello, E.~Coppa, D.~C. D'Elia, and C.~Demetrescu, ``{Reconstructing
  C2 Servers for Remote Access Trojans with Symbolic Execution},'' in
  \emph{Proceedings of the 2019 Cyber Security Cryptography and Machine
  Learning}, ser. CSCML '19.\hskip 1em plus 0.5em minus 0.4em\relax Springer
  International Publishing, 2019. [Online]. Available:
  \url{https://doi.org/10.1007/978-3-030-20951-3_12}
\BIBentrySTDinterwordspacing

\bibitem{SAGE-NDSS08}
\BIBentryALTinterwordspacing
P.~Godefroid, M.~Y. Levin, and D.~A. Molnar, ``{Automated Whitebox Fuzz
  Testing},'' in \emph{Proceedings of the 2008 Network and Distributed System
  Security Symposium}, ser. NDSS'08, 2008. [Online]. Available:
  \url{http://www.isoc.org/isoc/conferences/ndss/08/papers/10_automated_whitebox_fuzz.pdf}
\BIBentrySTDinterwordspacing

\bibitem{CDD-ASE17}
\BIBentryALTinterwordspacing
E.~Coppa, D.~C. D'Elia, and C.~Demetrescu, ``{Rethinking Pointer Reasoning in
  Symbolic Execution},'' in \emph{Proceedings of the 32nd IEEE/ACM
  International Conference on Automated Software Engineering}, ser. ASE '17,
  2017, pp. 613--618. [Online]. Available:
  \url{https://doi.org/10.1109/ASE.2017.8115671}
\BIBentrySTDinterwordspacing

\bibitem{BCE-STVR19}
\BIBentryALTinterwordspacing
L.~Borzacchiello, E.~Coppa, D.~C. D'Elia, and C.~Demetrescu, ``{Memory models
  in symbolic execution: key ideas and new thoughts},'' \emph{Software Testing,
  Verification and Reliability}, vol.~29, no.~8, 2019. [Online]. Available:
  \url{https://doi.org/10.1002/stvr.1722}
\BIBentrySTDinterwordspacing

\bibitem{PANGOLIN-SP20}
\BIBentryALTinterwordspacing
H.~Huang, P.~Yao, R.~Wu, Q.~Shi, and C.~Zhang, ``Pangolin: Incremental hybrid
  fuzzing with polyhedral path abstraction,'' in \emph{Proceedings of the 2020
  IEEE Symposium on Security and Privacy (SP)}, 2020, pp. 1613--1627. [Online].
  Available:
  \url{https://doi.ieeecomputersociety.org/10.1109/SP40000.2020.00063}
\BIBentrySTDinterwordspacing

\bibitem{TRIDENT-ISSTA20}
\BIBentryALTinterwordspacing
P.~Yao, Q.~Shi, H.~Huang, and C.~Zhang, ``Fast bit-vector satisfiability,'' in
  \emph{Proceedings of the 29th ACM SIGSOFT International Symposium on Software
  Testing and Analysis}, ser. ISSTA '20, 2020, p. 38–50. [Online]. Available:
  \url{https://doi.org/10.1145/3395363.3397378}
\BIBentrySTDinterwordspacing

\bibitem{aflsmart-tse}
\BIBentryALTinterwordspacing
V.~{Pham}, M.~{Boehme}, A.~E. {Santosa}, A.~R. {Caciulescu}, and
  A.~{Roychoudhury}, ``Smart greybox fuzzing,'' \emph{IEEE Transactions on
  Software Engineering}, 2019. [Online]. Available:
  \url{https://doi.org/10.1109/TSE.2019.2941681}
\BIBentrySTDinterwordspacing

\bibitem{google-oss-fuzz}
``{Google OSS-Fuzz: continuous fuzzing of open source software},''
  \url{https://github.com/google/oss-fuzz}, 2019, [Online; accessed
  20-Aug-2020].

\bibitem{DRILLER-NDSS16}
\BIBentryALTinterwordspacing
N.~Stephens, J.~Grosen, C.~Salls, A.~Dutcher, R.~Wang, J.~Corbetta,
  Y.~Shoshitaishvili, C.~Kruegel, and G.~Vigna, ``Driller: Augmenting fuzzing
  through selective symbolic execution,'' in \emph{Proceeings of the 23nd
  Annual Network and Distributed System Security Symposium}, ser. NDSS'16,
  2016. [Online]. Available:
  \url{http://www.internetsociety.org/sites/default/files/blogs-media/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf}
\BIBentrySTDinterwordspacing

\bibitem{lafintel}
``{Circumventing Fuzzing Roadblocks with Compiler Transformations},''
  \url{https://lafintel.wordpress.com/2016/08/15/circumventing-fuzzing-roadblocks-with-compiler-transformations/},
  2016, [Online; accessed 20-Aug-2020].

\bibitem{vuzzer}
\BIBentryALTinterwordspacing
S.~Rawat, V.~Jain, A.~Kumar, L.~Cojocar, C.~Giuffrida, and H.~Bos, ``Vuzzer:
  Application-aware evolutionary fuzzing,'' in \emph{24th Annual Network and
  Distributed System Security Symposium, {NDSS}}, 2017. [Online]. Available:
  \url{https://www.ndss-symposium.org/ndss2017/ndss-2017-programme/vuzzer-application-aware-evolutionary-fuzzing/}
\BIBentrySTDinterwordspacing

\bibitem{debray-scam14}
\BIBentryALTinterwordspacing
B.~Yadegari and S.~Debray, ``Bit-level taint analysis,'' in \emph{2014 IEEE
  14th International Working Conference on Source Code Analysis and
  Manipulation (SCAM)}, 2014, pp. 255--264. [Online]. Available:
  \url{https://doi.ieeecomputersociety.org/10.1109/SCAM.2014.43}
\BIBentrySTDinterwordspacing

\bibitem{angora}
\BIBentryALTinterwordspacing
P.~{Chen} and H.~{Chen}, ``Angora: Efficient fuzzing by principled search,'' in
  \emph{Proceedings of the 2018 IEEE Symposium on Security and Privacy (SP)},
  2018, pp. 711--725. [Online]. Available:
  \url{https://doi.org/10.1109/SP.2018.00046}
\BIBentrySTDinterwordspacing

\bibitem{redqueen}
\BIBentryALTinterwordspacing
C.~Aschermann, S.~Schumilo, T.~Blazytko, R.~Gawlik, and T.~Holz, ``{REDQUEEN:}
  fuzzing with input-to-state correspondence,'' in \emph{Proceedings of the
  26th Annual Network and Distributed System Security Symposium, {NDSS}}, 2019.
  [Online]. Available:
  \url{https://www.ndss-symposium.org/ndss-paper/redqueen-fuzzing-with-input-to-state-correspondence/}
\BIBentrySTDinterwordspacing

\bibitem{WEIZZ}
\BIBentryALTinterwordspacing
A.~Fioraldi, D.~C. D'Elia, and E.~Coppa, ``{WEIZZ: Automatic Grey-Box Fuzzing
  for Structured Binary Formats},'' in \emph{Proceedings of the 29th ACM
  SIGSOFT International Symposium on Software Testing and Analysis (ISSTA
  ’20)}, 2020. [Online]. Available:
  \url{https://doi.org/10.1145/3395363.3397372}
\BIBentrySTDinterwordspacing

\bibitem{SLF}
\BIBentryALTinterwordspacing
W.~You, X.~Liu, S.~Ma, D.~Perry, X.~Zhang, and B.~Liang, ``{SLF}: Fuzzing
  without valid seed inputs,'' in \emph{Proceedings of the 41st International
  Conference on Software Engineering}, ser. ICSE '19, 2019, pp. 712--723.
  [Online]. Available: \url{https://doi.org/10.1109/ICSE.2019.00080}
\BIBentrySTDinterwordspacing

\bibitem{wrapped-intervals}
\BIBentryALTinterwordspacing
J.~A. Navas, P.~Schachte, H.~S{\o}ndergaard, and P.~J. Stuckey,
  ``Signedness-agnostic program analysis: Precise integer bounds for low-level
  code,'' in \emph{Proceedings of the 10th Asian Symposium on Programming
  Languages and Systems}, ser. APLAS '12, 2012, pp. 115--130. [Online].
  Available: \url{https://doi.org/10.1007/978-3-642-35182-2\_9}
\BIBentrySTDinterwordspacing

\bibitem{Pin-PLDI05}
\BIBentryALTinterwordspacing
C.-K. Luk, R.~Cohn, R.~Muth, H.~Patil, A.~Klauser, G.~Lowney, S.~Wallace, V.~J.
  Reddi, and K.~Hazelwood, ``Pin: Building customized program analysis tools
  with dynamic instrumentation,'' ser. PLDI '05.\hskip 1em plus 0.5em minus
  0.4em\relax ACM, 2005. [Online]. Available:
  \url{http://doi.acm.org/10.1145/1065010.1065034}
\BIBentrySTDinterwordspacing

\bibitem{DCNPC-ASIACCS19}
\BIBentryALTinterwordspacing
D.~C. D'Elia, E.~Coppa, S.~Nicchi, F.~Palmaro, and L.~Cavallaro, ``{SoK: Using
  Dynamic Binary Instrumentation for Security (And How You May Get Caught Red
  Handed)},'' in \emph{Proceedings of the 14th ACM ASIA Conference on Computer
  and Communications Security}, ser. ASIACCS '19, 2019. [Online]. Available:
  \url{https://doi.org/10.1145/3321705.3329819}
\BIBentrySTDinterwordspacing

\bibitem{qsym-removed-fuzzbench}
Google, ``{FuzzBench: issue \#131},''
  \url{https://github.com/google/fuzzbench/issues/131}, 2020, [Online; accessed
  20-Aug-2020].

\bibitem{small-files-project}
M.~Bynens, ``{Smallest possible syntactically valid files of different
  types},'' \url{https://github.com/mathiasbynens/small}, 2019, [Online;
  accessed 20-Aug-2020].

\bibitem{jfs-custom-seeds}
D.~Liew, ``{JFS: issue \#4},''
  \url{https://github.com/mc-imperial/jfs/issues/4}, 2019, [Online; accessed
  20-Aug-2020].

\bibitem{libfuzzer}
K.~Serebryany, ``{libFuzzer: a library for coverage-guided fuzz testing},''
  \url{http://llvm.org/docs/LibFuzzer.html}, 2015, [Online; accessed
  20-Aug-2020].

\bibitem{jfs-c-interface}
R.~J. Stinnett, ``{JFS: issue \#22},''
  \url{https://github.com/mc-imperial/jfs/issues/22}, 2019, [Online; accessed
  20-Aug-2020].

\bibitem{aflpp-colorization}
``{CmpLog instrumentation for QEMU inspired by Redqueen},''
  \url{https://aflplus.plus/features/}, 2020, [Online; accessed 20-Aug-2020].

\bibitem{AFLPP-WOOT20}
\BIBentryALTinterwordspacing
A.~Fioraldi, D.~Maier, H.~Ei{\ss}feldt, and M.~Heuse, ``{AFL++: Combining
  incremental steps of fuzzing research},'' in \emph{Proceedings of the 14th
  USENIX Workshop on Offensive Technologies}, ser. WOOT '20, 2020. [Online].
  Available:
  \url{http://www.internetsociety.org/sites/default/files/blogs-media/driller-augmenting-fuzzing-through-selective-symbolic-execution.pdf}
\BIBentrySTDinterwordspacing

\bibitem{aflpp-parallel-mode}
``{Single-system parallelization},''
  \url{https://aflplus.plus/docs/parallel_fuzzing/}, 2020, [Online; accessed
  20-Aug-2020].

\bibitem{COLL-AFL}
\BIBentryALTinterwordspacing
S.~{Gan}, C.~{Zhang}, X.~{Qin}, X.~{Tu}, K.~{Li}, Z.~{Pei}, and Z.~{Chen},
  ``Collafl: Path sensitive fuzzing,'' in \emph{2018 IEEE Symposium on Security
  and Privacy}, ser. SP '18, 2018, pp. 679--696. [Online]. Available:
  \url{http://dx.doi.org/10.1109/SP.2018.00040}
\BIBentrySTDinterwordspacing

\bibitem{AFL-COV}
A.~Fioraldi, ``{afl-qemu-cov},''
  \url{https://github.com/andreafioraldi/afl-qemu-cov}, [Online; accessed
  20-Aug-2020].

\end{thebibliography}
