aplas2021.tex 2.74 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
\documentclass[runningheads,orivec]{llncs}

%% Packages
\usepackage{../latex/packages}

%% Macros
% for comments
\newcommand{\zhilin}[1]{\todo[color=blue!20,linecolor=black!60,size=\scriptsize]{Z: #1}}
\newcommand{\mihaela}[1]{\todo[color=green!20,linecolor=black!60,size=\scriptsize]{M: #1}}
% others
\input{../latex/commands.tex}

%% Title
%\title{Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions}
%\title{Decision Procedures for Heap-lists}
Mihaela SIGHIREANU's avatar
Mihaela SIGHIREANU committed
16
\title{Deciding Separation Logic with Heap Lists}
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
%%
\author{%
Double Blind
%Wanyun Su\inst{2} \and
%Zhilin Wu\inst{2}\orcidID{0000-0003-0899-628X} \and
%Mihaela Sighireanu\inst{1}\orcidID{0000-0002-1925-089X}
}
\institute{%
Double Blind
%   State Key Laboratory of Computer Science, \\
%   Institute of Software, Chinese Academy of Sciences, China \\
%   %\email{wuzl@ios.ac.cn}
%\and
%   LMF, ENS Paris-Saclay, University Paris-Saclay and CNRS, France
%    %\email{firstname.lastname@labmf.fr}
}
\date{}
%\authorrunning{W. Su, Z. Wu and M. Sighireanu}
35
\authorrunning{Double Blind}
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

\setlength{\parskip}{0eX}

\begin{document}

%------------------------------------------------------------------------------

\maketitle
\sloppy

%------------------------------------------------------------------------------
%\vspace{-4mm}
\input{abs.tex}

%------------------------------------------------------------------------------
%\vspace{-6mm}
\input{intro.tex}

%------------------------------------------------------------------------------
%% Overview of problems when reasoning about DMA
%\vspace{-2mm}
\input{overview.tex}

%------------------------------------------------------------------------------
%% Definition of the logic
%\vspace{-2mm}
\input{logic-hls.tex}

%------------------------------------------------------------------------------
%% The decision procedures for the satisfiability
%\vspace{-2mm}
\input{sat-hls.tex}

%------------------------------------------------------------------------------
%% The decision procedures for the satisfiability for wfid
%\input{sat-wfid.tex}

%------------------------------------------------------------------------------
%% The decision procedures for the entailment
%\vspace{-2mm}
\input{entail-hls.tex}

%------------------------------------------------------------------------------
%\vspace{-2mm}
\input{experiments.tex}

%------------------------------------------------------------------------------
%\vspace{-2mm}
\input{conclusion.tex}

%\newpage
%------------------------------------------------------------------------------
\bibliographystyle{../latex/splncs04}
\bibliography{../bibs/biblio}

\newpage
\appendix
%\section{Appendixes}
\input{app-sat-hls.tex}
%\input{app-ent-hls.tex}

%% temporary
%\newpage
%\setcounter{tocdepth}{3}
%\tableofcontents

\end{document}