text:
\section{Conclusion}\label{sec:conclusion}
We introduced the first termination analysis method that takes advantage of
neural networks. Our approach guesses a ranking function candidate
from sampled execution traces, then checks it using SMT solving.
Compared to approaches based on formal reasoning,
our approach is simple to implement:
together with infrastructure for running programs and checking ranking,
we implemented our prototype using a simple neural architecture
with one hidden layer and a straight-forward training script.
This solved 75\% of the programs in a standard set of benchmarks
for termination analysis.

Our result lends itself to future research in machine learning and formal
verification. Learning proofs from examples applies not only to
imperative programs, but also to functional programming and logic.
Moreover, separating proof learning from formal verification may also apply to
further verification questions and such as non-termination~\cite{GuptaHMRX08},
which requires different techniques.

\section{Illustrative Example}
\label{sec:example}
Termination arguments for programs can be subtle.
For example, consider the following program:
\begin{figure}[h]
  \centering
  \begin{lstlisting}[boxpos=b]
it = list.iterator();
while (it.hasNext()) {
  e = it.next();
}
\end{lstlisting}
\end{figure}\\
Such a loop structure often occurs often when iterating through a list
or array. Despite the fact that it may use such data structures it has a
termination argument that only uses integer sequences.  This can be spotted by
examining the traces we obtain when running the program.

In general, an observation is an $n$-di\-men\-sio\-nal vector of values,
where $n$ is the number of traced variables.
To learn a neural ranking function for this example,
we employ a simple neural network with $n$ input neurons directly connected
to one output neuron with resp. weights $\theta = (w_1, \dots, w_n) \in \ensuremath{\mathbb{R}}^n$
and bias $b$. The output neuron features a ReLU activation function, thus the
entire network represents the function
\begin{equation}
  f_\theta(x) = \relu(w_1 \cdot {\tt list.size} +
  \dots
  + w_n \cdot {\tt e} + b).
\end{equation}
We train this neural network so that its output value
decreases by $\delta > 0$ after every consecutive pair of observations for every trace.
Let $\{(\bm{x}^{(i)}, \bm{y}^{(i)})\}_{i=1}^k$ the set of such pairs,
where $\bm{y}$ appears immediately after $\bm{x}$.
To train our network, we solve the following optimisation problem:
\begin{equation}
  \argmin_{\theta \in \ensuremath{\mathbb{R}}^n}\frac{1}{k}
  \sum_{i = 1}^k \underbrace{\max\{f_{\theta}(\bm{y}^{(i)}) - f_{\theta}(\bm{x}^{(i)}) + \delta, 0 \}}_{\mathcal{L}(\bm{x}, \bm{y})}\label{eq:monolithicopt}
\end{equation}
Function $\mathcal{L}(\bm{x}, \bm{y})$ represents the ranking loss of
the neural network over a given pair.
The higher the value of $\mathcal{L}$ the more the network increases
over the pair, whereas for pairs that decrease by the constant $\delta$ its
value is always 0 (i.e., negative values do not affect the sum).
As a result, we obtain the optimal parameter ${\theta^\star}$, which yields
the function
\begin{equation}
  f_{\theta^\star}(x) = \relu({\tt list.length} - {\tt it.nextIndex}),
\end{equation}
after rounding numerical noise in ${\theta^\star}$.
Since this function is always non-negative (i.e., bounded from below) and,
as the formal verifier confirms, it decreases over all inputs,
then it is a valid neural ranking function for this program and thus
witnesses its termination.

By examining the numerical data in execution traces,
this simple neural network discovered a termination argument.
In this paper, we investigate the capabilities of
this and also more general neural networks at learning ranking functions.
For many practical problems, we argue that neural networks are an effective
model for witnessing termination.

\section{Experiments}\label{sec:case-studies}\label{sec:experim}
We developed a prototype implementation of the methods discussed in the previous
sections which we name \texttt{\ensuremath{\nu}Term}\xspace. In this section we present an evaluation of \texttt{\ensuremath{\nu}Term}\xspace on
a set of benchmarks. Subsequently, we discuss results, limitations, and possible
improvements.

\subsection{Benchmarks and Setup}
We consider a benchmark set comprised of problems from the TermComp Termination
Competition~\cite{DBLP:conf/tacas/GieslRSWY19} and the SV-COMP Software
Verification Competition~\cite{10.1007/978-3-030-45237-7_21}.  Both problems
sets are publicly available\footnote{2-Clause BSD License}. Both sets cover a
wide variety of termination and non-termination problems as well as software
verification in general. We restrict the evaluation to the two problem sets
\texttt{Aprove\_09} from TermComp and \texttt{term-crafted-lit} from
SV-COMP. Furthermore, for this evaluation we only consider deterministic
terminating programs with a maximum of two nested loops without function calls.
This left us with 73 problems from \texttt{term-crafted-lit} (originally 159)
and 38 problems (originally 76) from \texttt{Aprove\_09}. The problem set
\texttt{term-crafted-lit} is comprised of problems from literature on
termination analysis translated to C. We therefore had to translate these
problems into Java by hand. In addition, we also split the main functions'
bodies into an initialisation and loop part. Note that this purely
syntactic change does not alter the difficulty of determining termination of a
program. We also do not consider non-terminating programs as they do
not have ranking functions, so our tool simply times out.

The experiments were conducted on Ubuntu 18.04.5 LTS running on an Intel(R)
Xeon(R) CPU E5-2440 0 @ 2.40GHz CPU. We use PyTorch~\cite{NEURIPS2019_9015} as a
machine learning framework. For learning we use the Adam optimiser provided by
PyTorch and a learning rate of $0.05$. We run the benchmarks 5 times with seeds
that were fixed a priori for reproducibility. Instructions on how to reproduce
the results (including seeds etc.) are part of the supplementary material.
\begin{figure*}
\centering
\begin{minipage}[b]{.4\textwidth}
  \includegraphics[scale=0.45]{timings}
  \caption{Percentage of problems solved over number of iterations required
    (accumulative) and percentage of problems solved within a given time spent
    on learning(in seconds).}\label{fig:timings}
\end{minipage}\qquad
\begin{minipage}[b]{.4\textwidth}
  \begin{tikzpicture}[scale=0.8]
