arxiv.tex

% v2-acmsmall-sample.tex, dated March 6 2012
% This is a sample file for ACM small trim journals
%
% Compilation using 'acmsmall.cls' - version 1.3 (March 2012), Aptara Inc.
% (c) 2010 Association for Computing Machinery (ACM)
%
% Questions/Suggestions/Feedback should be addressed to => "acmtexsupport@aptaracorp.com".
% Users can also go through the FAQs available on the journal's submission webpage.
%
% Steps to compile: latex, bibtex, latex latex
%
% For tracking purposes => this is v1.3 - March 2012

\documentclass[10pt,a4paper]{article} % Aptara syntax

\usepackage{authblk}
\usepackage{breakcites}

% Package to generate and customize Algorithm as per ACM style
\usepackage[ruled]{algorithm2e} 
\renewcommand{\algorithmcfname}{ALGORITHM}
\SetAlFnt{\small}
\SetAlCapFnt{\small}
\SetAlCapNameFnt{\small}
\SetAlCapHSkip{0pt}
\IncMargin{-\parindent}

\newcommand{\fullver}{}
\newcommand{\arxivver}{}
\input{common}

% Document starts
\begin{document}

% Page heads
\markboth{R. Baldoni, E. Coppa, D. C. D'Elia, C. Demetrescu, and I. Finocchi}{A Survey of Symbolic Execution Techniques}

% Title portion
\title{\fontsize{22}{12}\selectfont{A Survey of Symbolic Execution Techniques}}
\author[1]{Roberto Baldoni}
\author[2]{Emilio Coppa}
\author[2]{Daniele Cono D'Elia}
\author[2]{\authorcr Camil Demetrescu}
\author[2]{Irene Finocchi}
\affil[1]{\small\href{http://www.cis.uniroma1.it/}{Cyber Intelligence and Information Security Research Center}, Sapienza University of Rome}
\affil[2]{\href{season-lab.github.io}{SEASON Lab}, Sapienza University of Rome}
\affil[ ]{{\vskip 1pt}\textit {\{baldoni,coppa,delia,demetres\}@dis.uniroma1.it\\ finocchi@di.uniroma1.it}}

\date{\vspace{-4mm}}

\maketitle

\begin{abstract}
Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any backdoor to bypass a program's authentication. One approach would be to test the program using different, possibly random inputs. As the backdoor may only be hit for very specific program workloads, automated exploration of the space of possible inputs is of the essence. Symbolic execution provides an elegant solution to the problem, by systematically exploring many possible execution paths at the same time without necessarily requiring concrete inputs. Rather than taking on fully specified input values, the technique abstractly represents them as symbols, resorting to constraint solvers to construct actual instances that would cause property violations. Symbolic execution has been incubated in dozens of tools developed over the last four decades, leading to major practical breakthroughs in a number of prominent software reliability applications. The goal of this survey is to provide an overview of the main ideas, challenges, and solutions developed in the area, distilling them for a broad audience.
\end{abstract}

% We no longer use \terms command
%\terms{Design, Algorithms, Performance}

%\keywords{Symbolic execution, static analysis, concolic execution, malware analysis}

%\acmformat{Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, and Irene Finocchi, 2016. A survey of symbolic execution techniques.}

\iffalse
\begin{bottomstuff}
Author's addresses: R. Baldoni, E. Coppa, D.C. D'Elia, and C. Demetrescu, Department of Computer, Control, and Management Engineering, Sapienza University of Rome; I. Finocchi, Department of Computer Science, Sapienza University of Rome. 
\end{bottomstuff}
\fi



% \input{intro}
% \myinput{executors}
% \myinput{memory}
% \myinput{environment}
% \myinput{loops}
% \myinput{explosion}
% \myinput{constraints}
% \myinput{binary}
% \input{applications}
% \input{conclusions}
% \input{glossary}

\input{intro}
\myinput{executors}
\myinput{memory}
\myinput{environment}
\myinput{explosion}
\myinput{constraints}
%\myinput{binary}
%\input{applications}
\input{hang}
\input{conclusions}

\myparagraph{Acknowledgements}
%This work is partially supported by a grant of the Italian Presidency of Ministry Council and by the CINI  (Consorzio Interuniversitario Nazionale Informatica) Cybersecurity National Laboratory.
This work is supported in part by a grant of the Italian Presidency of the Council of Ministers and by the CINI (Consorzio Interuniversitario Nazionale Informatica) National Laboratory of Cyber Security.


\input{glossary}

\appendix
\input{tables}
\myinput{binary}
\input{applications}


% Bibliography
%\bibliographystyle{abstract} 
\bibliographystyle{apalike-refs}
\bibliography{symbolic}

% History dates
%\received{--- 2016}{--- XXXX}{---- XXXX}

\end{document}

% End of v2-acmsmall-sample.tex (March 2012) - Gerry Murray, ACM