\setbinding{10mm} 

\setbinding{5mm} 

In \Cref{ch:theory} the method of control-flow refinement via partial evaluation
was expanded to \acrfull{pip}. The method is proven to be sound for \gls{pip}s
and can be used to refine a \gls{pip} when classical analysis fails at finding
tight runtime bounds. In \Cref{ch:implementation} we have presented a new
implementation of partial evaluation on probabilistic programs and successfully
inferred tighter expected runtime complexity bounds for two probabilistic
examples.

transition in the run. The runtime runtime complexity of a program is a special

transition in the run. The runtime complexity of a program is a special

similarly to the worst-case expected runtime complexity. However, answering this

similarly to the worst-case expected runtime complexity. However,  proving this

good as iRankFinder on a small number of programs in the test sets. Since we
tried to mirror the behaviour of iRankFinder as close as possible, there were
most probably mistakes made during implementation. For example, our
implementation of the heuristics deviate from iRankFinders implementation or the
selecting the feedback set for locations had an unexpected impact on the
analysis. In any case, the worsened analysis results warrant further
investigation. Until then, \gls{koat} can keep using iRankFinder for

good as iRankFinder on a small number of programs in the test sets. We tried to
mirror the behaviour of iRankFinder as closely as possible, but probably
deviated from it a significant way. For example, our implementation might
compute slightly different properties heuristically than iRankFinder's
implementation, or selecting the feedback set for locations had an unexpected
impact on the analysis. In any case, the worsened analysis results warrant
further investigation. Until then, \gls{koat} can keep using iRankFinder for

to Aprons representation of polyhedra. There is probably room for improvement,
by reducing the number of conversions to and from apron. Furthermore, the

to Aprons representation of polyhedra. There is room for improvement by
reducing the number of conversions to and from apron. Furthermore, the

the unolding and once after the unfolding during abstraction even though the

the unfolding and once after the unfolding during abstraction even though the

previous analysis better into account.

previous analysis into account in a more favourable way.

A last idea, that came up during the writing of this thesis is some sort of

A last idea that came up during the writing of this thesis, is some sort of

might be interesting for some other class of programs, we haven't considered in

might be interesting for some other class of program, we have not considered in

\section{Conclusion}\label{sec:conclusion} 
In \Cref{ch:theory} the method of control-flow refinement via partial evaluation
was expanded to \gls{pip}. The method is proven to be sound for \gls{pip} and
can be used to refine a \gls{pip} when classical analysis fails at finding tight
runtime bounds. In \Cref{ch:implementation} we have presented a new
implementation of partial evaluation on probabilistic programs and successfully
inferred tighter expected runtime complexity bounds for an example \gls{pip}. To
the best of our knowledge, we applied partial evaluation for the first time in a
complexity analysis frame work for probabilistic programs.

\section{Conclusion}\label{sec:conclusion}
Considering our goals, it was successfully proven in theory that partial
evaluation can be adapted to \glspl{pip}. The control-flow refinement technique
can be used when searching expected runtime complexity bounds of \glspl{pip}
since the expected runtime complexity bounds are preserved during partial
evaluation. With our new implementation, we successfully improved the runtime
performance of \gls{koat} during analysis of non-probabilistic integer programs.
In the future, our implementation can be used to replace iRankFinder, which is
used as a black-box at the moment. Furthermore, we have demonstrated that our
implementation for \glspl{pip} can be integrated into \gls{koat}'s analysis of
probabilistic integer programs and that tighter expected runtime complexity
bounds can be found on some programs. To the best of our knowledge, we applied
partial evaluation for the first time in a complexity analysis frame work for
probabilistic integer programs.

localised property-based abstraction as introduced in \Cref{ch:theory}. In
\Sref{sec:implementation} we describe the implementation using pseudo-code. We
will mostly focus on the practical aspects of the partial evaluation.
\Sref{sec:technical_details} will briefly describe the technical details of the
implementation. Finally, in \Sref{sec:performance} we will analyse the
performance of the new implementation.

localised property-based abstraction as introduced in \Cref{ch:theory}. We
extend \gls{koat}'s analysis of non-probabilistic programs with a new
implementation of control-flow refinement via partial evaluation and implement
partial evaluation on probabilistic programs. In \Sref{sec:implementation} we
describe the implementation using pseudo-code. We will mostly focus on the
practical aspects of the partial evaluation. \Sref{sec:technical_details} will
briefly describe the technical details of the implementation. Finally, in
\Sref{sec:performance} we will analyse the performance of the new
implementation.

graph is finite. The naive approach to assert this property, is to use a global

graph is finite. The naive approach to assert this property is to use a global