\begin{axis}
[
    ybar,
    axis lines*=left,
    ylabel={\% of problems solved},
    xlabel={\# nodes in neural network},
    symbolic x coords={1,2,3,4,5,6,7,8,9,10},

    ymin=0,
    ymax=100,
    ymajorgrids,
    yticklabel={$\pgfmathprintnumber{\tick}\%$},
    xtick=data,
     nodes near coords,
     nodes near coords align={vertical},
    y label style={at={(axis description cs:0.1,.5)},anchor=south},
    ]
\addplot coordinates {(1,64) (2,75) (3,76) (4,75) (5,75) (6,75) (7,75) (8,74) (9,74) (10,73) };

\end{axis}
\end{tikzpicture} \caption{Showing the number of problems solved with 1 to 10 hidden nodes in
    the SOR architecture with PAS.}\label{fig:nodes-results}
\end{minipage}
\end{figure*}
\subsection{Results and Discussion}
We ran \texttt{\ensuremath{\nu}Term}\xspace on the aforementioned benchmarks using one the Sum-of-Relu model
with a variable size number of hidden neurons. The execution traces were
obtained by creating 1000 samples using PAS. As a comparison we also ran
\texttt{Aprove}\cite{GieslABEFFHOPSS17},\texttt{iRankFinder}\cite{DBLP:journals/jacm/Ben-AmramG14},
and \texttt{Ultimate}\cite{HeizmannHP14} on the same benchmarks. Note that since
\texttt{iRankFinder} and \texttt{Ultimate} do not support Java programs as input
those benchmarks were run on the original C versions. The results of these tools
as well as \texttt{\ensuremath{\nu}Term}\xspace with 1 and 5 neurons are presented in
\prettyref{tab:results}. A comparison of \texttt{\ensuremath{\nu}Term}\xspace with different neuron numbers
is presented in \prettyref{fig:nodes-results}.  We present the average number of
solved problems over the multiple runs of \texttt{\ensuremath{\nu}Term}\xspace. Overall, the strongest tool
is \texttt{Aprove} as it solves every problem in \texttt{term-crafted-lit} and
\texttt{Aprove\_09}. In the combined data set \texttt{iRankFinder} and
\texttt{Ultimate} come second and third.  When only considering
\texttt{Aprove\_09} \texttt{\ensuremath{\nu}Term}\xspace{} comes second outperforming \texttt{Ultimate} and
\texttt{iRankFinder}. On the \texttt{term-crafted-lit} set \texttt{Aprove}
solves every single problem while \texttt{Ultimate} and \texttt{iRankFinder}
come second again and \texttt{\ensuremath{\nu}Term}\xspace{} is last.

Comparing different instances of \texttt{\ensuremath{\nu}Term}\xspace{} as presented in
\prettyref{fig:nodes-results} we see that having more than one hidden neuron
improves performance by up to 12\%. However, increasing the complexity further
does not lead to any gains.

\begin{table*}[h]
  \centering
  \begin{tabularx}{\textwidth}{p{0.10\textwidth} p{0.15\textwidth} | X X | X X |
      X X}
    \cmidrule[\heavyrulewidth]{3-8}

    & & \multicolumn{2}{X|}{\texttt{term-crafted-lit}} &  \multicolumn{2}{X|}{\texttt{Aprove\_09}} & \multicolumn{2}{X}{combined}\\
    \# & & 73 & & 38& & 111 & \\
    \midrule
    \multirow{2}{*}{\texttt{\ensuremath{\nu}Term}\xspace}& 1 neuron & 41  & 56.2\% & 29.8 & 78.4\% & 70.8 & 63.8\% \\
    & 5 neurons & 48.0 & 65.8\% & 35.4 & 93.2\% & 83.4 & 75.1\%\\
    \midrule \multicolumn{2}{p{0.25\textwidth}|}{\texttt{Aprove}} & 73 & 100\% &
    38 &
    100\% & 111  &100\% \\
    \midrule \multicolumn{2}{p{0.25\textwidth}|}{\texttt{Ultimate}} & 66 &
    90.4\% & 31 & 81.6\%
    & 97 & 87.3\% \\
    \midrule \multicolumn{2}{p{0.25\textwidth}|}{\texttt{iRankFinder}} & 65 &
    89.0\% &
    33 & 86.8\% & 98 & 88.2\% \\
    \bottomrule
  \end{tabularx}
  \caption{Results of running \texttt{\ensuremath{\nu}Term}\xspace (with 1 neuron, 5 neurons with PAS, and 5
    neurons with Gaussian sampling), \texttt{Aprove}, \texttt{Ultimate}, and
    \texttt{iRankFinder} on \texttt{term-crafted-lit} and
    \texttt{Aprove\_09}. In the case of \texttt{\ensuremath{\nu}Term}\xspace we report the average results.}
  \label{tab:results}
\end{table*}

\begin{figure*}
  \centering
  \begin{tabular}{cc}
    \includegraphics[scale=0.45]{iterationspairwisegauss}
    &
      \includegraphics[scale=0.45]{samplingstrats}\\
    \footnotesize  (a) & \footnotesize (b)
  \end{tabular}
  \caption{Comparing the number of iterations and time required to solve
    problems using Gaussian sampling and PAS in the SOR model with 5 hidden
    neurons.}
  \label{fig:sampling-strat}
\end{figure*}
\paragraph{Discussion}
Overall, \texttt{\ensuremath{\nu}Term}\xspace proves termination for 75.1\% of all problems in the average
case and 76.6\% in the best run with 5 neurons. In comparison, when using only 1
neuron we solve 63.8\% and 65.8\% of all problems in the average and best case,
respectively. \prettyref{fig:timings} presents a plot describing the learning
process and how fast the models converge in terms of time. Although the more
complex model should theoretically be slower when performing a learning step,
this is offset by the fact that the more complex model requires fewer iterations
to minimise the loss. \prettyref{fig:nodes-results} shows how increasing the
number of hidden nodes is only initially improves the efficacy of the network
drastically (by 11\%). This indicates that simply increasing the number of hidden nodes
would not lead to further improvements.

Similarly, the sampling strategy also has an impact on the performance of the
network as shown in \prettyref{fig:sampling-strat}. In total the 5 neuron model
using the Gaussian sampling strategy only solves 64\% of the problems and is
therefore closer to the one neuron model when it comes to
performance. \prettyref{fig:sampling-strat} (b) shows that Gaussian sampling is
slower overall. This is unsurprising as Gaussian sampling leads to more large
numbers and therefore longer traces.

In comparison with other tools \texttt{\ensuremath{\nu}Term}\xspace comes in last when considering the
combined data set as well as \texttt{term-crafted-lit}. In the combined data set
our prototype is trailing by around 13\% in the average case and around 11\% in
the best case. In contrast when considering the \texttt{Aprove\_09} dataset
\texttt{\ensuremath{\nu}Term}\xspace comes in second place (behind \texttt{Aprove}) and beats
\texttt{Ultimate} and \texttt{iRankFinder} by approximately 12\% and 8\% respectively.
\texttt{Aprove}, \texttt{Ultimate}, and \texttt{iRankFinder} are mature
tools that have seen a lot of development and contributions from multiple
researchers over many years. Furthermore, they implement multiple theoretical
methods and results gathered over the years. On the other hand, \texttt{\ensuremath{\nu}Term}\xspace only
implements neural termination analysis as discussed in this paper. Despite this we can keep up with state of the art tools and
even manage to improve on them in the \texttt{Aprove\_09} set.
\subsection{Limitations}
Owing to the inherent difficulty of the problem at hand (termination), methods
for solving it are necessarily incomplete.  Neural termination analysis is no
exception. It is easy to construct programs that other methods can prove
terminating but where neural termination analysis fails. Usually, these fall
into one of the following three cases.
\begin{figure}
  \centering
  \begin{tabular}{cc}
    \begin{lstlisting}[boxpos=Java]
while(x > 0) {
  x = -2*x + 10;
}
    \end{lstlisting}
    &
      \begin{lstlisting}[boxpos=Java]
int j = i;
while(i < 100) {
  i++;
  j = i;
}
      \end{lstlisting}\\
    \footnotesize (a) & \footnotesize (b)
  \end{tabular}
  \caption{Two loops that are challenging for neural termination analysis due to
    either lack of data or deceiving data.}
  \label{fig:limit-examples}
\end{figure}
\paragraph{Insufficient Data}
Neural termination analysis learns termination arguments from execution traces.
Hence, any program feature that limits the data that can be gathered is a
problem for our approach. Multiple problems in the dataset exhibit
behaviour such as \prettyref{fig:limit-examples} (a).
This loop only has more than one iteration if $x$ is sampled with one of
$1,2,3,4$ and even then the trace is only extremely short. Similar issues can occur
when learning offsets (biases) or when branching only occurs in rare
cases. These issue may be mitigated by
letting the verifier propose specific initial conditions for the sampling.
\paragraph{Model Expressivity}
As ranking functions become more complex, the models also need to be able to
express them. On instance of such a problem from the dataset
is a problem where the ranking function depends on the evenness of an input
variable. Neither of our models is expressive enough to capture the concept of
evenness. A solution to this problem is considering more
expressive models. However, with more complex models the effort required to
verify and the amount of data required to train these models increases.
\paragraph{Verification}
When there are multiple correct ranking functions the
verification procedure may not be able to prove all of them correct. The loop
presented in \prettyref{fig:limit-examples} (b) can exhibit such behaviour. When
purely looking at the execution traces, which is what the learning procedure
does, $i$ and $j$ have the exact same values at the loop head.  Hence, if the
learner comes up with the ranking function $100 - j$ the verifier would not be
able to prove it correct unless it is supplied with the invariant that $i = j$
at the loop head.  One way to solve this problem could be to integrate existing
methods that discover such
invariants~\cite{SiDRNS18,DBLP:journals/scp/ErnstPGMPTX07}.

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

In this section we give an overview of the implementation of \texttt{\ensuremath{\nu}Term}\xspace.  A
prototype implementation of the ideas presented in the previous sections for
termination analysis of Java bytecode (JBC) programs.  Note that this is
merely an engineering choice, motivated by the existence of libraries and
the widespread usage of the JVM.  Furthermore, as noted above, the
separation of tracing, learning, and verification makes this approach very
modular.  Hence, to support a different input language one only has to
adjust tracing and verifification while the implementation of the primary
contribution of this paper (the learning) remains unchanged.

\paragraph{Tracing and Sampling}

Tracing is the first step of our method (\prettyref{fig:arch}).  This
requires two parts.  First, any program requires an input that needs to be
generated.  Second, the program in question has to be executed with this
input.  During the execution of the program we take snapshots of the memory.
The sequence of all snapshots is what we refer to as the \emph{trace} of a
program.  By repeating this process with different inputs we collect a large
number of samples.  Ideally, this sampled data exhibits every possible
behaviour of the program.

We limit ourselves to deterministic programs, that is, programs that always
exhibit the same behaviour given the same input.  We generate the inputs
using a pseudorandom generator with one of the following three distribution
strategies:
\begin{itemize}[topsep=0ex]
    \setlength\itemsep{-0.3em}
\item uniform,
\item Gaussian, and
\item pairwise anticorrelated sampling (PAS).
\end{itemize}
The first two simply denote the strategy where for each program input
parameter we sample random values with either a uniform or a Gaussian
distribution, respectively.  The PAS strategy uses a multivariate normal
distribution where we create a dependence between two randomly chosen
values.  Hence, this is a standard Gaussian distribution for all
variables except for two where we create an indirect correlation.  If enough
samples are traced we can expect a sample for each possible pair in the
input data.  This has the advantage that it keeps the traces short while
simultaneously creating diversity in the traces.

Once the input data is generated we can execute the programs with these
arguments.  Note that the runs of the program are independent, which allows
us to parallelise the sampling process.  The tracing itself is done by
taking snapshots of all local variables and their contents throughout the
execution of the target program.  All of this functionality is provided by
the Java Virtual Machine Tool Interface (JVM~TI), which allows us to control
and inspect the state of a JVM during the execution of a program.

\paragraph{Learning}

Once we have obtained the traces of the program we can learn ranking
functions.  As we are only interested in ranking the strongly connected
components (i.e., loops) we analyse the CFG to identify the loop headers.  With
these we can extract the parts of the trace that are relevant.  The memory
snapshots at the loop header are joined together and subsequently turned into
ranking pairs in a sliding window fashion.  These pairs constitute our
training data to which we apply a \emph{pairwise learning to rank} algorithm
(cf.~\prettyref{sec:learning}).  All of this is implemented using
PyTorch~\cite{NEURIPS2019_9015}.

\paragraph{Verification}

There are numerous ways to check that a termination certificate (i.e., a
ranking function) is correct.  In our case, we translate the program into
single static assignment (SSA) form, which we then translate into a
satisfiability modulo theories (SMT) formula.  This SMT formula encodes the
requirement that the ranking function is indeed a decreasing measure for
every iteration of every loop.  Furthermore, it ensures that the relation is
well founded.  Finally, we use the SMT solver Z3 to prove
these assertions~\cite{tacas/MouraB08}.

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

Software is a complex artefact.  Programming is prone to error and some bugs are
hard to find even after extensive testing. Bugs may cause crashes, undesirable
outputs, and can prevent a program from responding at all.  Termination analysis
addresses the question of whether, for every possible input, a program
halts. This is undecidable in general, yet tools that work in practice have been
developed by industry and
academia~\cite{CookPR06,HeizmannCDEHLNSP13,BrockschmidtCIK16,GieslABEFFHOPSS17,LeAFKN20}.
The use of machine learning for termination analysis is rare. In this paper, we
introduce a novel technique that effectively trains neural networks to act as
formal proofs of termination.

To argue that a program terminates one usually presents a
\emph{ranking function}. Ranking functions map program states to values
that (i)~decrease by a discrete amount after every loop iteration and
(ii)~are bounded from below~\cite{Floyd67}.  They are certificates of
termination: if a ranking function exists, then the program terminates for
every possible input. Previous methods find termination proofs by
relying on sound symbolic reasoning
procedures~\cite{ArtsG00,PodelskiR04,BradleyMS05,Cousot05,pldi/CookPR06,ChenXYZZ07,DBLP:journals/fmsd/CookKRW13,icalp/BradleyMS05,10.1007/978-3-642-54862-8_12,Urban13,10.1007/978-3-642-36742-7_4,GieslABEFFHOPSS17,BrockschmidtOEG10,rta/OttoBEG10,DBLP:conf/sas/Spoto16,DBLP:conf/fmco/AlbertAGPZ07,HeizmannHP14,DBLP:conf/pldi/ChenHLLTTZ18}.
However, \emph{finding a
proof is much harder than checking that a given candidate proof is valid}.
We propose a framework that leverages this observation.
First, we learn a ranking function candidate by training a neural network
that decreases along sampled runs of the program;
only then, we use symbolic reasoning to check whether this candidate
{\em ranking neural network} decreases along every run of the program.
If the network is also bounded from below, then this witnesses termination.

\begin{figure*}
  \centering
  \begin{tikzpicture}[scale=0.9]

    \def1.5pt{1.5pt}
    \def.25{.25}
    \def.6{.6}
    \def0.15{0.15}

    \defblack{black!20}
    \def5.5*\nnyd{6*.25}
    \node[draw, circle, thick, inner sep=1.5pt,black] (i1) at (0.15,5.5*\nnyd+.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i2) at (0.15,5.5*\nnyd) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i3) at (0.15,5.5*\nnyd-.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h1) at (0.15+.6,5.5*\nnyd+1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h2) at (0.15+.6,5.5*\nnyd+.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h3) at (0.15+.6,5.5*\nnyd-.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h4) at (0.15+.6,5.5*\nnyd-1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (o1) at (0.15+2*.6,5.5*\nnyd) {};
    \draw[black] (i1) -- (h1) -- (i2) -- (h2) -- (i3) -- (h3) -- (o1) -- (h1)
    -- (i3) -- (h4) -- (o1) -- (h2) -- (i1) -- (h3) -- (i2) -- (h4) -- (i1);

    \defblack{black!35}
    \def5.5*\nnyd{4*.25}
    \node[draw, circle, thick, inner sep=1.5pt,black] (i1) at (0.15,5.5*\nnyd+.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i2) at (0.15,5.5*\nnyd) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i3) at (0.15,5.5*\nnyd-.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h1) at (0.15+.6,5.5*\nnyd+1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h2) at (0.15+.6,5.5*\nnyd+.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h3) at (0.15+.6,5.5*\nnyd-.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h4) at (0.15+.6,5.5*\nnyd-1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (o1) at (0.15+2*.6,5.5*\nnyd) {};
    \draw[black] (i1) -- (h1) -- (i2) -- (h2) -- (i3) -- (h3) -- (o1) -- (h1)
    -- (i3) -- (h4) -- (o1) -- (h2) -- (i1) -- (h3) -- (i2) -- (h4) -- (i1);

    \defblack{black!50}
    \def5.5*\nnyd{2*.25}
    \node[draw, circle, thick, inner sep=1.5pt,black] (i1) at (0.15,5.5*\nnyd+.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i2) at (0.15,5.5*\nnyd) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i3) at (0.15,5.5*\nnyd-.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h1) at (0.15+.6,5.5*\nnyd+1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h2) at (0.15+.6,5.5*\nnyd+.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h3) at (0.15+.6,5.5*\nnyd-.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h4) at (0.15+.6,5.5*\nnyd-1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (o1) at (0.15+2*.6,5.5*\nnyd) {};
    \draw[black] (i1) -- (h1) -- (i2) -- (h2) -- (i3) -- (h3) -- (o1) -- (h1)
    -- (i3) -- (h4) -- (o1) -- (h2) -- (i1) -- (h3) -- (i2) -- (h4) -- (i1);

    \defblack{black}
    \def5.5*\nnyd{0}
    \node[draw, circle, thick, inner sep=1.5pt,black] (i1) at (0.15,5.5*\nnyd+.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i2) at (0.15,5.5*\nnyd) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i3) at (0.15,5.5*\nnyd-.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h1) at (0.15+.6,5.5*\nnyd+1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h2) at (0.15+.6,5.5*\nnyd+.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h3) at (0.15+.6,5.5*\nnyd-.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h4) at (0.15+.6,5.5*\nnyd-1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (o1) at (0.15+2*.6,5.5*\nnyd) {};
    \draw[black] (i1) -- (h1) -- (i2) -- (h2) -- (i3) -- (h3) -- (o1) -- (h1)
    -- (i3) -- (h4) -- (o1) -- (h2) -- (i1) -- (h3) -- (i2) -- (h4) -- (i1);

    \def1.1pt{1.1pt}
    \def.07{.07}
    \def1.1{1.1}
    \def1.05cm{1.05cm}
    \node[draw, rectangle, inner sep=1.1pt, minimum width=1.05cm*1.1] (ta)
    at (0.15-1.1, 0) {\scriptsize 98, 44, 20};

    \def2pt{2pt}
    \draw[rounded corners=1pt,thick] ($(ta.north west)+(-2pt,2pt)$) --
    ($(ta.north east)+(2pt,2pt)$) --
    ($(ta.south east)+(2pt,-2pt)$) --
    ($(ta.south west)+(-2pt,-2pt)$) -- cycle;

    \draw[thick] ($(ta.east) + (2pt,0)$) edge[->] ($(0.15,0)-(.2,0)$);

    \draw ($(ta.north west)-(5pt,0)$) edge[thick,->] ($(ta.south west)-(5pt,0)$);

    \node[draw, rectangle, inner sep=1.1pt, minimum width=1.05cm,
    above=.25 of ta] (ta1) {\tiny 99, 44, -3};
    \node[draw, rectangle, inner sep=1.1pt, minimum width=1.05cm,
      above=.25 of ta1] (ta2) {\tiny 99, 43, 34};
    \node[draw, rectangle, inner sep=1.1pt, minimum width=1.05cm,
      above=.25 of ta2] (ta3) {\tiny 99, 42, 56};
    \node[above=.02 of ta3, inner sep=0] (t0) {\vdots};

    \node[below=-.1 of ta, inner sep=0] (tlast) {\vdots};

    \node at (0.15+2.5*.6,5.5*\nnyd+6*.25) {\scriptsize 57};
    \node at (0.15+2.5*.6,5.5*\nnyd+4*.25) {\scriptsize 56};
    \node at (0.15+2.5*.6,5.5*\nnyd+2*.25) {\scriptsize 55};
    \node at (0.15+2.5*.6,5.5*\nnyd) {\scriptsize 54};
    \node[rotate=90] at (0.15+2.5*.6,5.5*\nnyd+.25) {\scriptsize $<$};
    \node[rotate=90] at (0.15+2.5*.6,5.5*\nnyd+3*.25) {\scriptsize $<$};
    \node[rotate=90] at (0.15+2.5*.6,5.5*\nnyd+5*.25) {\scriptsize $<$};
    \draw let \p1=(tlast) in node at (0.15+2.5*.6,\y1+1) {$\vdots$};
    \draw let \p1=(t0) in node at (0.15+2.5*.6,\y1) {$\vdots$};

    \draw[thick,rounded corners] let \p1=($(t0.north)$), \p2=($(tlast.south)$) in
    (-1.9, \y2-.1cm) -- (1.9, \y2-.1cm) -- (1.9, \y1-.1cm) --
    (-1.9, \y1-.1cm) -- cycle;

    \def6{6}
    \draw[thick,rounded corners] let \p1=($(t0.north)$), \p2=($(tlast.south)$) in
    (6-1.9, \y2-.1cm) -- (6+1.9, \y2-.1cm) -- (6+1.9, \y1-.1cm) --
    (6-1.9, \y1-.1cm) -- cycle;

    \defblack{black}
    \def5.5*\nnyd{0.5*.25}
    \node[draw, circle, thick, inner sep=1.5pt,black] (i1) at (0.15+6,5.5*\nnyd+.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i2) at (0.15+6,5.5*\nnyd) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i3) at (0.15+6,5.5*\nnyd-.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h1) at (0.15+6+.6,5.5*\nnyd+1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h2) at (0.15+6+.6,5.5*\nnyd+.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h3) at (0.15+6+.6,5.5*\nnyd-.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h4) at (0.15+6+.6,5.5*\nnyd-1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (o1) at (0.15+6+2*.6,5.5*\nnyd) {};
    \draw[black] (i1) -- (h1) -- (i2) -- (h2) -- (i3) -- (h3) -- (o1) -- (h1)
    -- (i3) -- (h4) -- (o1) -- (h2) -- (i1) -- (h3) -- (i2) -- (h4) -- (i1);

    \node[inner sep=1.1pt, minimum width=1.05cm*1.1] (ta)
    at (0.15-1.1+6, 5.5*\nnyd) {\scriptsize $x'$, $y'$, $z'$};
    \draw[rounded corners=1pt,thick] ($(ta.north west)+(-2pt,2pt)$) --
    ($(ta.north east)+(2pt,2pt)$) --
    ($(ta.south east)+(2pt,-2pt)$) --
    ($(ta.south west)+(-2pt,-2pt)$) -- cycle;
    \draw[thick] ($(ta.east) + (2pt,0)$) edge[->] ($(0.15+6,5.5*\nnyd)-(.2,0)$);

    \node at (0.15+2.5*.6+6,5.5*\nnyd) {\scriptsize $R'$};
    \node[rotate=90] at (0.15+2.5*.6+6,5.5*\nnyd+2.5*.25) {\scriptsize $<$};

    \defblack{black}
    \def5.5*\nnyd{5.5*.25}
    \node[draw, circle, thick, inner sep=1.5pt,black] (i1) at (0.15+6,5.5*\nnyd+.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i2) at (0.15+6,5.5*\nnyd) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (i3) at (0.15+6,5.5*\nnyd-.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h1) at (0.15+6+.6,5.5*\nnyd+1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h2) at (0.15+6+.6,5.5*\nnyd+.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h3) at (0.15+6+.6,5.5*\nnyd-.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (h4) at (0.15+6+.6,5.5*\nnyd-1.5*.25) {};
    \node[draw, circle, thick, inner sep=1.5pt,black] (o1) at (0.15+6+2*.6,5.5*\nnyd) {};
    \draw[black] (i1) -- (h1) -- (i2) -- (h2) -- (i3) -- (h3) -- (o1) -- (h1)
    -- (i3) -- (h4) -- (o1) -- (h2) -- (i1) -- (h3) -- (i2) -- (h4) -- (i1);

    \node[inner sep=1.1pt+1, minimum width=1.05cm*1.1] (ta)
    at (0.15-1.1+6, 5.5*\nnyd) {\scriptsize $x$,\;\;\,$y$,\;\;\,$z$};
    \draw[rounded corners=1pt,thick] ($(ta.north west)+(-2pt,2pt)$) --
    ($(ta.north east)+(2pt,2pt)$) --
    ($(ta.south east)+(2pt,-2pt)$) --
    ($(ta.south west)+(-2pt,-2pt)$) -- cycle;
    \draw[thick] ($(ta.east) + (2pt,0)$) edge[->] ($(0.15+6,5.5*\nnyd)-(.2,0)$);

    \node at (0.15+2.5*.6+6,5.5*\nnyd) {\scriptsize $R$};

    \node (scroll) at (6, 3.5){\includegraphics[width=1cm]{ancient-scroll.png}};
    \node [above=-.1cm of scroll] {\scriptsize Machine Code};

    \node (run) at (0, 3.5){\includegraphics[width=1cm]{settings-gears.png}};
    \node [above=-.1cm of run] (tracing) {\scriptsize Execution Traces};

    \draw[thick] let \p1=($(t0.north)$) in (run.south) edge[->] (0,\y1);
    \draw[thick] let \p1=($(t0.north)$) in (scroll.south) edge[->] (6,\y1);
    \draw[thick] (scroll.west) edge[->] (run.east);
    \draw[thick] (1.9,3*.25) edge[->]
    node[above] {\scriptsize \begin{tabular}{c}
        Candidate Neural\\Ranking Function\end{tabular}}
    (6-1.9,3*.25);

    \node (yes) at (6+2.9, 5*.25) {\scriptsize Terminates};
    \node (no) at (6+2.9, 1*.25) {\scriptsize Unknown};
    \draw[thick] (6+1.9, 3*.25) edge[->] (yes);
    \draw[thick] (6+1.9, 3*.25) edge[->] (no);

    \node[inner sep=0] (input) at (-2.9, 3*.25) {\scriptsize \begin{tabular}{c}
        Hyper-\\parameters\end{tabular}};
    \draw[thick] (input) edge[->] (-1.9, 3*.25);

    \def1.1{1.1}
    \draw node[anchor=north, inner sep=0] at (0,-1.1)
          {\begin{tabular}{c}1. Train\end{tabular}};
    \draw node[anchor=north, inner sep=0] at (6, -1.1)
          {\begin{tabular}{c}2. Verify\end{tabular}};
  \end{tikzpicture}
  \caption{Schema of our procedure.}
  \label{fig:arch}
\end{figure*}

We propose a framework (see Fig.~\ref{fig:arch})
for termination analysis where a neural ranking function
is first trained over executions of a program and
then verified over the program code
(namely, for different programs we train different ranking functions).
We produce a set of traces by executing the program multiple times with
random inputs and collecting consecutive observations of its variables as it runs.
All traces are then given to a training procedure together
with hyperparameters and a chosen neural architecture; we require
a priori that the neural network's output is bounded from below (see Sect.~\ref{sec:learning}).
The training procedure minimises a loss function whose value is
the higher the less the neural network decreases over all sampled observations.
This produces a neural network that behaves as a ranking function over the samples executions.
To determine whether it generalises to all possible executions,
we pass it to a formal verification procedure.
The formal verification procedure encodes the program and the
neural network symbolically; then, it uses satisfiability modulo theories (SMT)
to formally decide whether the neural network is a valid ranking function.
Upon an affirmative result, our procedure concludes that the program terminates;
upon a negative result, it returns an inconclusive answer, that is,
the program may or may not terminate. Overall, the verification procedure
guarantees that our method is sound when it determines that the
program terminates.

We demonstrate that our technique is effective over a broad variety of programs.
We present a loss functions for training monolithic and lexicographic ranking functions.
Using a neural network with one hidden layer and a straight-forward training routine,
our method discovers neural ranking functions for over 75\% of the benchmarks
in a standard problem set for termination analysis~\cite{DBLP:conf/tacas/GieslRSWY19,10.1007/978-3-030-45237-7_21}.
Our method discovers linear ranking functions, as well as
ranking functions for problems that require piecewise linear or lexicographic
termination arguments~\cite{HeizmannHP14,UrbanGK16}.
Neural networks unify multiple termination
analysis strategies.
Our training procedure is agnostic with respect to the
programming language and requires no information about the program
other than execution traces. It thus applies without modifications to
toy examples as well as to software that uses data structures as long as
a procedure for verifying ranking functions is available.
The complexity of reasoning about the program is entirely delegated to the verification procedure
which must only solve the task of checking the validity of the ranking function.

Neural termination analysis defines a framework whose main knobs are
\begin{enumerate}
\item sampling strategy,
\item neural architecture, and
\item verification procedure.
\end{enumerate}
A sampling strategy determines tracing coverage.
Traditional testing aims at finding bugs quickly and thus covers in breath;
sampling for termination analysis must cover in depth so as to avoid a bias over short traces.
For this purpose, we sample variables far-apart in pairs, exploiting the
empirical observation that execution length is often given by the difference of two variables.
A neural architecture determines which ranking functions are learnable.
We consider an architecture with one hidden layer and ReLU activation functions
which allows expressing linear and piecewise linear functions (e.g., the absolute value).
Finally, a verification procedure determines the programming language features
we support. We built a verifier for Java bytecode that manipulate native types.
This combination of sampling strategy, neural architecture, and verification
procedure is one exemplar configuration for our approach,
which offers a flexible and extensible termination analysis framework that
combines testing methods, deep learning, and symbolic reasoning.

\subsection{Related Work}
As termination is an important problem in computer science many methods for
automatically proving termination have been developed and implemented. Due to
the underlying undecidability most techniqus restrict the programs to linear
programs~\cite{PodelskiR04}, semi-definite programs~\cite{Cousot05},
semi-algebraic systems~\cite{ChenXYZZ07}, or formulae over SMT
theories~\cite{DBLP:journals/fmsd/CookKRW13}. To deal with the increasing
complexity of programs lexicographic ranking
functions~\cite{BradleyMS05,icalp/BradleyMS05,10.1007/978-3-642-54862-8_12} and
disjoint well-founded relations were
introduced~\cite{pldi/CookPR06,10.1007/978-3-642-36742-7_4}.  Other methods
perform termination analysis by translating programs to alternate models of
computation and show that the resulting translation is terminating.  This
requires a guarantee that termination of the translation implies the termination
of the original program. Such models can be term rewrite
systems~\cite{GieslABEFFHOPSS17,BrockschmidtOEG10,rta/OttoBEG10}, constraint
logic programs~\cite{DBLP:conf/sas/Spoto16}, recurrence
relations~\cite{DBLP:conf/fmco/AlbertAGPZ07}, and Büchi
automata~\cite{HeizmannHP14,DBLP:conf/pldi/ChenHLLTTZ18}.

The aforementioned approaches do not incorporate modern artificial intelligence
technologies for the discovery of termination arguments.  However, more recently
such approaches where presented.  In~\cite{sigsoft/Nori013} the authors use
execution traces to construct linear regression problem whose solution describes
a correct loop bound.  More recently, execution traces were used to pose the
finding of ranking functions as a satisfiability modulo theories (SMT)
problem~\cite{LeAFKN20}. In~\cite{DBLP:journals/access/YuanL19} Support Vector
Machines (SVM) are used to predict coefficients to ranking function templates.
Most recently, \cite{DBLP:journals/nca/TanL21} use deep neural networks in a
similar fashion to find coefficients for ranking function templates. It is worth
noting that both approaches are only presented for very simple loop languages
where the loop guards are only conjunctions and the bodies are only deterministic
updates.

Machine learning has also been applied to safety analysis~\cite{SiDRNS18},
stability analysis of dynamical systems~\cite{ChangRG19,AbateAGP21}, logic
queries~\cite{DBLP:conf/icml/FischerBDGZV19} and program
synthesis~\cite{DBLP:conf/iclr/ParisottoMS0ZK17}

\section{Training Neural Ranking Functions}\label{sec:learning-ranking-functions}\label{sec:learning}

Our method collects execution traces from a program and then proceeds
in two phases: first it trains and then it formally verifies.
We train a neural networks so that its output
descends by a discrete amount $\delta > 0$ over transition observation samples.
For programs that may have nested loops,
we train a neural network with multiple outputs which decrease
lexicographically by $\delta$.

\paragraph{Transition Observations and Traces}

Our dataset is a collection of observations from the transition relation $T$.
The state of a program is large and complex and contains internal information
that a neural network cannot handle directly. The standard approach to address
this issue is to define an \emph{embedding}.  To this end, we define an
observation function $\omega \colon S \to \ensuremath{\mathbb{R}}^n$, which extracts appropriate
input to the neural network from a program state.  States are recorded at key
locations during a run, specifically, at loop headers; then $\omega$ is possibly
partial. The observation function converts a run (see Eq.~\ref{eq:run}) into a
{\em trace} $x_0, x_1, x_2, \dots$
where, for all $i>0$, the relation between $x_{i-1} \in \ensuremath{\mathbb{R}}^n$ and
$x_{i} \in \ensuremath{\mathbb{R}}^n$ is that the former has been observed before the latter at
the same control location.  In other words, for all $i>0$, we have that
$x_{i-1} = \omega(s_{i-1})$ and $x_{i} = \omega(s_{i})$ for some
$(s_{i-1},s_i) \in T^+$ such that $\lambda(s_{i-1}) = \lambda(s_i)$.

\begin{figure}
  \centering
  \begin{tikzpicture}[scale=0.9,inner sep=2pt, minimum size=0.4cm,node
    distance=.5cm]

    \node (x1) [draw, circle] at (0,.6) {}; \node (x2) [draw, circle, below
    of=x1] {}; \node (x3) [inner sep=0pt,minimum size=0,below of=x2] {\vdots};
    \node (x4) [draw, circle, below of=x3,yshift=-2mm] {};

    \def.2cm{.4cm} \node (l1) [left=.2cm of x1, anchor=east]
    {$x_1$}; \node (l2) [left=.2cm of x2, anchor=east] {$x_2$}; \node (l4)
    [left=.2cm of x4, anchor=east] {$x_n$};

    \draw (l1) edge[->] (x1); \draw (l2) edge[->] (x2); \draw (l4) edge[->]
    (x4);

    \node (y1) [draw, circle] at (2.5,2) {};

    \node (y2) [draw, circle, below of=y1] {};

    \node (y3) [inner sep=0pt,minimum size=0,below of=y2,yshift=.1cm] {\vdots};
    \node (y4) [draw, circle, below of=y3,yshift=-.1cm] {};

    \def\bmar{3pt} \draw[rounded corners] let
    \p1=(y1.north),\p2=(y1.east),\p3=(y4.south),\p4=(y4.west) in
    (\x2+\bmar,\y1+\bmar) -- (\x2+\bmar,\y3-\bmar) -- (\x4-\bmar,\y3-\bmar) --
    (\x4-\bmar,\y1+\bmar) -- cycle;

    \node (y5) [inner sep=0pt,minimum size=0,below of=y4] {\vdots};

    \node (y6) [draw, circle, below of=y5,yshift=-.2cm] {}; \node (y7) [draw,
    circle, below of=y6] {}; \node (y8) [inner sep=0pt,minimum size=0,below
    of=y7,yshift=.1cm] {\vdots}; \node (y9) [draw, circle, below
    of=y8,yshift=-.1cm] {};

    \draw[rounded corners] let
    \p1=(y6.north),\p2=(y6.east),\p3=(y9.south),\p4=(y9.west) in
    (\x2+\bmar,\y1+\bmar) -- (\x2+\bmar,\y3-\bmar) -- (\x4-\bmar,\y3-\bmar) --
    (\x4-\bmar,\y1+\bmar) -- cycle;

    \draw let \p1=(y1.north),\p3=(y4.south) in node (z1) [draw, circle, inner
    sep=2pt, minimum size=0.4cm] at (5,.5*\y1+.5*\y3) {};

    \draw let \p1=(y6.north),\p3=(y9.south) in node (z2) [draw, circle, inner
    sep=2pt, minimum size=0.4cm] at (5,.5*\y1+.5*\y3) {};

    \node at ($(z1)!.5!(z2)$) {\vdots};

    \draw (y1) -- node[above,pos=.25] {\scriptsize 1} (z1); \draw (y2) --
    node[above,pos=.25] {\scriptsize 1} (z1); \draw (y4) -- node[above,pos=.25]
    {\scriptsize 1} (z1);

    \draw (y6) -- node[above,pos=.25] {\scriptsize 1} (z2); \draw (y7) --
    node[above,pos=.25] {\scriptsize 1} (z2); \draw (y9) -- node[above,pos=.25]
    {\scriptsize 1} (z2);

    \node (o1) [right=.2cm of z1, anchor=west] {$f_\theta(x)_1$}; \draw
    (z1) edge[->] (o1);

    \node (o2) [right=.2cm of z2, anchor=west] {$f_\theta(x)_m$}; \draw
    (z2) edge[->] (o2);

    \path[draw] (y1) -- (x1) -- (y2) -- (x1) -- (y4); \path[draw] (y1) -- (x2)
    -- (y2) -- (x2) -- (y4); \path[draw] (y1) -- (x4) -- (y2) -- (x4) -- (y4);

    \path[draw] (y6) -- (x1) -- (y7) -- (x1) -- (y9); \path[draw] (y6) -- (x2)
    -- (y7) -- (x2) -- (y9); \path[draw] (y6) -- (x4) -- (y7) -- (x4) -- (y9);

    \def3mm{3mm}
    \draw[decorate,thick,decoration={brace,amplitude=6pt,mirror,raise=0pt}] let
    \p1=(x1.east),\p2=(y1.west),\p3=(y9.south) in (\x1,\y3-3mm) --
    (\x2-2*\bmar,\y3-3mm) node[midway,yshift=-6mm]{\scriptsize
      \begin{tabular}{c}Trainable\\weights $\theta$\end{tabular}};

    \draw[decorate,thick,decoration={brace,amplitude=6pt,mirror,raise=0pt}] let
    \p1=(y1.west),\p2=(y1.east),\p3=(y9.south) in (\x1-\bmar,\y3-3mm) --
    (\x2+\bmar,\y3-3mm) node[midway,yshift=-5mm]{\scriptsize ReLU};

    \draw[decorate,thick,decoration={brace,amplitude=6pt,mirror,raise=0pt}] let
    \p1=(y1.east),\p2=(z1),\p3=(y9.south) in (\x1+2*\bmar,\y3-3mm) --
    (\x2,\y3-3mm) node[midway,yshift=-5mm]{\scriptsize Sums of ReLUs};
  \end{tikzpicture}
  \caption{``Sum of ReLUs'' architecture for lexicographic neural ranking
    functions.}
  \label{fig:sor}
\end{figure}

\paragraph{Sum of ReLUs Architecture}
We train a ranking function model $f_\theta \colon \ensuremath{\mathbb{R}}^n \to \ensuremath{\mathbb{R}}^m$
(parameterised by $\theta$) with $n$ inputs and $m$ outputs where $m$ so that it
acts as a ranking function along every trace. Note that $m$ is the number of
nested loop heads in the given program.  First, we require that $f_\theta$ is
bounded from below a priori.  We enforce this condition over the neural network
by choosing an appropriate architecture as depicted in Fig.~\ref{fig:sor}.  The
\emph{sum of ReLUs} (SOR) architecture features $n$ inputs, $m$ outputs, and one
hidden layer. Every hidden neuron (represented by a circle) has ReLU activation
function. Hidden neurons are partitioned into $m$ groups.  Input and hidden
layer are fully connected with trainable weights, whereas as each group is
independently connected to an output neuron with non-trainable weights fixed
to~1.  This ensure that the network's output is always non-negative, and allows
learning a variety of non-trivial ranking functions.
\begin{figure}
  \centering
  \begin{tabular}{ccc}
    \begin{lstlisting}[boxpos=b]
while (x > z || y > z) {
  if (x > z)
    x--;
  else if (y > z)
    y--;
}
    \end{lstlisting}
    &
    \begin{tikzpicture}[font=\scriptsize,scale=0.9]

    \node (x1) [draw, circle, inner sep=2pt, minimum size=0.4cm]
    at (0,1.75) {};
    \node (x2) [draw, circle, inner sep=2pt, minimum size=0.4cm]
    at (0,1) {};
    \node (x3) [draw, circle, inner sep=2pt, minimum size=0.4cm]
    at (0,.25) {};

    \def.2cm{.2cm}
    \node (l1) [left=.2cm of x1, anchor=east] {\tt x};
    \node (l2) [left=.2cm of x2, anchor=east] {\tt y};
    \node (l3) [left=.2cm of x3, anchor=east] {\tt z};

    \draw (l1) edge[->] (x1);
    \draw (l2) edge[->] (x2);
    \draw (l3) edge[->] (x3);

    \node (y1) [draw, circle, inner sep=2pt, minimum size=0.4cm] at (1,1.5) {};
    \node (y2) [draw, circle, inner sep=2pt, minimum size=0.4cm] at (1,.5) {};
    \node () [above=.5mm of y1] {ReLU};
    \node () [below=.5mm of y2] {ReLU};

    \draw (x1) edge[->] node[above] {$1$} (y1);
    \draw (x2) edge[->] node[above,pos=.8] {$1$} (y2);
    \draw (x3) edge[->] node[above,pos=.7, xshift=-1mm] {$-1$} (y1);
    \draw (x3) edge[->] node[below] {$-1$} (y2);

    \node (z) [draw, circle, inner sep=2pt, minimum size=0.4cm] at (2,1) {};

    \draw (y1) edge[->] node[above] {$1$} (z);
    \draw (y2) edge[->] node[above] {$1$} (z);

    \node (o) [right=.2cm of z, anchor=west, inner sep=0] {};
    \draw (z) edge[->] (o);

    \node[draw=none] at (0,-0.5mm) {};
    \end{tikzpicture}\\
    \footnotesize (a) & \footnotesize (b)
  \end{tabular}
  \caption{Program with SOR ranking function.}
  \label{fig:progsor}
\end{figure}
Consider, for instance, the example of Fig.~\ref{fig:progsor}.
This program does not admit a linear ranking function. As it turns out,
the simple neural network in Fig.~\ref{fig:progsor}b is a correct
ranking function for this program, and was efficiently learned by our prototype.
Notably, this is the function $\relu(x-z) + \relu(y-z)$, which is
non-linear and correspond to a special case of SOR function with $m=1$.

\paragraph{Lexicographic Ranking Loss}

For program with possibly nested loops, we train general models ($m > 1$)
so their output descends a lexicographic order along the traces.
More specifically, we train them so that every
transition may strictly decrease any output neuron by the constant $\delta$, as long as
all other output neurons with smaller index do not increase.  That is, for
every transition observation $(\bm{x}, \bm{y})$ there exists an index
$\bm{j} \in \{1,\dots,m\}$ such that
\begin{align}
  &f_\theta(\bm{y})_{\bm{j}} \leq f_\theta(\bm{x})_{\bm{j}} - \delta&&\text{and}\\
  &f_\theta(\bm{y})_i \leq f_\theta(\bm{x})_i&&\text{for all}~i < \bm{j}.
\end{align}
To train a {\em lexicographic neural ranking function}, we augment the
dataset so that every transition observation $(\bm{x}, \bm{y})$ is
associated with a desired lexicographic index $\bm{j}$.  Then, we optimise
the average value of the following loss function:
\begin{equation}
\begin{split}
  \mathcal{L}_\theta(\bm{x},\bm{y},\bm{j}) = \max\{f_\theta(\bm{y})_{\bm{j}} - f_\theta(\bm{x})_{\bm{j}} + \delta, 0 \} +
  \\
  \sum_{i = 1}^{\bm{j}-1} \max\{f_\theta(\bm{y})_i - f_\theta(\bm{x})_i, 0\}.
\end{split}
\end{equation}
Lexicographic indices are added to the dataset before training. It is a
good heuristic to associate indices to the nesting of the corresponding loop
header, by increasing index from outermost to innermost nesting.
Then, we minimise the loss function until it attains a value that is
sufficiently close to zero. We round all parameters to the nearest
integer or to few binary digits and pass it to the formal verifier.
As we show, this indexing and rounding heuristic is effective in practice.

\section{Acknowledgments}
\input{acks}

\end{document}

\section{Termination Analysis}\label{sec:ranking-nn}\label{sec:learning-ranking-functions} \label{sec:term-analysis-ml}\label{sec:prelims}

\paragraph{Programs and Transition Systems}

A computer program is a list of instructions that, together with the machine
interpreting them, defines a state transition system over the state space of
the machine.  A state transition system $P$ is a pair $(S,T)$ where $S$ is a
countable (possibly infinite) set of states and $T \subset S \times S$ is a
transition relation.  A \emph{run} of $P$ is any sequence of states
\begin{equation}
  s_0, s_1, s_2, \dots \label{eq:run}
\end{equation}
such that $(s_i,s_{i+1}) \in T$ for all $i \geq 0$.  A state without any
successors is a terminating state.  We say that a program terminates if all
its runs are finite.

\paragraph{Ranking Functions}

To determine whether a program terminates, our method attempts to find a
ranking function for it. A function $f \colon S \to W$
is a ranking function for the program $P$ if
\begin{equation}
  f(t) < f(s)\quad \text{for all } (s,t) \in T
\end{equation}
and the relation $(W,<)$ is well founded~\cite{Floyd67}.  The standard example
is a function that maps the traces to sequences of numbers that (i)~decrease a
discrete amount and (ii)~are bounded from below.  The existence of a ranking
function proves that the program terminates for every possible input. Every
program that do not terminate necessarily lacks a ranking function. In
Sect.~\ref{sec:learning}, we consider non-negative functions
that map to real numbers and decrease by a discrete amount. Furthermore, we also
consider lexicographic ranking functions which are are a special case of a
ranking function $f \colon S \to W$ where $W$ is a set of tuples and the
associated well founded order $<$ is a lexicographic order. Such lexicographic
arguments can be useful when considering nested loops.
\begin{figure}
  \centering
  \begin{tabular}{cc}
    \begin{lstlisting}[boxpos=b]
while (i < k) {
  j = 0;
  while (j < i) {
    j++;
  }
  i++;
}
    \end{lstlisting}
    &
    \begin{tikzpicture}[font=\scriptsize \tt, inner sep=0, minimum size=10pt]
      \node[draw,circle] (l1) {L1};
      \node[draw,circle,below=.2cm of l1] (l2) {L2};
      \node[draw,circle,below=.2cm of l2] (l3) {L3};
      \node[draw,circle,below=.2cm of l3] (l4) {L4};
      \node[draw,circle,below=.2cm of l4] (l5) {L5};
      \node[draw,circle,left=1.2cm of l2] (l6) {L6};
      \path (l1) edge[->] node[right] {
        \begin{tabular}{l}iload\_0\\iload\_2\end{tabular}} (l2);
      \draw (l2) edge[->] node[above] {if\_icmpge L6} (l6);
      \path (l2) edge[->] node[right] {
        \begin{tabular}{l}iconst\_0\\istore\_1
      \end{tabular}} (l3);
      \path (l3) edge[->] node[right]
            {\begin{tabular}{l}iload\_1\\iload\_0\end{tabular}} (l4);
      \path (l4) edge[->] node[right]
            {\begin{tabular}{l}if\_icmpge L5\end{tabular}}(l5);
            \path[draw] (l4) -- node[below,xshift=-.2cm]
                 {\begin{tabular}{l}iinc 1,1\\goto L3\end{tabular}}
                 ($(l4)-(1.4,0)$)
      -- ($(l3)-(1.4,0)$) edge[->] (l3);
      \path[draw] (l5) -- node[below,xshift=.2cm]
           {\begin{tabular}{l}iinc 0,1\\goto L1\end{tabular}} ($(l5)+(1.6,0)$)
      -- ($(l1)+(1.6,0)$) edge[->] (l1);
    \end{tikzpicture}\\
    \footnotesize (a) & \footnotesize (b)
  \end{tabular}
  \caption{Program with nested counting and its CFG annotated by the respective bytecode.}
  \label{fig:cfg}
\end{figure}

\paragraph{Control Flow Graph} A control flow graph (CFG) for program $P$
is a finite directed graph $G = (L, E)$ where $L$ is a finite set
of control locations and $E \subseteq L \times L$ is a set of control edges.
Let $\lambda \colon S \to L$ map states to the respective control location,
then a CFG satisfies that $(\lambda(s), \lambda(t)) \in E$ for all $(s,t) \in T$.

For a Java program, a CFG can be obtained from its bytecode as shown
in Fig.~\ref{fig:cfg}, where control locations correspond to source and
target positions of jump instructions. Special control locations are
the loop headers, that is, the dominators (entry locations) of the
strongly connected components in the graph~\cite{cfg}; for instance, the
loop headers for Fig.~\ref{fig:cfg}b are L1 and L3. For simplifying our analysis,
we discover ranking functions that decrease between every two loop headers
rather than every two instructions; this is sufficient for proving termination.

\section{Related Work}\label{sec:related-work}

Termination analysis is a large and mature area with a long history.  Hence,
we will only discuss previous work that is directly related to this paper.
State-of-the-art methods for termination analysis can be categorized as
either \emph{direct} or \emph{indirect}.

\paragraph{Direct}

Tools that follow the direct approach to termination analysis construct
termination arguments that apply directly to the input program without
translating it to a different representation.  Such arguments are often
found by combining static analysis and constraint solving to synthesise
ranking functions.  Depending on the class of input programs these
constraints can be linear programs~\cite{PodelskiR04}, semi-definite
programs~\cite{Cousot05}, semi-algebraic systems~\cite{ChenXYZZ07}, or
formulae over SMT theories~\cite{DBLP:journals/fmsd/CookKRW13}.  To deal
with complex programs lexicographic ranking functions were introduced.  To
synthesise such ranking arguments constraint solving has been combined with
combinatorial search or abstract interpretation to synthesise
lexicographic~\cite{BradleyMS05,icalp/BradleyMS05,10.1007/978-3-642-54862-8_12},
piecewise~\cite{Urban13}, and disjoint well-founded
relations~\cite{pldi/CookPR06,10.1007/978-3-642-36742-7_4}.

\paragraph{Indirect}

Indirect termination describes methods that translate the input into a
different model of computation and prove that the translated version
terminates.  This requires a guarantee that termination of the translation
implies the termination of the original program.  These alternate models of
computation can be term rewrite
systems~\cite{GieslABEFFHOPSS17,BrockschmidtOEG10,rta/OttoBEG10}, constraint
logic programs~\cite{DBLP:conf/sas/Spoto16}, recurrence
relations~\cite{DBLP:conf/fmco/AlbertAGPZ07}, and Büchi
automata~\cite{HeizmannHP14,DBLP:conf/pldi/ChenHLLTTZ18}.

\paragraph{Termination from Execution Traces}

To our knowledge there are only two tools that utilise execution traces to
synthesise termination arguments: one generates loop bounds and the other
uses SMT to fit ranking functions~\cite{sigsoft/Nori013,LeAFKN20}.  The
earlier utilises execution to create a quadratic program with linear
constraints so that the solution describes a loop bound.  The latter, which
is implemented in the tool DynamiTe, considers traces by themselves together
with their transitive closure.  Using SMT solvers this data is fitted to
ranking function templates to produce ranking function candidates.  If the
SMT query is successful, an off-the-shelf reachability analysis tool is used
to validate the candidate ranking function.

\paragraph{Ranking Measures}\label{sec:ranking-measures}

The concept of learning rankings is not foreign to the machine learning
community~\cite{NIPS2009_3708,10.1145/1102351.1102363,burges2010from}.  This
is commonly referred to as \emph{machine-learned ranking}\ (MLR) and is for
example used for information retrieval~\cite{DBLP:books/daglib/0027504} and
recommender systems~\cite{DBLP:conf/recsys/KaratzoglouBS13}, and search
engines.  However, machine-learned ranking has never been applied to
termination analysis.

\section{Tracing}\label{sec:tracing}
In this section we will discuss how we extract execution traces from programs.
An execution trace is essentially a list of consecutive snapshots of the
program's memory during its execution.  As previously discussed and shown in
\prettyref{fig:arch} program traces are a core part of our approach to
termination analysis. These program traces are generated dynamically, that is
during the termination analysis.

Tracing requires two things, a function that is to be traced and a list of
positions in the function where a snapshot has to be taken. In our case these
positions denote the loop heads of the function. A single execution trace for
this function is then generated by the following steps: \emph{Sampling},
\emph{Execution}, \emph{Snapshot}.  We describe each of these steps below. As we
are working with Java Bytecode we also mention some implementation details
specific to the Java environment and the Java Virtual Machine (JVM). As
mentioned in previous chapters, our approach is conceptually simple and platform
independent. Hence, this could also be applied to more abstract models of
computation. However, due to the need to be able to collect exeuction traces as
training data using a general purpose programming language is more
practical. Furthermore, thanks to the JVM's great tooling we are able to keep
the tracing lightweight. Something that would otherwise require a large
engineering effort.

\paragraph{Sampling:}
Sampling describes the process of generating input data for a function $f$ with
an argument list $l$. Importantly, we only consider deterministic
functions. Hence, two traces of a function with the same argument list $l$ are
identical. This allows us to control the traces using only the input data.  We
use two sampling strategies based on a Gaussian distribution: \emph{pairwise
  anticorrelated sampling} (PAS) and \emph{Gaussian sampling}. PAS uses a
multivariate normal distribution where we enforce the same variance for every
argument in $l$ except for two randomly chosen arguments. For these two chosen
variables we create a covariance. Hence, this is a standard Gaussian
distribution for all variables except for two where we create a covariance. As
an example consider a function with the following signature:
\inlinecode{Java}{void compute(int a, int b, int c, int d)}. If we choose the
pair of arguments $b,c$ as an anticorrelated pair we get the following
covariance matrix:
\[
  \begin{bmatrix}
    1 & 0 & 0 & 0 \\
    0 & 1 & 100 & 0 \\
    0 & 100 & 100 & 0 \\
    0 & 0 &0 &1
  \end{bmatrix}
\]
While $a$ and $d$ are sampled using a Gaussian distribution with variance $1$ we
sample $b$ and $c$ with a covariance of $100$. Gaussian sampling on the other
hand describes a sampling strategy where each variable is sampled independently
from another from a Gaussian distribution with a variance
of $1000$ and no covariance.
\paragraph{Execution:}
We start executing $f$ with the sampled arguments. Using the Java
Virtual Machine Tool Interface (JVMTI) allows us to maintaining control over the
JVM during the exuection of $f$. Once we hit a loop head location, we halt the
exuction and take a snapshot.

\paragraph{Snapshot:}
Using JVMTI we have access to the Local Variable Table (LVT). The LVT contains
all local variables of the function including variables that are only
declared later in the same function (i.e. variables that are invalid at the
current position in the program). We create a
memory snapshot by iterating
through the LVT and reading the values of every valid variable. For invalid
variables we create a placeholder default value (which depends on the type of the
variable). Note that since the types of variables cannot change, the size of the
snapshots is always the same. Once the
snapshot is collected we append it to the trace of the current program. If the
maximum length of a trace is reached we force a termination of the virtual
machine, otherwise we resume the execution.

The resulting list of snapshots constitutes an
execution trace. The goal is to sample the input data in such a
way that we achieve a high coverage of the function and the data therefore best
represents a possible ranking argument while keeping the amount of traces and
therefore data low.

redpajama_set_name: RedPajamaArXiv


Drug crimes carry a wide range of serious penalties, including jail time, fines, loss of your driving privileges and required counseling, education and/or therapy. Prosecution and defense of drug offenses often involve complex legal issues surrounding search and seizure actions by law enforcement as well as scientific and technical examination of drugs seized and tested by crime laboratories.
At the federal level, issues surrounding participation in drug conspiracies are attendant to many federal cases. To address your case, we recommend that you meet with an experienced drug defense attorney to understand your constitutional rights; to determine if possible violations of those rights have occurred; and to explore potential legal defenses and familiarize and prepare yourself for the severe penalties that you may face if convicted of a drug offense in state or federal court.
Leary Porter Law handles cases involving Schedule 1, Schedule 2 and Schedule 3 substances, including but not limited to marijuana, cocaine, crack, PCP, LSD, methamphetamine and Ecstasy as well as cases involving prescription medications such as Percocet, Valium, Xanax, codeine and oxycodone. Consideration for substance abuse and mental health evaluations will often have an important role in the defense of a drug offense prosecution.
A vigorous and zealous defense of a juvenile drug offense prosecution involves hiring experienced counsel who can help you understand all aspects of your case and all options available to you in the resolution of your charges.
Prior to opening her firm in 2011, Ms. Leary was a partner at a prominent criminal defense firm in Fairfax where she earned a reputation among prosecutors and judges as a hardworking, thorough and knowledgeable criminal defense attorney ready to aggressively protect and defend her clients' interests. Since opening her practice, Ms. Leary has continued to build her criminal defense practice.
Integrity, open communication, hard work and preparedness are the cornerstones of Leary Porter Law's efforts on behalf of all of their clients. You can be assured that they will work directly with you throughout the process, keep you informed and ensure you are knowledgeable regarding your options.


text:
1303 Life review (an1303)
This article gives a brief summary of the life of Augustine and his influence on education.
Aurelius Augustine was born in north Africa in the year 354, at the close of the Roman Empire.
His home town is Tagaste, 250 kms (200 miles) from the Mediterranean coast and two thousand feet above it, cut off from the sea by great forests of pine trees.
He lived with his father, Patricius, and mother, Monica.
As a young boy at school, he is beaten by the teacher because he loved to play and could not see the use of learning at school.
One night - then sixteen years old - for the simple thrill of doing wrong, he and his friends steal from the pear tree of a neighbour, and throw the pears to pigs.
At seventeen he takes a concubine ("I was in love with love", he wrote), and at the age of eighteen years is the father of a son.
He completes his Roman education at the capital city of Carthage and becomes a teacher, and opens his own school in his home town of Tagaste. He finds the students noisy, frustrating and difficult.
In search of a philosophy of life he studies astrology, and joins a religious sect called Manichees.
But in Milan he meets a saint, Ambrose, and is converted to the Christian Faith. At Easter time and at thirty three years of age, Augustine is baptised with his son and his best friends.
He gives up lecturing and his ambition to become a Provincial Governor, and chooses a celibate life, with neither wife nor concubine.
VIDEO: Biography of St Augustine
Uploaded on 15 Sep 2010. (6 minutes 11 seconds) Merrimack's community is committed to scholarship and service to others, and provides students myriad opportunities to develop intellectually, spiritually, socially and ethically. At Merrimack (at Andover, Massachusetts, USA), our dedication to the Augustinian values of hospitality, community, and the pursuit of truth will make you feel right at home as you explore the world and gain the experiences you need to chart your future. This video details the origins of St Augustine and how they relate to your experience at Merrimack.
At thirty Augustine is a professor of liberal arts in Rome and soon wins the appointment of Public Orator in Milan, the imperial capital.
Back in Africa Augustine begins to live as a monk in a community of friends. The search for wisdom becomes the one goal of his life. His son Adeodatus dies aged seventeen.
At thirty six Augustine is pressured by the people of Hippo to become their priest, though he is only three years a Christian.
He later commented about this, "I was made to stand at the helm of the ship when I did not know how to hold an oar."
But his acceptance of the Christian Faith had flooded his heart with light.
He is sustained by a brilliant mind and memory (the classics and the Bible he knows by heart) and his faith in God absorbs him completely.
Love now becomes the one goal in his life. He unifies all existence, all feeling, all knowledge, all friendship into one love. And it is love to the utmost.
Augustine founds monasteries to promote the community ideal but circumstances force him to govern and teach the church in his city of Hippo.
He was pressed to become a priest, and then a bishop. In fact he becomes the Christian teacher to the whole Western Empire.
He is faithful to contemplation but finds time to write 113 books.
People take his books to read and publish them before he finishes writing them.
Popular even today are his "Confessions" and his "City of God". He leaves behind him 200 letters and 500 sermons.
In the year 430, when seventy six years of age, Augustine dies while praying. The great Roman empire is in collapse and confusion.
Murder and pillage are everywhere. The Vandals are at the very walls of Hippo, yet Augustine its bishop had become a saint. He made no will and left no property.
So Augustine lives a changing and dramatic life. His is an age of distress, with civilisation falling to pieces around him.
He has a restless, seeking, dissatisfied adolescence which he later confesses as "sinful", and a spiritual unease.
But peace comes to his heart at the age of thirty three.
He awakens out of doubt and confusion, a wave of religious faith breaking within his mind.
He writes that God called to him, broke through his deafness and touched him: "I came to know You late," he prayed.
In his personality and emotions, before and after this turning point, Augustine needs to love and to be loved.
He is timid, however, and finds it hard to give his confidence to others. He knows the difficulty of entering into communication with others.
But once he overcomes that difficulty, what capacity for friendship, what power of attraction!
He remains young in spirit till the end of his life, keeping the memory of his childhood and youth clearly before him.
He is refined at heart, sensitive to feeling and in love with truth. Of his writings an admirer has said, "his words have a beauty and a thrill of emotion that I find in no other."
Sixteen centuries separate our present age from Augustine of Hippo. After he died his the Christian Church in North Africa disappeared, destroyed; its descendants passed to Islam and now speak Arabic.
His land above the pine forests we now know as Algeria.
But his influence entered Europe, and Augustine came to be recognised in history as the founder of the Middle Ages and the architect of Western civilisation.
In his teaching he established the patterns of learning upon which the first universities were founded; our western contemporary ideals of freedom, progress and social justice owe much to him.
He is called in fact the spiritual and intellectual ancestor of the 20th century. People who read his books today discover that in many ways he is truly a modern scholar.

redpajama_set_name: RedPajamaCommonCrawl


In cooperation with Volga-Dnepr's partner, Bolloré Logistics, one of the airline's An-124-100 freighters delivered six satellites from their manufacturing facility in Toulouse, France, to Cayenne in French Guiana.
"As an air cargo operator, we understand all too well how important stable internet access is, with customers relying on real-time cargo shipment data, airline specialists communicating through internet systems to guarantee cost-effective and timely deliveries, and innovative technologies being facilitated through the development of internet solutions. We are, therefore, especially honoured to be part of the OneWeb constellation project, which will enhance the quality of life for customers globally," stated Axel Kaldschmidt, Global Director Aerospace of Volga-Dnepr Group.
Volga-Dnepr Airlines has been operating its unique fleet of An-124-100 and Il-76TD-90VD freighters for more than 29 years, providing dedicated airlift for project shipments for various industries, including the aerospace, oil&gas, energy, automotive and humanitarian sectors and others.
In 2018, the company performed more than 55 flights carrying satellites and related equipment, contributing to the development of the space industry.


HURRY on over to CVS.com where you can save 40% off ONE regular priced item + snag Free Shipping when you use the code 40FORU at checkout. How cool is that?
One idea, head over and grab this Conair Ion Shine Ionic Styler Dryer for ONLY $11.99 shipped (regularly $19.99) when you use promo code 40FORU at checkout. This hair dryer includes a concentrator and finger diffuser.
This is just one idea. You can find plenty of other items to use this on.


In this episode of the China in the World podcast, Paul Haenle joined Kaiser Kuo, editor-at-large of SupChina, to discuss next steps for DPRK diplomacy and tensions between the United States and China over trade, Taiwan, and the Belt and Road Initiative.
Haenle shared his experience working as White House representative to the Six-party talks in the Bush administration. He said China's relations with North Korea reached a historic low in 2017 due to the leadership's frustration with Pyongyang's provocative nuclear and missile tests, leading to Beijing's increased willingness to join the international maximum pressure campaign. Haenle argued the Singapore summit reduced U.S. leverage with North Korea and produced a vague statement which failed to advance denuclearization. On the U.S.-China trade dispute, Haenle urged the Trump administration to work closely with U.S. allies who share concerns about China's industrial policies, market access restrictions, and intellectual property rights violations. He expressed concern over the lack of a comprehensive U.S. strategy toward China, especially with regard to cross-Strait relations and the Belt and Road Initiative.
Paul Haenle holds the Maurice R. Greenberg Director's Chair at the Carnegie–Tsinghua Center for Global Policy based at Tsinghua University in Beijing. His research focuses on Chinese foreign policy and U.S.-China relations.


One concert-goer got the surprise of a lifetime when country rockstar, Eric Church, personally greeted her on stage. While fans have gotten high-fives and smiles from their favorite stars, this little girl got a full-blown serenade.
While on his Double Down Tour, Church has been giving fans the experience of a lifetime. From his stage presence to his insane vocals, the crowd can't get enough. The tour expands into 19 cities where the singer will perform two completely unique shows in each city. While fans lined up to get their hands on a pair of tickets for the six-month-long tour, two parents got an extra seat for their daughter's first concert.
At Church's January 25th show in St. Louis, he noticed one fan sitting front row having the time of her life. While the singer was rockin' out to his hit, "Springsteen" he made his way over to the little girl. While her mom propped her up, Church bent down to hold her hand while still singing. Clearly loving his newest fan, he then proceeded to sit down on the stage and sing with her!
The 2012 hit, "Springsteen" had an overwhelming success following its release. The single debuted across all the charts and hit No.1 on the Billboard Hot Country. It later went on to be 3x platinum certified in the United States. The song has gone on to be one of Church's most well-known singles and clearly, a crowd favorite at concerts.
Watch the sweet moment between Church and his newest fan below!


text:
Q: How do I add all elements in an array using SSE2? Suppose I have a very simple code like:
double array[SIZE_OF_ARRAY];
double sum = 0.0;

for (int i = 0; i < SIZE_OF_ARRAY; ++i)
{
    sum += array[i];
}

I basically want to do the same operations using SSE2. How can I do that?

A: Here's a very simple SSE3 implementation:
#include <emmintrin.h>

__m128d vsum = _mm_set1_pd(0.0);
for (int i = 0; i < n; i += 2)
{
    __m128d v = _mm_load_pd(&a[i]);
    vsum = _mm_add_pd(vsum, v);
}
vsum = _mm_hadd_pd(vsum, vsum);
double sum = _mm_cvtsd_f64(vsum0);

You can unroll the loop to get much better performance by using multiple accumulators to hide the latency of FP addition (as suggested by @Mysticial).  Unroll 3 or 4 times with multiple "sum" vectors to bottleneck on load and FP-add throughput (one or two per clock cycle) instead of FP-add latency (one per 3 or 4 cycles):
__m128d vsum0 = _mm_setzero_pd();
__m128d vsum1 = _mm_setzero_pd();
for (int i = 0; i < n; i += 4)
{
    __m128d v0 = _mm_load_pd(&a[i]);
    __m128d v1 = _mm_load_pd(&a[i + 2]);
    vsum0 = _mm_add_pd(vsum0, v0);
    vsum1 = _mm_add_pd(vsum1, v1);
}
vsum0 = _mm_add_pd(vsum0, vsum1);    // vertical ops down to one accumulator
vsum0 = _mm_hadd_pd(vsum0, vsum0);   // horizontal add of the single register
double sum = _mm_cvtsd_f64(vsum0);

Note that the array a is assumed to be 16 byte aligned and the number of elements n is assumed to be a multiple of 2 (or 4, in the case of the unrolled loop).
See also Fastest way to do horizontal float vector sum on x86 for alternate ways of doing the horizontal sum outside the loop.  SSE3 support is not totally universal (especially AMD CPUs were later to support it than Intel).
Also, _mm_hadd_pd is usually not the fastest way even on CPUs that support it, so an SSE2-only version won't be worse on modern CPUs.  It's outside the loop and doesn't make much difference either way, though.

redpajama_set_name: RedPajamaStackExchange


JGL Ltd is one of the North Wests fastest growing painting and decorating companies. All of our operatives are City and Guilds qualified, and all of our work is guaranteed. We provide quality painting and decorating solutions for every requirement be it commercial, residential, or construction.
As well as being period property specialists, we are also the preferred contractors of Manchester working. We have built up excellent working relationships with many respected Interior designers, Architects and Building contractors. We are based in Manchester, but more than happily cover Lancashire, Cumbria and the surrounding areas. Please get in touch today if you are interested in any of the services that we have to offer.
Click here to see our industrial accreditations.


text:
Africa Oil & Power to Honor Senegal President as "Africa Oil Man of the Year"
Africa Oil & Power will present the award to H.E. Macky Sall at its annual conference in Cape Town
H.E. Macky Sall is renowned for his efforts to revive Senegal's economy and create an attractive market for oil and gas
H.E. Macky Sall will provide a keynote address at Africa Oil & Power 2019
CAPE TOWN, SOUTH AFRICA - EQS - June 24th, 2019 - H.E. Macky Sall, President of the Republic of Senegal, will be bestowed with the prestigious "Africa Oil Man of the Year" award during the Africa Oil & Power conference, to be hosted October 9-11, 2019 in Cape Town. The President will be presented the award during the conference, during which he will also present the keynote address.
Senegal is a global hotspot for oil and gas discoveries -- well-known as the place in Africa to make major oil and gas finds, due in large part to a decades-long campaign by Sall to improve transparency, create an attractive investment environment and spark new growth.
"As African countries across the continent aim to spur growth and diversify economically, Senegal is a prime example of a country making energy work -- creating an enabling environment for business to succeed, attracting huge international investments, while providing for a strong local capacity and downstream investment options," said Guillaume Doane, CEO of Africa Oil & Power. " H.E. Macky Sall is one of Africa's top leaders, not just in oil and gas, but as an advocate for overall economic success. We are honored to present him this award."
Sall first worked as the CEO of Petrosen from 2000 -- 2001, before becoming the country's Minister of Mines Energy and Hydraulics in 2001. After a long political career in Senegal, Sall was elected president of Senegal in 2012, and pushed through a series of reforms to revive Senegal's economy and attract international investors.
"In a continent where border disputes have held back the development of offshore resources, President Macky Sall insists on a more productive outcome. He worked with his counterpart of Mauritania, H.E. Mohamed Ould Abdel Aziz, to secure an agreement to jointly develop offshore resources for the mutual benefit of both countries" said Jude Kearney, former Deputy Assistant Secretary for Service Industries and Finance at the U.S. Department of Commerce during the Clinton Administration and currently President of Kearney Africa Advisors.
This form of agreement represents the best practice for the development of cross-border resources, and in this particular case is based on the landmark Frigg Agreement of 1976 between the UK and Norway. That case showed that when leaders work together resources can be developed peacefully to benefit the people of both nations.
"The agreement between Mauritania and Senegal paved the way for the development of the Tortue field through cross-border unitisation, with a 50%-50% initial split of costs, production, and revenue, as well as a mechanism for future equity redeterminations based on field performance. It takes leadership, vision and foresight to get this done". Continued Kearney.
Today, Senegal has one of the fastest growing economies in the world, and is the fastest growing economy in West Africa. Sall has closely guided the development two multi-billion dollar oil projects off the coast of Senegal -- the world-class SNE oilfield and the Greater Tortue/Ahmeyim gas project. The Greater Tortue project reached FID in December of 2018, and has already awarded several initial contracts, including the EPCIC contract for the development of the needed FPSO to Technip for an estimated $500 million to $1billion. The SNE oilfield is expected to reach FID this year. Both projects are scheduled to start producing export revenues in the early 2020s.
To ensure the country's new oil revenue will directly benefit the country, Sall advocated for a new hydrocarbons code, which was approved by the national assembly this year, and he also created the agency Cos-Petrogaz to oversee the oil and gas sector and issue licenses. Other reforms aimed at promoting transparency included limiting the presidential terms from seven years to five years, to be renewed once, and launching the Emerging Senegal Plan in 2014, which provides detailed planning for Senegal's continued social and economic development.
The fourth annual Africa Oil & Power, to be held from Oct. 9-11 in Cape Town, has a theme of "Make Energy Work" that will focus on how oil, gas and power can generate greater opportunities for the people of African nations and stimulate sustainable economic growth.
Africa Oil & Power industry leaders will celebrate Sall's notable achievements and spark conversations on Making Energy Work throughout the continent.
The last recipient of this award was OPEC Secretary General, H.E Mohammed Sanusi Barkindo . H.E. Barkindo guided OPEC through one of its most turbulent periods, with a sustained oil price decline and a loss in global market share. He is credited with restoring market stability on a global scale through the landmark deal between OPEC and non-OPEC members to cut oil production.
Download Image: https://bit.ly/2KzrHzk
Africa Oil & Power


text:
Home Science Research: Forest fragmentation disrupts parasite infection in Australian lizards —
Research: Forest fragmentation disrupts parasite infection in Australian lizards —
Janet R. Aguilar
In a study with implications for biodiversity and the spread of infectious diseases, CU Boulder ecologists have demonstrated that deforestation and habitat fragmentation can decrease transmission of a parasitic nematode in a particular species of Australian lizard, the pale-flecked garden sunskink.
The new experimental research, published today in the journal Ecology, found that specimens of the blue and brown-colored, index finger-length skinks who live in isolated forest plots were 75 percent less likely to be infected with parasitic worms than their counterparts living in untouched, continuous forests — an indication that the parasite's life cycle had been disrupted.
A decrease in parasite prevalence isn't necessarily good or bad for an ecosystem, the researchers said, but it can result in dramatic changes.
"Parasites are a massive unseen component of an ecosystem and there so many that we don't see," said Associate Professor Kendi Davies of CU Boulder's Department of Ecology and Evolutionary Biology (EBIO). "Parasites regulate populations and influence multiple hosts. It's largely unknown how these complex interdependencies respond to changes."
Habitat fragmentation in the form of deforestation remains a major threat worldwide. Scientists estimate that nearly one-third of global forests have disappeared, leaving behind a patchwork of ecological "islands" that can threaten food chains and alter long-standing species interactions
"Fragmentation is a big deal because it leads to loss of biodiversity and ecosystem functions" said Julian Resasco, lead author of the study and a postdoctoral researcher in EBIO. "It can also change the way diseases spread, with the potential to impact human health."
The new study was conducted at the long-running Wog Wog Habitat Fragmentation Experiment, a 33-year-old continuously-run experiment in the eucalyptus forests of New South Wales, Australia. The site allows researchers to compare uninterrupted forestland to forest fragments that have been isolated by clear-cutting and burning.
Resasco zeroed in on skinks after a chance observation. While examining the gut contents of many historical specimens preserved in a museum, he noticed that the commonly-found lizards had been infected with a particular parasitic nematode. After consulting with Australian colleagues, he learned that it was, in fact, a brand new species.
"I wanted to quantify infections by these nematodes to see if fragmentation had an effect on parasitism," Resasco said.
The nematodes use a small amphipod crustacean species as an intermediate host, which is in turn eaten by the skink, resulting in infection. But forest fragmentation significantly reduces the moist leaf litter habitat that these amphipods require, depriving the skinks of a meal and the parasites of a transmission pathway.
The study found that among skinks living in continuous forest, 55 percent contained nematodes compared to just 11 percent of skinks living in the fragments.
"We see the consequences of messing with key players in the landscape," said Resasco.
The next step, the researchers said, is to think in even longer timescales. Now more than thirty years in at Wog Wog, parts of the landscape there have gradually changed from clear-cut to pine plantation forest, which could prompt a rebound.
"Pine forests are a pretty desirable place for the amphipods to live," said Matthew Bitters, a doctoral researcher in EBIO and a co-author of the study. "So if they do recover, will that mean a rise in skink infections again? Or has something else emerged to disrupt the transmission?"
"Fragmentation research has a long history of studying species interactions such as pollination, seed dispersal and predation," said Resasco. "Parasitism has received less attention but such research is important for understanding how landscape changes affect biodiversity and disease transmission."
Previous articleStudy: A prosthetic arm that decodes phantom limb movements — (Details)
Next articleTech: Researchers remove silicon contamination from graphene to double its performance — (Report)
2033 Hickory Lane Savage, DC 20763 202-519-4101 Almost all Tdnews staff, including reporters, can be contacted by e-mail. In most cases the e-mail address follows this formula: first initial + last name + @tunisiesoir.com. For example, Laura F. Nixon is [email protected]
New discoveries show Tibet was the source of Ice Age fauna


I wish to inform you that in absence of any default you may go to Kuwait and there may not be any restriction. In absence of default law enforcement agencies may not restrict your entry. As last payment will be paid by you thus creditor may not restrict your movement outside country.
I have unpaid bank loan in kuwait of kd5,000 and i left kuwait in 2016 and making re-entry to kuwait in couple of days. Is there any chances of getting arrested in Kuwait's immigration? Kindly reply its little urgent will be awaiting your reply.


What a month for Hartford Primary School in Cheshire!
Hartford Primary joined Sycol in 2014 and this September we saw our existing team of Green belt Leads graduate to Blue belt, and our Blue belt Leads graduate to the prestigious Black belt level (you can find out more about progressing through the belt system here).
We were also pleased to be able to train a brand new team of Green belt Leads – continuous improvement is obviously an ongoing initiative for Hartford Primary.
Congratulations to Headteacher Mair Fairweather and everyone involved. Quite an all-round achievement!


All companies, regardless of their size or solvency, must ensure that they have appropriate systems for dealing with statutory demands.
In my last article, I looked at the use of statutory demands. Time now to go through the looking glass and examine the impact of demands on the companies which receive them.
A company which receives a statutory demand has 21 days to respond. If it does nothing, it is deemed to be insolvent and will almost certainly be faced with a winding up application.
In a large number of cases, it has to be admitted, that deemed insolvency simply reflects reality. However, there are many other cases in which solvent companies create unnecessary problems for themselves by failing to act promptly on receipt of a demand.
Unfortunately, no-one knows when a statutory demand is going to pop up in the morning post, so all companies, regardless of their size or solvency, must ensure that they have appropriate systems for dealing with them.
As noted above, a company must respond to a demand within 21 days of receiving it. Unlike many other areas of the law, there is no wriggle room here. Many years ago, the High Court ruled that those 21 days are set in stone and that courts have no power to extend the time limit.
Twenty-one days sounds like a lot of time, but it's surprising how many companies fail to meet that deadline. The case reports are full of examples of companies which have been just one or two days late in their response. What lessons can be drawn from those cases?
There are many ways in which a demand can be validly served on a company. The two most common are by mail addressed to the company's registered office and hand delivery to the company's registered office.
if you use your accountant's office as your registered office, make sure that your accountant keeps ASIC informed if he or she changes address (or if you change accountant).
Of course, keeping a registered office address up to date is only half the battle. What does a company do if a creditor claims to have served a statutory demand on a particular date but the company didn't receive it until a couple of weeks later?
Judges are often called on to decide who is telling the truth in this situation. As I mentioned in my previous article, canny creditors will keep records of when statutory demands were sent out. It's No Contest when a judge has to decide between a creditor who has good records and a company whose only witness is an office junior or receptionist who has only a vague memory of what happened on the critical day.
the office procedures can be tailored to fit the circumstances of the company.
all staff and directors should be made aware of the importance of a statutory demand, and there should be a designated person to handle statutory demands.
We've got the demand: what do we do now?
Contact your lawyer right away! This may be easier said than done, for a couple of reasons.
The first is human nature. A statutory demand can be a shock to the system, especially if it's sent by a long-term customer or client, of if there has been no hint that the creditor is unhappy. It's quite understandable that your first reaction might be to pick up the phone and try to sort out the problem informally. Resist that temptation: the legal clock is now running on the survival of your company, and (dramatic as it may sound) every minute counts. There'll be time to talk to the creditor once you've prepared your legal response.
The second possible hitch is finding your lawyer. Some small companies may not even have a lawyer, but even companies with lawyers may sometimes experience problems arranging an appointment. The reason is that a statutory demand is a declaration of war, and the creditor will not go out of its way to make life easy for the recipient company. A South Australian judge recently commented that he was seeing increased numbers of statutory demands being served just before Christmas - when, he commented, many companies would have difficulty in getting legal advice.
Accordingly, if you don't have a regular lawyer, at least make sure that you have the name and contact details of a lawyer who can be contacted in an emergency. If you have a lawyer, make sure that you have contact details for times when the lawyer's office may be shut.
What will my lawyer tell me?
That all depends upon the circumstances.
apply to the court to have the demand set aside.
With the first two options, it is again important to keep good records. A company which pays the debt even just one day late will still have failed to comply with the demand and will be deemed to be insolvent, so the date of any payment is important. If the creditor agrees on a compromise, that agreement should be put in writing and should include an undertaking from the creditor to withdraw the statutory demand (agreements made over the phone aren't worth the paper they're written on).
Most applications to set aside a statutory demand claim that there is a genuine dispute about the debt or that the creditor actually owes money to the company.
It is also possible to argue that the statutory demand wasn't in a form that complied with the statutory requirements in the Corporations Act and Regulations. However, the Corporations Act makes it clear that this argument will only succeed if the defects in the demand would cause serious injustice to the company: a missing full stop or a minor typing error just don't cut it.
At this point, it might seem that the law is stacked against companies which receive statutory demands. That is definitely not true when it comes to disputing the debt claimed in a demand.
A demand will be set aside if the company can show that there is a plausible argument that the debt is genuinely disputed. The courts take the view that a set-aside application is not the appropriate occasion for a full trial of a commercial dispute, so the threshold for a "plausible" argument is fairly low (although it must be more than just a simple assertion that "we don't owe the money").
What happens if the demand is not set aside?
Making a set-aside application stops the statutory demand clock. If the application is dismissed, the company has seven days to comply with the demand. At the end of that seven days, the company will be deemed to be insolvent.
Once the company is deemed to be insolvent, the creditor can apply to have the company wound up.
The sad reality is that most winding up applications are just rubber-stamp affairs. Most companies which have failed to pay a statutory demand debt or even to persuade a court that the debt is genuinely disputed don't turn up in court to contest the winding up application.
That said, there are a handful of situations in which a winding up application might be successfully resisted. For example, the company may never have received the demand or, despite have failed to comply with the demand, it might actually be solvent. One thing that cannot be done, however, is to oppose a winding up order using arguments that could have been (or were) used in a set-aside application.
There are also two out of court possibilities.
The company may be able to reach an out of court settlement with the creditor. That does not, however, totally remove the threat of winding up: other creditors can apply to take over the winding up application.
The other possibility is to place the company in voluntary administration before the court hears the winding up application. The court then has to decide whether to suspend the winding up application while the voluntary administration is in force. It is unlikely to do this if it believes that the voluntary administration is just a sham designed to postpone the inevitable.