paper.tex 3.34 KB
Newer Older
Dennis Müller's avatar
init  
Dennis Müller committed
1
2
3
4
5
6
7
8
9
10
11
12
\documentclass[orivec]{llncs}

\usepackage[utf8]{inputenc}
\usepackage{url}
%\usepackage{tipa}
\usepackage{amsmath,amssymb,amstext}
\usepackage{graphicx,stmaryrd,mathabx,MnSymbol,tabularx,mathtools}
\usepackage[normalem]{ulem}
\usepackage{array}
\usepackage{mdframed}
\usepackage{wrapfig}
\usepackage{paralist}
Michael Kohlhase's avatar
Michael Kohlhase committed
13
\usepackage{xspace}
Dennis Müller's avatar
init  
Dennis Müller committed
14
15
16
17
18
19
%\usepackage{appendix}

\usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}
% \addbibresource{../../fr-macros/rabe.bib}
% \addbibresource{../../fr-macros/systems.bib}
% \addbibresource{../../fr-macros/pub_rabe.bib}
Michael Kohlhase's avatar
Michael Kohlhase committed
20
21
22
23
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
Dennis Müller's avatar
init  
Dennis Müller committed
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
  \iftoggle{bbx:doi}
    {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
    {}%
  \newunit\newblock
  \iftoggle{bbx:eprint}
    {\usebibmacro{eprint}}
    {}%
  \newunit\newblock
  \iftoggle{bbx:url}
    {\usebibmacro{url+urldate}}
    {}}

\setlength{\hfuzz}{3pt} \hbadness=10001
\setcounter{tocdepth}{2} % for pdf bookmarks
\usepackage{xcolor}
Michael Kohlhase's avatar
Michael Kohlhase committed
41
42
\usepackage{listings}
\lstset{columns=fullflexible,basicstyle=\sf}
Dennis Müller's avatar
init  
Dennis Müller committed
43
44
45
46
47
48
49
50
51
\usepackage[bookmarks,linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksopen,bookmarksnumbered]{hyperref}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% local macros and configurations

% \usepackage{../../fr-macros/basics}
% \usepackage[llncs]{../../fr-macros/theorems}
% \input{macros}

Michael Kohlhase's avatar
Michael Kohlhase committed
52
53
54
55
56
\def\cB{\mathcal{B}}
\def\cL{\mathcal{L}}
\def\defemph{\textbf}
\def\MMT{\textsf{MMT}\xspace}
\usepackage[show]{ed}
Dennis Müller's avatar
init  
Dennis Müller committed
57
58
59
\newif\ifshort\shorttrue

\pagestyle{plain} % remove for final version
Michael Kohlhase's avatar
Michael Kohlhase committed
60
61
62
63

\author{Dennis Müller\inst{1} \and Florian Rabe\inst{1,2} \and Michael Kohlhase\inst{1}}
\institute{Computer Science, FAU Erlangen-N\"urnberg\and LRI, Universit\'e Paris Sud}

Dennis Müller's avatar
init  
Dennis Müller committed
64
65
66
67
68
69
70
\begin{document}

%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\


\title{Alignment Finding}
\maketitle
Michael Kohlhase's avatar
Michael Kohlhase committed
71
72
73
74
\begin{abstract}\ednote{tbw}
\end{abstract}

\setcounter{tocdepth}{2}\tableofcontents\newpage
Dennis Müller's avatar
Dennis Müller committed
75
76
77
78
79
80
81
82

\section{Introduction}\label{sec:intro}\input{intro}

\section{Preliminaries}\label{sec:prelim}\input{prelim}

\section{Viewfinder}\label{sec:viewfinder}\input{viewfinder}

\section{Extended Use Case}\label{sec:usecase}\input{usecase}
Dennis Müller's avatar
init  
Dennis Müller committed
83

Michael Kohlhase's avatar
Michael Kohlhase committed
84
\section{Conclusion}\label{sec:concl}
Dennis Müller's avatar
init  
Dennis Müller committed
85

Michael Kohlhase's avatar
Michael Kohlhase committed
86
87
\subsubsection*{Acknowledgements}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
Michael Kohlhase's avatar
Michael Kohlhase committed
88
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Michael Kohlhase's avatar
Michael Kohlhase committed
89
Open Archive for Formalizations (KO 2428/13-1).
Dennis Müller's avatar
init  
Dennis Müller committed
90
91
92
93
94
95
96
97
98
99
100
101
102
103

\renewcommand*{\bibfont}{\small}
\printbibliography

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:


%  LocalWords:  inst maketitle formalization defs well-formedness textsf sec:impl impl
%  LocalWords:  sec:conc conc Universit printbibliography ednote Internalizing newpage
Michael Kohlhase's avatar
Michael Kohlhase committed
104
105
106
107
%  LocalWords:  ifshort sec:relwork relwork renewcommand bibfont tbw setcounter tocdepth
%  LocalWords:  tableofcontents defemph compactenum emptyset newpart compactitem lstset
%  LocalWords:  centering aboveskip 0pt,belowskip hline lstlisting mathescape rightarrow
%  LocalWords:  vdash baseset sec:concl subsubsection Formalizations