which require a call to the \gls{smt}-solver. This call is expensive and as was
demonstrated in Example \ref{ex:global_abstr}, a global abstraction function
does not yield the smallest partial evaluations, which makes successive analysis
unnecessarily slow. 

which require a call to an \gls{smt}-solver in \gls{koat}. This call is
expensive and as was demonstrated in Example \ref{ex:global_abstr}, a global
abstraction function does not yield the smallest partial evaluations, which
makes successive analysis unnecessarily slow. 

In our implementation, we detect loops with the algorithm described by

In our implementation, loops are detected with the algorithm described by

    Given a finite collection of finite sets $S = \{S_1, \dots, S_n\}$, where
    each $S_i \subseteq U$ for some set $U$, find a minimal set $R$ such that
    $R\intersect S_i \neq \emptyset$ for all $i = 1,\dots,n$.

    For a given finite collection of finite sets $S = \{S_1, \dots,S_n\}$, where
    each $S_i \subseteq U$ for some finite set $U$, find a minimal set $R$ such
    that $R\intersect S_i \neq \emptyset$ for all $i = 1,\dots,n$.

    {}{\sum_{i=1}^{N} x_{\ell_i}\label{eq:lip1-goal}}{\label{eq:ilp-vfs}}{}

    {}{\sum_{i=1}^{N} x_{\ell_i}\label{eq:ilp1-goal}}{\label{eq:ilp-vfs}}{}

selected, and the optimisation goal \eqref{eq:ilp-vfs} minimises the number of

selected, and the optimisation goal \eqref{eq:ilp1-goal} minimises the number of

During \gls{koat}s analysis of a program size and runtime-complexity bounds for

During \gls{koat}s analysis of a program, size and runtime complexity bounds for

runtime-complexity bounds for a transition, the transition is added to a set of

