-
Notifications
You must be signed in to change notification settings - Fork 10
/
main.tex
159 lines (133 loc) · 6.84 KB
/
main.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
% 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 => "[email protected]".
% 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[prodmode,acmcsur]{acmsmall} % Aptara syntax
% 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}
% Metadata Information
\acmVolume{0}
\acmNumber{0}
\acmArticle{0}
\acmYear{0000}
\acmMonth{0}
% Copyright
%\setcopyright{acmcopyright}
%\setcopyright{acmlicensed}
%\setcopyright{rightsretained}
%\setcopyright{usgov}
%\setcopyright{usgovmixed}
%\setcopyright{cagov}
%\setcopyright{cagovmixed}
\input{common}
% DOI
\doi{0000001.0000001}
%ISSN
\issn{1234-56789}
% 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{A Survey of Symbolic Execution Techniques\\}
\author{ROBERTO BALDONI
\affil{\href{http://www.cis.uniroma1.it/}{Cyber Intelligence and Information Security Research Center}, Sapienza}
EMILIO COPPA
\affil{\href{http://season-lab.github.io}{SEASON Lab}, Sapienza University of Rome}
DANIELE CONO D'ELIA
\affil{\href{http://season-lab.github.io}{SEASON Lab}, Sapienza University of Rome}
CAMIL DEMETRESCU
\affil{\href{http://season-lab.github.io}{SEASON Lab}, Sapienza University of Rome}
IRENE FINOCCHI
\affil{\href{http://season-lab.github.io}{SEASON Lab}, Sapienza University of Rome}
}
% NOTE! Affiliations placed here should be for the institution where the
% BULK of the research was done. If the author has gone to a new
% institution, before publication, the (above) affiliation should NOT be changed.
% The authors 'current' address may be given in the "Author's addresses:" block (below).
% So for example, Mr. Abdelzaher, the bulk of the research was done at UIUC, and he is
% currently affiliated with NASA.
\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}
%\begin{comment}
\begin{CCSXML} % http://dl.acm.org/ccs.cfm
<ccs2012>
<concept>
<concept_id>10011007.10010940.10010992.10010998.10010999</concept_id>
<concept_desc>Software and its engineering~Software verification</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10010940.10010992.10010998.10011001</concept_id>
<concept_desc>Software and its engineering~Dynamic analysis</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011074.10011099.10011102.10011103</concept_id>
<concept_desc>Software and its engineering~Software testing and debugging</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10002978.10003022</concept_id>
<concept_desc>Security and privacy~Software and application security</concept_desc>
<concept_significance>100</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Software and its engineering~Software verification}
%\ccsdesc[300]{Software and its engineering~Dynamic analysis}
\ccsdesc[300]{Software and its engineering~Software testing and debugging}
\ccsdesc[100]{Security and privacy~Software and application security}
%\end{comment}
% We no longer use \terms command
%\terms{Design, Algorithms, Performance}
\keywords{Symbolic execution, static analysis, concolic execution, software testing}
\acmformat{Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu,
and Irene Finocchi, 2016. A survey of symbolic execution techniques.}
% At a minimum you need to supply the author names, year and a title.
% IMPORTANT:
% Full first names whenever they are known, surname last, followed by a period.
% In the case of two authors, 'and' is placed between them.
% In the case of three or more authors, the serial comma is used, that is, all author names
% except the last one but including the penultimate author's name are followed by a comma,
% and then 'and' is placed before the final author's name.
% If only first and middle initials are known, then each initial
% is followed by a period and they are separated by a space.
% The remaining information (journal title, volume, article number, date, etc.) is 'auto-generated'.
\begin{bottomstuff}
%This work is supported by the National Science Foundation, under grant CNS-0435060, grant CCR-0325197 and grant EN-CS-0329609.
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.
This work is supported in part by a grant of the Italian Presidency of the Council of Ministers and by the CINI National Laboratory of Cyber Security. % (Consorzio Interuniversitario Nazionale Informatica)
\end{bottomstuff}
\maketitle
\input{intro}
\myinput{executors}
\myinput{memory}
\myinput{environment}
\myinput{explosion}
\myinput{constraints}
\input{hang}
\input{conclusions}
% Bibliography
%\bibliographystyle{abstract}
\bibliographystyle{ACM-Reference-Format-Journals}
\bibliography{symbolic}
% History dates
%\received{--- 2016}{--- XXXX}{---- XXXX}
\end{document}
% End of v2-acmsmall-sample.tex (March 2012) - Gerry Murray, ACM