\PassOptionsToPackage{acronym}{glossaries}

    \input{acronyms}

@Article{Brockschmidt16,

@Article{brockschmidt2016acm,

  groups    = {AProVE},

  groups    = {AProVE, Complexity Tools},

@Article{DBLP:journals/jar/GieslABEFFHOPSS17,

@Article{giesl2017aprove,
  author    = {J{\"{u}}rgen Giesl and Cornelius Aschermann and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Jera Hensel and Carsten Otto and Martin Pl{\"{u}}cker and Peter Schneider{-}Kamp and Thomas Str{\"{o}}der and Stephanie Swiderski and Ren{\'{e}} Thiemann},

  groups    = {AProVE},

  groups    = {AProVE, Complexity Tools},

@Article{meyer21,

@Article{meyer2021tacas,

  title   = {Inferring Expected Runtimes of ProbabilisticInteger Programs Using Expected Sizes},

  title   = {Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes},

  groups    = {CoFloCo},

  groups    = {CoFloCo, Complexity Tools},

  groups    = {CoFloCo},

  groups    = {Complexity Tools},

  groups    = {Partial Evaluation},

  groups    = {Partial Evaluation, Complexity Tools},

}
@InProceedings{termcomp2015,
  author    = {J{\"{u}}rgen Giesl and Fr{\'{e}}d{\'{e}}ric Mesnard and Albert Rubio and Ren{\'{e}} Thiemann and Johannes Waldmann},
  booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
  title     = {Termination Competition (termCOMP 2015)},
  year      = {2015},
  editor    = {Amy P. Felty and Aart Middeldorp},
  pages     = {105--108},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {9195},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/cade/GieslMRTW15.bib},
  doi       = {10.1007/978-3-319-21401-6_6},
  file      = {Full Conference:/home/paradyx/MA/literatur/cade2015full.pdf:PDF},
  groups    = {Competitions},
  timestamp = {Wed, 25 Sep 2019 18:19:14 +0200},
  url       = {https://doi.org/10.1007/978-3-319-21401-6_6},
}
@InProceedings{termcomp2019,
  author    = {J{\"{u}}rgen Giesl and Albert Rubio and Christian Sternagel and Johannes Waldmann and Akihisa Yamada},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}},
  title     = {The Termination and Complexity Competition},
  year      = {2019},
  editor    = {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen},
  pages     = {156--166},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {11429},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/tacas/GieslRSWY19.bib},
  doi       = {10.1007/978-3-030-17502-3_10},
  file      = {Full Conference:/home/paradyx/MA/literatur/tacas2019full.pdf:PDF},
  groups    = {Competitions},
  timestamp = {Fri, 09 Apr 2021 18:45:37 +0200},
  url       = {https://doi.org/10.1007/978-3-030-17502-3_10},
}
@InProceedings{alarcon2017muterm,
  author    = {Beatriz Alarc{\'{o}}n and Ra{\'{u}}l Guti{\'{e}}rrez and Jos{\'{e}} Iborra and Salvador Lucas},
  booktitle = {Proceedings of the Sixth Spanish Conference on Programming and Languages, {PROLE} 2006, Sitges, Barcelona, Spain, October 4-6, 2006},
  title     = {Proving Termination of Context-Sensitive Rewriting with {MU-TERM}},
  year      = {2006},
  editor    = {Paqui Lucio and Fernando Orejas},
  pages     = {105--115},
  publisher = {Elsevier},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {188},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/entcs/AlarconGIL07.bib},
  doi       = {10.1016/j.entcs.2007.05.041},
  groups    = {Complexity Tools},
  timestamp = {Tue, 31 Jan 2023 15:28:53 +0100},
  url       = {https://doi.org/10.1016/j.entcs.2007.05.041},
}
@Online{termcomp2022url,
  groups  = {Competitions},
  title   = {Termination Competition 2022},
  url     = {https://termination-portal.org/wiki/Termination_Competition_2022},
  urldate = {2023-05-09},
  year    = {2022},
}
@InProceedings{frohn2017ifm,
  author    = {Florian Frohn and J{\"{u}}rgen Giesl},
  booktitle = {Integrated Formal Methods - 13th International Conference, {IFM} 2017, Turin, Italy, September 20-22, 2017, Proceedings},
  title     = {Complexity Analysis for Java with AProVE},
  year      = {2017},
  editor    = {Nadia Polikarpova and Steve A. Schneider},
  pages     = {85--101},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {10510},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/ifm/FrohnG17.bib},
  doi       = {10.1007/978-3-319-66845-1_6},
  file      = {Full Conference:/home/paradyx/MA/literatur/ifm2017full.pdf:PDF},
  groups    = {AProVE},
  timestamp = {Fri, 07 Aug 2020 17:57:32 +0200},
  url       = {https://doi.org/10.1007/978-3-319-66845-1_6},
}
@Article{giesel2011rsst,
  author    = {J{\"{u}}rgen Giesl and Matthias Raffelsieper and Peter Schneider{-}Kamp and Stephan Swiderski and Ren{\'{e}} Thiemann},
  journal   = {{ACM} Trans. Program. Lang. Syst.},
  title     = {Automated termination proofs for haskell by term rewriting},
  year      = {2011},
  number    = {2},
  pages     = {7:1--7:39},
  volume    = {33},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/journals/toplas/GieslRSST11.bib},
  doi       = {10.1145/1890028.1890030},
  groups    = {AProVE},
  timestamp = {Wed, 25 Sep 2019 17:52:01 +0200},
  url       = {https://doi.org/10.1145/1890028.1890030},
}
@Article{giesl2022arxiv,
  author     = {J{\"{u}}rgen Giesl and Nils Lommen and Marcel Hark and Fabian Meyer},
  journal    = {CoRR},
  title      = {Improving Automatic Complexity Analysis of Integer Programs},
  year       = {2022},
  volume     = {abs/2202.01769},
  bibsource  = {dblp computer science bibliography, https://dblp.org},
  biburl     = {https://dblp.org/rec/journals/corr/abs-2202-01769.bib},
  eprint     = {2202.01769},
  eprinttype = {arXiv},
  file       = {:/home/paradyx/MA/literatur/giesl2022arxiv.pdf:PDF},
  groups     = {KoAT},
  timestamp  = {Wed, 09 Feb 2022 15:43:35 +0100},
  url        = {https://arxiv.org/abs/2202.01769},

@InProceedings{giesl2022lncs,
  author    = {J{\"{u}}rgen Giesl and Nils Lommen and Marcel Hark and Fabian Meyer},
  booktitle = {The Logic of Software. {A} Tasting Menu of Formal Methods - Essays Dedicated to Reiner H{\"{a}}hnle on the Occasion of His 60th Birthday},
  title     = {Improving Automatic Complexity Analysis of Integer Programs},
  year      = {2022},
  editor    = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Einar Broch Johnsen},
  pages     = {193--228},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {13360},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/birthday/GieslLHM20.bib},
  doi       = {10.1007/978-3-031-08166-8\_10},
  file      = {Full Conference:/home/paradyx/MA/literatur/thelogicofsoftware2022full.pdf:PDF},
  groups    = {KoAT},
  timestamp = {Tue, 18 Oct 2022 22:17:02 +0200},
  url       = {https://doi.org/10.1007/978-3-031-08166-8\_10},
}

1 StaticGroup:CoFloCo\;0\;1\;0xb3e6e6ff\;\;\;;

1 StaticGroup:Complexity Tools\;0\;1\;0xb3e6e6ff\;\;\;;
1 StaticGroup:Competitions\;0\;1\;0x99ccccff\;\;\;;

\section{Conclusion}

\section{Conclusion}\label{sec:conclusion}

\section{Implementation}

\section{Implementation}\label{sec:implementation}

\section{Theory}

\section{Theory}\label{sec:theory}

\section{Preliminaries}

\section{Preliminaries}\label{sec:preliminaries}

\newacronym{smt}{SMT}{Satisfiability Modulo Theory}
\newacronym{ppl}{PPL}{Parma Polyhedra Library}
\newacronym{koat}{KoAT2}{KoAT2} \todo{wrong acronym}
\newacronym{chc}{CHC}{Constraint Horn Clause}
%

\section{Background}
The question if a program terminates is a famous problem at the heart of
computer science known to be undecidable. The so-called \textit{Halting Problem}
is strongly related to the question upper and lower runtime bounds, or the
runtime complexity of a program, is equally non-computable. Nevertheless, the
answers to those questions are very important, since proven termination or small
runtime-complexities are generally desirable in practice. For example a compiler
might want to warn the programmer about faulty code sections that were not
marked explicitly to run indefinitely, or the developer could be forced to prove
the efficiency of his program in critical scenarios. In an ever more complex
world, with ever more complex algorithms, the need for automatic tools arised.
Even though the question for runtime-complexity can not be answered in a general
case, many tools were developed to automatically analyze the complexity of
various programming paradigms as tight and fast as possible.
\cite{giesl2017aprove, montoya2014aplas,alarcon2017muterm,irankfinder2018wst}
Those tools are improved on constantly and they are regularly compared to each
other in the \gls{termcomp}\cite{termcomp2015,termcomp2019}, the goal being to
find as many, as tight bounds for a set of test programs as possible. 
The tests are chosen to represent a large variety of commonly encountered
real-world programs, but also include known-to-be hard-to-solve problems in
order to challenge the competitors and improve their tools. Their collection of
test programs can be found in the \gls{tpdb} which is publicly
available\footnote{\url{https://github.com/TermCOMP/TPDB}}. During the latests
competition in 2022, eleven candidates lined up in twenty-eight
categories\cite{termcomp2022url}. 

\section{Related Works}
\subsection{Background}
\subsection{Related Works}
    Koat was first presented in \cite{brockschmidt2014tacas}
\begin{comment}

\subsection{\acrshort{aprove}, \acrshort{koat}, and \acrshort{loat}}
The \gls{aprove} is developed by \citeauthor{giesl2014ijcar} at RWTH
University\cite{giesl2014ijcar}. \Gls{aprove} is capable of analyzing real-world
programming languages like Java, C, Haskell, Prolog by transforming the given
program into an equivalent \gls{trs} and then analyzing the resulting \gls{trs}
with various different techniques and tools. Explaining every technique used in
\gls{aprove} would go beyond the scope of this thesis. It should only be
mentioned that during analysis parts of the \gls{trs} can be transformed further
into \gls{its} which opens the possibility for many more analysis techniques
typically not available for \gls{trs}. 
The tools LoAT\cite{frohn2022ijcar} and KoAT\cite{brockschmidt2016acm} are also
developed at RWTH University and aim at the finding lower and respectively upper
runtime-complexity and size bounds on integer transition systems. At its core,
KoAT iteratively computes ranking \todo{be more precise}functions to prove upper
bounds, alternating between size and runtime-bounds and thus leveraging the
relation between both to get tight results. Optionally to improve the analysis,
KoAT resorts to refinement techniques, like \gls{mprf} and
\gls{cfr}\cite{giesl2022lncs}. Recently, KoAT was expanded to work on
probabilistic integer programs as well\cite{meyer2021tacas}.
\subsection{iRankFinder}
The tool iRankFinder is another tool taking part in \gls{termcomp}. It converts
\gls{its} into \gls{chc} and uses 
% Hier weiter machen
\section{Goal}
This thesis improves on the latest version of \gls{koat} by reimplementing the
control flow refinement technique of iRankFinder\cite{irankfinder2018wst}
natively in KoAT instead of calling an external library and adapting it to the
paradigm of probabilistic programs. The well-known basics required to understand
this thesis are recapitulated in \Sref{sec:preliminaries}, focusing especially
on constraints, probability, and (probabilistic) integer programs. In
\Sref{sec:theory} the \gls{cfr} techniques from iRankFinder are adapted to
\Gls{pip}, showing the proving the theoretical correctness of the construction.
\Sref{sec:implementation} will focus on the changes made to \gls{koat} and the
challenges met during implementation of the technique in Ocaml. Finally in
\Cref{sec:conclusion} the new version of \gls{koat} will be compared to its
predecessor with regard to the found runtime-complexity and size bounds as well
as the overall computational performance of the tool using the problems from the
\gls{tpdb}. 

\end{comment}

\newacronym{termcomp}{termCOMP}{Termination and Complexity Competition}
\newacronym{aprove}{AProVE}{Automated Program Verification Environment Web Interface}
\newacronym{its}{ITS}{integer transition system}
\newacronym{trs}{TRS}{term rewrite system}
\newacronym{tpdb}{TPDB}{Termination Problems Data Base}
\newacronym{cfr}{CFR}{control-flow refinment}
\newacronym{smt}{SMT}{Satisfiability Modulo Theory}
\newacronym{ppl}{PPL}{Parma Polyhedra Library}
\newacronym{koat}{KoAT}{KoAT\todo{wrong acro}} 
\newacronym{loat}{LoAT}{LoAT\todo{wrong acro}} 
\newacronym{chc}{CHC}{constraint Horn clause}
\newacronym{mprf}{M$\Phi{}$RF}{multi-phase ranking function}
\newacronym{pip}{PIP}{probabilistic integer program}