runtime complexity bounds for a transition, the transition is added to a set of

    \KwResult{A PIP $\Prog'$ with equal runtime-complexity bounds.}

    \KwResult{A PIP $\Prog'$ with equal runtime complexity bounds.}

and handling polyhedra we recurred \gls{apron}\cite{apron} and the

and handling polyhedra we recur to \gls{apron}\cite{apron} and the

used by other tools in the future, that want to profit from partial evaluation
on probabilistic programs. 

used by other tools that want to profit from partial evaluation on probabilistic
programs in the future. 

The evaluation on sub-\gls{scc} was integrated into \gls{koat}s analysis similar
to iRankFinder as described in \cite{giesl2022lncs}, possibly replacing the old
implementation in the future. The analysis command was expanded with new
settings, which allow to select the various parameters of the evaluation, such
the selection of locations for abstraction.

The evaluation on sub-\gls{scc} was integrated into \gls{koat}s analysis of
classical programs similar to iRankFinder as described in \cite{giesl2022lncs},
possibly replacing the old implementation in the future. The analysis command
was expanded with new settings, which allow to select the various parameters of
the evaluation, such as the selection of locations for abstraction.
Unfortunately, for probabilistic programs we were not able to integrate the
sub-\gls{scc} level implementation into the analysis due to technical problems.
The current implementation uses an extensive typing system that asserts that
partial evaluation cannot be used with probabilistic programs and we were not
able to change those constraints in \gls{koat}s source-code without rewriting
and restructuring major parts of the analysis, which went beyond the scope of
this thesis. Furthermore, the probabilistic analysis underwent a full rewrite
during the writing of this thesis by its developers, making the task at hand
even harder to fulfill. However, the implementation we provide should be
reasonably easy to integrate, for someone who has experience dealing with
\gls{koat}s typing system.

polynomial and exponential runtime-complexity bounds, as well as the average

polynomial and exponential runtime complexity bound, as well as the average

        functions. \cite{giesl2022lncs} No control-flow refinement is used.

        functions \cite{giesl2022lncs}. No control-flow refinement is used.

        depth used in competitions.\cite{giesl2022lncs} Still, no

        depth used in competitions \cite{giesl2022lncs}. Still, no

        the maximum depth of linear ranking functions to $\textit{mdepth} = 1$.
        The control-flow refinement is done by calling iRankFinder as a

        the maximum depth of multi-phase ranking functions to $\textit{mdepth} =
        1$. The control-flow refinement is done by calling iRankFinder as a

well. The average analysis time of programs where a finite runtime-bound is
found shortens by 0.96 seconds from 5.10 seconds to 4.14 seconds without
\glspl{mprf}; and by 1.93 seconds from 5.74 seconds to 3.81 seconds with

well. The average analysis time of programs where a finite runtime complexity
bound is found shortens by 0.96 seconds from 5.10 seconds to 4.14 seconds
without \glspl{mprf}; and by 1.93 seconds from 5.74 seconds to 3.81 seconds with

This worsened behaviour needs further investigation. We suspect there to be
either a bug in the implementation or that the properties are not optimally
chosen. Besides, there is certainly room for performance optimisation in the new
implementation.

This worsened behaviour needs further investigation.

The implementation for probabilistic programs was done on a 

Due to the missing integration into the full analysis of probabilistic programs,
the implementation for probabilistic programs was evaluated on two cases.
Instead of using sub-\gls{scc} level control-flow refinement, we partially
evaluate the entire program and then feed the results to the probabilistic
analysis. 
Our first test was done with the example program $\Prog_3$ studied in
\Cref{ch:introduction} and \Cref{ch:theory}. The full partial evaluation yields
the same program as the theoretically conjectured partial evaluation of Example
\ref{ex:localized_pba}. For the original program, \gls{koat} failed at finding
finite expected runtime complexity bounds. After the partial evaluation,
\gls{koat} successfully finds a quadratic expected runtime complexity bound
$18y^2 + 524y+ 543 \in \mathcal{O}(n^2)$. 
Our second test, addresses multiphase-loops in probabilistic programs.
\gls{mprf} have a very similarly advantage as partial evaluation when
determining the runtime of loops where the loop implicitly has multiple phases.
However, probabilistic ranking functions are lacking this capabilities, hence
rendering partial evaluation on probabilistic programs even more powerful. We
demonstrate it with our second test program $P_5$ displayed in
\fref{fig:splitting-loop}. The loops at $\ell_1$ have two phases. In the first
phase $y$ is incremented up to $z$, and in the second phase $x$ in decremented
until it reaches a value less than zero. On non-probabilistic programs, this
behaviour could be bounded using a single \gls{mprf} at $\ell_1$. Probabilistic
ranking functions cannot bound the runtime complexity of this loop and
\gls{koat} cannot find a finite expected runtime complexity bound for this
program. After a full partial evaluation with our implementation the program is
transformed into an equivalent program, and \gls{koat} finds the linear
expected runtime complexity bound $12y + 12z + 24x + 47/2 \in \mathcal{O}(n)$.

\begin{figure}
    \centering
    \input{figures/ch4_p5_program}
    \caption{The \gls{pip} $\Prog_5$ with a multiphase-loop at $\ell_1$ and a
    hard to detect expected runtime complexity bound.
    \label{fig:splitting-loop}}
\end{figure}
We successfully demonstrated that partial evaluation of \gls{pip}s works and it
can be used to find tighter expected runtime complexity bounds with \gls{koat}.
% \begin{figure}
%     \centering
%     \input{figures/ch4_p5_pe}
%     \caption{The partial evaluation of the entire \gls{pip} $\Prog_5$. \label{fig:splitting-loop-pe}}
% \end{figure}

    $\varfpi{n} = \simu(\varf) = c'_0c'_1\cdots{}c'_n \in \fpath_{\Prog'}$ with:

    $\varfpi{n} = \simu_{\Prog,S,T}(\varf) = c'_0c'_1\cdots{}c'_n \in \fpath_{\Prog'}$ with:

    t_\text{in},s_0)$. Set $\varfpi{0} = c'_0 = \simu(\varf) = (\langle

    t_\text{in},s_0)$. Set $\varfpi{0} = c'_0 = \simu_{\Prog,S,T}(\varf) = (\langle

    a finite prefix $\varfpi{n} = \simu(f_n) = c'_0\dots{}c'_{n} \in

    a finite prefix $\varfpi{n} = \simu_{\Prog,S,T}(f_n) = c'_0\dots{}c'_{n} \in

    finite prefix $\varfpi{{}n+1} =\simu(f_{n+1})= \simu(f_n)c'_{n+1}$ to 

    finite prefix $\varfpi{{}n+1} =\simu_{\Prog,S,T}(\varff_{n+1})= \simu_{\Prog,S,T}(\varff_n)c'_{n+1}$ to 

