@InProceedings{lommen2022twn,
  author    = {Nils Lommen and Fabian Meyer and J{\"{u}}rgen Giesl},
  booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings},
  title     = {Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops},
  year      = {2022},
  editor    = {Jasmin Blanchette and Laura Kov{\'{a}}cs and Dirk Pattinson},
  pages     = {734--754},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {13385},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl    = {https://dblp.org/rec/conf/cade/LommenMG22.bib},
  doi       = {10.1007/978-3-031-10769-6_43},
  timestamp = {Mon, 24 Oct 2022 16:36:35 +0200},
  url       = {https://doi.org/10.1007/978-3-031-10769-6_43},
}

The analysis techniques used, such as \acrfullpl{mprf} and \cite{twn}, have

The analysis techniques used, such as \acrfullpl{mprf} and \cite{lommen2022twn}, have

        \unfold_\alpha(\langle l,\varphi\rangle, t) = (\langle \ell,

        \unfold_\alpha(\langle \ell,\varphi\rangle, t) = (\langle \ell,

    Let $\Psi_{\ell_0},\dots,\Psi_{\ell_n} \in (2^\C \union \{\bot\})$ be

    Let $\Psi_{\ell_0},\dots,\Psi_{\ell_n} \subseteq (2^\C \union \{\bot\})$ be

    Let $G^*_{\Prog,S}$ be the evaluation graph of a \gls{pip} $\Prog$ for any

    Let $G^*_{\Prog,S,T}$ be the evaluation graph of a \gls{pip} $\Prog$ for any

    \in E(G^*_{\Prog,\alpha})$ one can find a unique transition denoted as

    \in E(G^*_{\Prog,S,T})$ one can find a unique transition denoted as

    Let $S$ be a localised abstraction function and $T \subseteq \T_Prog$ The

    Let $S$ be a localised abstraction function and $T \subseteq \TP$ The

        graph $G_{\Prog,S}^*$ is infinite. 

        graph $G_{\Prog,S,T}^*$ is infinite. 

        pairwise different versions in $G_{\Prog,S}^*$ as well.

        pairwise different versions in $G_{\Prog,S,T}^*$ as well.

Let $\GT_{G^*_{\Prog,\alpha}}$ be the set of general transitions in the partial
evaluation graph $G^*_{\Prog,\alpha}$ where every general transition $g \in
\GT_{G^*_{\Prog,\alpha}}$ was added by the unfolding of a unique general
transition $g' \in \GT_Prog$. We call $\bar{g} = g'$, similar to Lemma

Let $\GT_{G^*_{\Prog,S,T}}$ be the set of general transitions in the partial
evaluation graph $G^*_{\Prog,S,T}$ where every general transition $g \in
\GT_{G^*_{\Prog,S,T}}$ was added by the unfolding of a unique general
transition $g' \in \GTP$. We call $\bar{g} = g'$, similar to Lemma

            \simu_{\Prog,S,T}((\ell, t, s)) = 
            \begin{cases}
            (\langle \ell, \texttt{true}\rangle,
                \unfold_{\Prog,S}(\langle \ell, \texttt{true}\rangle, t), s) & t
                = (\ell, \_,\_, \_,\_) \in T \\

            \simu_{\Prog,S,T}((\ell, t, s)) =

                (\langle\ell,\texttt{true}\rangle,p,\tau,\eta,\langle\ell',\texttt{true}),
                s) & t = (\ell,p,\tau,\eta,\ell') \not\in T
            \end{cases}\\

                \unfold_{\Prog,S}(\langle \ell, \texttt{true}\rangle, t), s) \\

            \begin{cases}

                \unfold_{\Prog,S}(\langle \ell, \varphi\rangle, t), s) & t
                = (\ell, \_,\_, \_,\_) \in T \\
            \varf'(\langle \ell, \varphi\rangle,
                (\langle\ell,\varphi\rangle,p,\tau,\eta,\langle\ell',
                \texttt{true}), s) & t = (\ell,p,\tau,\eta,\ell') \not\in T
            \end{cases} \\ 

                \unfold_{\Prog,S}(\langle \ell, \varphi\rangle, t), s)\\

            \ESs(\Rt_{\Prog}) &= \sum_{i=1}^\infty i \cdot \PrSs(\Rt_\Prog=i) 
            = \sum_{i=1}^\infty \PrSs(\Rt_\Prog \leq i) 
            = \sum_{\substack{f \in \fpath_\Prog\\ \Rt_\Prog(f) \leq
            i}}^\infty \prSs(\varf) \\

            \ESs(\Rt_{\Prog}) &= \sum_{i=1}^\infty i \cdot \PrSs(\Rt_\Prog=i) =
            \sum_{i=1}^\infty \PrSs(\Rt_\Prog \geq i) \\ &= \sum_{i=1}^\infty
            \sum_{\substack{f \in \fpath_\Prog\\ |\varf| \leq i \\ \Rt_\Prog(f)
            \leq i}} 1-\prSs(\varf) \\

            \sum_{\substack{f \in \fpath_\Prog\\ \Rt_\Prog(f) \leq i}}^\infty
            \prSs(f) &\leq \sum_{\substack{f \in \fpath_{\Prog'}\\ \Rt_\Prog(f)
            \leq i}}^\infty \prSns(f) \label{eq:sumsleq} \\

            \sum_{i=1}^\infty\sum_{\substack{f \in \fpath_\Prog\\ |\varf| \leq
            i\\ \Rt_\Prog(\varf) \leq i}}^\infty 1- \prSs(\varf) &\leq
            \sum_{i=1}^\infty\sum_{\substack{f \in
            \fpath_{\Prog'}\\ |\varf| \leq i\\ \Rt_\Prog(\varf)
            \leq i}}^\infty 1- \prSns(\varf) \label{eq:sumsleq} \\

        $\H$ & set of polyhedra \\

        $\TV$ & set of temporary variables \\

consecutive substitutions $[x_i/y(i)]$ where the replacement expression $y_i$

consecutive substitutions $[x_i/y_i]$ where the replacement expression $y_i$

\models \varphi$. Finally, we define two trivial formulas $\texttt{true} = (0 =

\models \varphi$. Finally, we define two trivial constraints $\texttt{true} = (0 =

    Let $\varphi \in \Phi$ be an \gls{fo}-formula. $\llbracket \varphi
    \rrbracket$ is defined as the set of all satisfying assignments of the
    formula $\varphi$.

    Let $\varphi = \psi_1, \dots, \psi_n$ be an conjunction of constraints
    $\psi_1, \dots,\psi_n \in \C$. $\llbracket \varphi \rrbracket$ is defined as
    the set of all satisfying assignments of the formula $\varphi$.

We define a function $\texttt{lin} 2^\PC \rightarrow 2^\C$ that linearly

We define a function $\texttt{lin} : 2^\PC \rightarrow 2^\C$ that linearly

\begin{definition}[Convex Polyhedra\cite{bagnara2005convexpolyhedron}\label{def:polyhedra}]
    $\mathcal{H} \subseteq \N^n$ is a \emph{convex polyhedron} if and only if it
    can be expressed by an intersection of a finite number of affine
    half-spaces.

\begin{definition}[Convex Polyhedra \cite{bagnara2005convexpolyhedron}\label{def:polyhedra}]
    $H \subseteq \N^n$ is a \emph{convex polyhedron} if and only if it can be
    expressed by an intersection of a finite number of affine half-spaces. Let
    $\mathcal{H}$ be the set of all convex polyhedra.

Polyhedra will be used to compute the projection of \gls{fo}-formulas, possibly
over-approximating the constraints in the process. 

Polyhedra will be used to compute the projection of sets of constraints. 

\begin{definition}[Octagons\cite{mine2006hosc,mine2001wcre}\label{def:octagons}]

\begin{definition}[Octagons \cite{mine2006hosc,mine2001wcre}\label{def:octagons}]

    $\mathcal{B} \subseteq \R^n$ is a Box if it can be expressed by a cartesian

    $B \subseteq \R^n$ is a Box if it can be expressed by a cartesian

polyhedron $\mathcal{H}$ one can find a box $\mathcal{B}$ that contains the
polyhedron $\mathcal{H}$. Boxes are computationally very efficient, although
rather imprecise for most applications.

polyhedron $H \in \mathcal{H}$ one can find a box $B$ that contains the
polyhedron $H$. Boxes are computationally very efficient, although rather
imprecise for most applications.

\begin{align}

\begin{align*}

\end{align}

\end{align*}

    \begin{align}

    \begin{align*}

    \end{align}

    \end{align*}

\begin{align}

\begin{align*}

\end{align}

\end{align*}

    \begin{align}

    \begin{align*}

    \end{align}

    \end{align*}

\begin{align}

\begin{align*}

\end{align}

\end{align*}

\subsection{Non-probabilistic approximation}

\subsection{Non-probabilistic over-approximation}

    $(\lfloor f\rceil,\tilde{\varf}) \in \C \times \Z[A \uplus \{d_1,\dots,d_n\}]$  with

    $(\lfloor\varf\rceil,\tilde{\varf}) \in \C \times \Z[A \uplus \{d_1,\dots,d_n\}]$  with

            f[x_i \backslash s(x_i)][D_i\backslash a_i] = s'(x)

            \varf[x_i \backslash s(x_i)][D_i\backslash a_i] = s'(x)

\section{Probabilistic integer programs}\label{sec:pip}

\section{Probabilistic Integer Programs}\label{sec:pip}

However, classical analysis using only \gls{mprf} fails to find a finite
runtime-complexity bound for this program \cite{giesl2022lncs}. With the help of

However, classical analysis using only \gls{mprf}\cite{benamram2017} runtime
complexity bound for this program \cite{giesl2022lncs}. With the help of

\gls{mprf} succeeds at finding a finite runtime-complexity bound, because now

\gls{mprf} succeeds at finding a finite runtime complexity bound, because now

    runtime-complexity bounds using only \gls{mprf}.\cite{giesl2022lncs}}

    runtime complexity bounds using only \gls{mprf}.\cite{giesl2022lncs}}

\citeauthor{Domenech19} \cite{Domenech19} and it is called \gls{cfr}
via partial evaluation. It was implemented in their analysis tool
iRankfinder \cite{irankfinder2018wst}. It achieves very similar results to
\gls{mprf} when used on entire programs or whole \glspl{scc}. Its real
strength comes from applying it to a sub-\gls{scc} level and refining
specifically the loops where \glspl{mprf} fail to find size bounds. This technique
was presented by \citeauthor{giesl2022lncs} \cite{giesl2022lncs}
and implemented in \gls{koat} \cite{giesl2014ijcar} the complexity analysis tool
developed by \citeauthor{giesl2014ijcar} at RWTH University. 

\citeauthor{Domenech19} \cite{Domenech19} and it is called \gls{cfr} via partial
evaluation. It was implemented in their analysis tool iRankfinder
\cite{irankfinder2018wst}. It achieves very similar results to \gls{mprf} when
used on entire programs or whole \glspl{scc}. Its real strength comes from
applying it to a sub-\gls{scc} level and refining specifically the loops where
\glspl{mprf} fail to find bounds. This technique was presented by
\citeauthor{giesl2022lncs} \cite{giesl2022lncs} and it is implemented in
\gls{koat} \cite{giesl2014ijcar} the complexity analysis tool developed by
\citeauthor{giesl2014ijcar} at RWTH University. 

Underneath, \gls{koat} uses iRankFinder for the \gls{cfr}.
Recently, \gls{koat} was extended to probabilistic integer
programs \cite{meyer2021tacas}. For probabilistic programs, \gls{koat} uses
probabilistic ranking functions, that work similarly to \gls{mprf}, but take
probability into accound. They fail for the same reasons as \gls{mprf} for
certain kinds of loops. Unfortunately, by using iRankFinder which is limited to
non-probabilistic integer programs, the technique of \gls{cfr} via partial
evaluation remained out of reach for probabilistic programs.

Underneath, \gls{koat} uses iRankFinder for the \gls{cfr}. Recently, \gls{koat}
was extended to probabilistic integer programs \cite{meyer2021tacas}. For
probabilistic programs, \gls{koat} uses probabilistic ranking functions, that
work similarly to linear ranking functions, but take probability into account.
They fail for the same reasons as \gls{mprf} for certain kinds of loops.
Unfortunately, by using iRankFinder which is limited to non-probabilistic
integer programs, the technique of \gls{cfr} via partial evaluation remained out
of reach for probabilistic programs.

find lower and upper (respectively) runtime-complexity bounds on transition

find lower and upper (respectively) runtime complexity bounds on transition

\gls{mprf} or a \gls{twn}, and then puts the subprograms together in order to
generate upper runtime-complexity and size bounds for the whole program.
Optionally to improve the analysis, \gls{koat} can resort to partial evaluation
as a control-flow refinement technique on a sub-\gls{scc} level
\cite{giesl2022lncs}. \gls{aprove} is the overall tool, and it has taken part in
competitions. It works on various input formats and transforms them accordingly
so that they can be used with specialised tools such as \gls{koat} and
\gls{loat}.

\gls{mprf}\cite{benamram2017} or a \gls{twn}\cite{lommen2022twn}, and then puts the subprograms
together in order to generate upper runtime complexity and size bounds for the
whole program. Optionally to improve the analysis, \gls{koat} can resort to
partial evaluation as a control-flow refinement technique on a sub-\gls{scc}
level \cite{giesl2022lncs}. \gls{aprove} is the overall tool, and it has taken
part in competitions. It works on various input formats and transforms them
accordingly so that they can be used with specialised tools such as \gls{koat}
and \gls{loat}.

technique by partial evaluation proposed by \cite{gallagher2019eptcs}.

technique by partial evaluation proposed by \citeauthor{gallagher2019eptcs}
\cite{gallagher2019eptcs}.

\newcommand{\TV}[0]{\mathcal{TV}} % Program variables

% \newcommand{\TV}[0]{\mathcal{TV}} % Program variables