% TeX root = main.tex

\begin{titlingpage}
    \newlength{\logoheight}	\setlength{\logoheight}{5cm}
    \setlength{\droptitle}{-3em}
    
    \renewcommand{\maketitlehooka}{%
        \begin{center}
            {\Large Rheinisch-Westfälische Technische Hochschule Aachen\par\noindent}
            Lehr- und Forschungsgebiet Informatik 2\par\noindent Programmiersprachen und Verifikation\\
            Prof. Dr. Jürgen Giesl\\
            \vspace{\logoheight}
            %\includegraphics[height=\logoheight]{PETs4DS.pdf}\\
            \vspace*{1em}
            {\LARGE\scshape Master's Thesis}
            \vspace*{1.5em}
        \end{center}
    }
    \pretitle{\begin{center}\bfseries\HUGE\color{rwth-75}}
        \title{Control-Flow Refinement in a Framework for Automated (Probabilistic) Complexity Analysis}
    \posttitle{\end{center}\vskip 4em}
    
    \preauthor{\begin{center}\Large}
        \author{Yoann Maurice Kehler}
    \postauthor{\end{center}\vskip 2em}
    
    \predate{\begin{center}\Large}
    \date{\today}
    \postdate{\end{center}\vskip 2em}

    \renewcommand{\maketitlehookd}{%
        \vfill
        \centerfloat
        \begin{tabular}{ll}
            \color{rwth}\nth{1} Supervisor	& Prof. Jürgen Giesl\\
            \color{rwth}\nth{2} Supervisor 	& Prof. Erika Ábrahám\\	
            \color{rwth} Advisor		& Nils Lommen, MSc\\
            \color{rwth} Advisor		& Eleanore Meyer, MSc\\
        \end{tabular}
    }
    \calccentering{\unitlength}
    \begin{adjustwidth*}{\unitlength}{-\unitlength}
        \maketitle
    \end{adjustwidth*}
\end{titlingpage}

\begin{abstract}
    \acrshort{koat} is an automatic complexity analysis tool for integer
    programs, which was recently extended to the analysis of probabilistic
    integer programs. Currently, \acrshort{koat} applies so-called control-flow
    refinement via partial evaluation to classic programs by calling the tool
    iRankFinder externally. In this thesis, we extend partial evaluation to
    probabilistic programs. A partially evaluated probabilistic integer program
    has the same expected runtime complexity as the original program. However,
    the transformed program might be easier to analyse. The new algorithm is
    implemented natively in \acrshort{koat} and it is integrated into the
    existing analysis algorithm modular and on demand. Our evaluation shows that
    the native implementation is faster on classical programs. Furthermore, the
    new implementation also infers tighter runtime complexity bounds for some
    probabilistic programs.
\end{abstract}

\cleardoublepage

\begin{vplace}
    \textit{
    Hanna and Thibaud, I want to express my deepest gratitude for your
    continuous encouragement and assistance. Your unwavering belief in my
    abilities and your willingness to lend a helping hand during challenging
    times have been instrumental in the successful completion of this thesis.
    Thank you, from the bottom of my heart.
    }
\end{vplace}

\maxtocdepth{section}
\cleardoublepage

\cleardoublepage
\tableofcontents