Lemma \ref{lem:constrfleq} implies that $\simu(\varf)\in\fpath_{\Prog'}$ is
admissible for any admissible finite prefix $f \in \fpath_\Prog$.

Lemma \ref{lem:constrfleq} implies that
$\simu_{\Prog,S,T}(\varf)\in\fpath_{\Prog'}$ is admissible for any admissible
finite prefix $f \in \fpath_\Prog$.

                &\text{if } \varf' = \simu(\varf(\ell,t,s)) = \dots c'_n, \\
                &\scheduler(c'_n) = (g, \tilde{s})\text{, and } g \neq g_\bot

                &\text{if } \varf' = \simu_{\Prog,S,T}(\varf(\ell,t,s)) = \dots
                c'_n, \scheduler(c'_n) = (g, \tilde{s})\text{, and }\\ &g \neq
                g_\bot,
            \end{aligned}\\
            (g^*, \tilde{s}^*) & \begin{aligned}
                &\text{if } \simu_{\Prog,S,T}(\varf(\ell,t,s)) = \dots c'_n,
                \scheduler(c'_n) = (g, \tilde{s}), \\ &g = g_\bot \text{, and }
                g^* \in \GTPout(\ell), \text{ and } \tilde{s}^* \models
                \tau_{g^*} \text { exists,}

    \begin{rem}
        Since all general transitions have more restrictive guards then their
        originals, it is possible that a location $\ell$ a general transition
        with a satisfiable guard exists in $\Prog$ whereas the guards of all
        general transitions at a location $\langle \ell, \varphi\rangle$ cannot
        be satisfied by the scheduler. In that case, the new scheduler selects
        any one of the valid general transitions $g^*$ and a matching assignment
        $\tilde{s}^*$. As before, this doesn't matter since those
        configurations can never be reached by an admissible run.
    \end{rem}

    prefix $f \in \fpath_\Prog'$ with probability $\prSs(\varf) > 0$ there
    exists a finite prefix $\varf' \in \fpath_\Prog$ for which 

    prefix $f = \dots (\langle\ell_n, \varphi_n\rangle, t_n, s_n) \in
    \fpath_{\Prog'}$ with probability
    $\prSs(\varf) > 0$ there exists a finite prefix $\varf' = \dots
    (\ell_n,\bar{t}_n,s_n) \in \fpath_\Prog$ for which 

    initial configuration with non-zero probability $\prSs(f_0) = 1$. We set
    $\varfpi{0} = c'_0 = (\ell_0, t_\text{in}, s_0)$ which is by construction the
    only valid starting configuration of $\Prog'$ with $\prSns(c'_0) = 1$.

    initial configuration with non-zero probability $\prSs(\varff_0) = 1$. We
    set $\varfpi{0} = c'_0 = (\ell_0, t_\text{in}, s_0)$ which is by
    construction the only valid starting configuration of $\Prog'$ with
    $\prSns(c'_0) = 1$.

    \in \N$ be an admissible prefix with probability $\prSs(f_{n+1})>0$, then
    $f_n = c_0\dots{}c_{n}$ of length $n$ is also admissible with $\prSs(f_n) >
    0$. By induction hypothesis a finite prefix $\varfpi{n}  = c'_0\dots{}c'_{n}
    \in \fpath_{\Prog}$ of equal length and probability exists.

    \in \N$ be an admissible prefix with probability $\prSs(\varff_{n+1})>0$,
    then $f_n = c_0\dots{}c_{n}$ of length $n$ is also admissible with
    $\prSs(\varff_n) > 0$. By induction hypothesis a finite prefix $\varfpi{n}
    = c'_0\dots{}c'_{n} \in \fpath_{\Prog}$ of equal length and probability
    exists. Additionally $c_n = (\langle\ell_n,\varphi\rangle, \_, s_n)$ and
    $c'_n = (\ell_n, \_, s_n)$.

    \textbf{Case 2}: $g = g_\bot$. In that case the constructed scheduler
    selects $\scheduler'(c'_{n+1}) = (g_bot,s)$ as well. This is correct
    because every outgoing general transition of $\Prog$ at $\ell$ was unfolded
    or copied and added to the partial evaluation with more restrictive guards.
    Hence, no general transition in $\Prog$ is satisfiable.

    \textbf{Case 2}: $g = g_\bot$. By construction of the unfolding the $s_n
    \models \varphi_n$ and because $s_n \not\models \varphi \land \tau_g =
    \varphi \land \tau_{\bar{g}}$ for any general transition $g \in
    \GTPnout(\langle\ell_n, \varphi_n\rangle)$, there cannot be any general
    transition $g' \in \GTPout$ for which $s_n \models \tau_{g'}$. The newly
    constructed scheduler selects $\scheduler'(c'_{n+1}) = (g_\bot,s)$ as well. 

        \prSs(f_nc_{n+1}) = prSns(f'_{n+1}c'_{n+1}) 

        \prSs(\varff_nc_{n+1}) = \prSns(\varfpi{n+1}c'_{n+1}) 

    \todo{ Beweis ist noch unsauber}

    Hanna and Thibaud, I would like to express my deepest gratitude for your

    Hanna and Thibaud, I want to express my deepest gratitude for your