# Improving Mitosis Detection Via UNet-based Adversarial Domain Homogenizer
††thanks: * Indicates equal contribution.

1st Tirupati Saketh Chandra  Electrical Engineering
Indian Institute of Technology Bombay
Mumbai, India
0000-0002-0325-5821  2nd Sahar Almahfouz Nasser  Electrical Engineering
Indian Institute of Technology Bombay
Mumbai, India
0000-0002-5063-9211  3rd Nikhil Cherian Kurian  Electrical Engineering
Indian Institute of Technology Bombay
Mumbai, India
0000-0003-1713-0736  4th Amit Sethi  Electrical Engineering
Indian Institute of Technology Bombay
Mumbai, India
0000-0002-8634-1804

###### Abstract

The effective localization of mitosis is a critical precursory task for
deciding tumor prognosis and grade. Automated mitosis detection through deep
learning-oriented image analysis often fails on unseen patient data due to
inherent domain biases. This paper proposes a domain homogenizer for mitosis
detection that attempts to alleviate domain differences in histology images
via adversarial reconstruction of input images. The proposed homogenizer is
based on a U-Net architecture and can effectively reduce domain differences
commonly seen with histology imaging data. We demonstrate our domain
homogenizer’s effectiveness by observing the reduction in domain differences
between the preprocessed images. Using this homogenizer, along with a
subsequent retina-net object detector, we were able to outperform the
baselines of the 2021 MIDOG challenge in terms of average precision of the
detected mitotic figures.

###### Index Terms:

MIDOG, domain generalization, mitosis detection, domain homogenizer, auto-
encoder.

##  I Introduction and Related Work

The demand for robust models which perform well on unseen testing data has
increased rationally in the last two years, especially in the medical domain.

In many practical applications of machine learning models domain shift occurs
after training, wherein the characteristics of the test data are different
from the training data. Particularly in the application of deep neural
networks (DNNs) to pathology images, the test data may have different colors,
stain concentration, and magnification compared to what the DNN was trained on
due to changes in scanner, staining reagents, and sample preparation
protocols. MIDOG2021 [20] was the first MICCAI challenge that addressed the
problem of domain shift as it is one of the reasons behind the failure of
machine learning models after training, including those for mitosis detection
techniques when tested on data from a different domain (scanner) than the one
used during the training. MIDOG2021 was the first MICCAI challenge that
addressed the problem of domain shift due to change in scanner [20].

Domain generalization is the set of techniques that improve the prediction
accuracy of machine learning models on data from new domains without assuming
access to those data during training. Proposing and testing various domain
generalization techniques was the main goal of the MIDOG2021 challenge. In
this section, we introduce the most significant notable solutions for the
MIDOG20201 challenge before introducing our proposed method.

In [1] the authors modified RetinaNet network for mitosis detection [2] for
mitosis detection by adding a domain classification head and a gradient
reversal layer to encourage domain agnosticism. In this work, they used a pre-
trained Resnet18 for the encoder. For their discriminator, it was a simple
sequence of three convolutional blocks and a fully connected layer. The domain
classifier was placed at the bottleneck of the encoder. Breen et al [3]
proposed a U-Net type architecture that outputs the probability map of the
mitotic figures. These probabilities get converted into bounding boxes around
the mitotic figures. They used a neural style transfer (NST) as a domain
adaptation technique. This technique casts the style of one image on the
content of another. The method proposed by [4] consists of two parts, a patch
selection and a style transfer module. To learn the styles of images from
different scanners, they used a StarGAN. A two steps domain-invariant mitotic
detection method was proposed by [5]. This method is based on Fast RCNN [6].
For domain generalization purposes they used StainTools software [17] to
augment the images. StainTools package decomposes the image into two matrices,
a concentration matrix C and a stain matrix S. By combining the C and S
matrices from different images they produced the augmented images. A cascaded
pipeline of a Mask RCNN [9] followed by a classification ensemble was proposed
by [7] to detect mitotic candidates. A Cycle GAN [8] was used to transfer
every scanner domain to every other scanner domain. In [10] the authors used a
stain normalization method proposed by [11] as a preprocessing step for the
images. Others like [12] merged Hard negative mining with immense data
augmentation for domain generalization was proposed by [12]. Stain
normalization techniques such as [14] and [15] were used in [13] to account
for the domain difference between images. Almahfouz Nasser et al., [16]
proposed an autoencoder trained adversarially on the sources of domain
variations. This autoencoder makes the appearance of images uniform across
different domains.

In this paper, we present our work which is an extension of our proposed
method for MIDOG2021 [16]. Our contribution is three-fold and can be
summarised in as follows. Firstly, we modified [16] by shifting the domain
classifier from the latent space to the end of the autoencoder, which improved
the results drastically. Secondly, we showed the importance of perceptual loss
in preserving the semantic information which affects the final accuracy of the
object detection part. Finally, unlike our previous work, training the auto-
encoder along with the object detection network end-to-end improved the
quality of the homogenized outputs substantially.

##  II Methodology

###  II-A Notations

In domain generalization there are source (seen) domains which are shown to
the model during training, and there are some target (unseen) domains which
are used only during testing. Labelled samples from the source domains are
represented by $D_{ls}$=$\\{(x^{ls}_{i},y^{ls}_{i})\\}^{N_{ls}}_{i=1}$,
unlabelled source domains are represented by
$D_{us}$=$\\{(x^{us}_{i})\\}^{N_{us}}_{i=1}$ and labelled target domains are
represented by $D_{lus}$=$\\{(x^{lus}_{i},y^{lus}_{i})\\}^{N_{lus}}_{i=1}$.
Let the unlabelled images from all subsets be represented by
$D_{all}$=$D_{ls}$ $\cup$ $D_{us}$ $\cup$ $D_{lus}$.

###  II-B Adversarial end-to-end trainable architecture

Inspired by the work of [18], we have used an encoder-decorder network to
translate the patches from different domains (scanners) to a common space. The
translated images are then passed through RetinaNnet [2] for object detection.
The architecture also consists of an adversarial head with domain
classification as an auxiliary task. This head encourages the encoder-decoder
network to erase all the domain- specific information. The architecture of our
method is as shown in figure 1.

Figure 1: The pipeline of our proposed method for mitosis detection.

###  II-C Training Objectives

The object detection loss consists of bounding box loss ($\mathcal{L}_{bb}$)
and instance classification loss ($\mathcal{L}_{inst}$). The bounding box loss
($\mathcal{L}_{bb}$) is computed as smooth L1 loss and the focal loss function
is used for the instance classification ($\mathcal{L}_{inst}$).

In order to ensure that the images translated by encoder-decoder network
contains the semantic information we have used a perceptual loss
($\mathcal{L}_{percp}$). We have used the perceptual loss based on pretrained
VGG-16, which is proposed in [19].

At the end of the adversarial head we have used standard cross entropy loss
($\mathcal{L}_{CE}$) for domain classification.

The overall loss for the end-to-end training is given by,

$\mathcal{L}=\mathcal{L}_{bb}+\mathcal{L}_{inst}+\lambda_{1}\mathcal{L}_{percep}+\lambda_{2}\mathcal{L}_{CE}$
(1)

##  III Data and Experiments

###  III-A Dataset

The experiments were conducted on MIDOG 2021 dataset [20] which consists of 50
whole slide images of breast cancer from four scanners namely Hamamatsu XR
NanoZoomer 2.0, Hamamatsu S360, Aperio ScanScope CS2, and Leica GT450 forming
four domains. Two classes of objects are to be detected namely mitotic figures
and hard negatives. The whole slide images from scanners other than the Leica
GT450 areis labelled. Small patches of size 512 x 512 are mined for supervised
end-to-end training such that the cells belonging to at least one of the
mitotic figures or hard negatives are present in the patch.

The seen and unseen domains i.e., the scanners are $D_{ls}$={Hamamatsu XR
NanoZoomer 2.0, the Hamamatsu S360}, $D_{us}$={Leica GT450}, $D_{lus}$={Aperio
ScanScope CS2} (refer II-A for notations.)

###  III-B Implementation Details

The model is implemented using Pytorch [21] library [21]. For supervised end-
to-end training a batch size of 12 is used with equal number of patches being
included from each scanner. Here the model is trained using FastAI [22]
library default settings with an initial learning rate of $1e^{-4}$. In the
equation 1 we have set the values of hyperparameters as $\lambda_{1}$=10 and
$\lambda_{2}$=25.

###  III-C Results

Two classes of objects – hard negatives, and mitotic figures – are detected.
The models are evaluated on $D_{ls}\cup D_{lus}$. Average precision at IoU
threshold of 0.5 is used as metric for evaluation. End-to-end training with
(AEC_RetinaNet + Pecp) and without using perceptual loss (AEC_RetinaNet) were
tried. The results are compared with the reference algorithm DA_RetinaNet
[23], RetinaNet [24] with and without data augmentation. The results obtained
are as shown in table I.

TABLE I: Results obtained using end -to -end training of models Model | AP-Hard Neg | AP-Mitotic figures | mAP
---|---|---|---
RetinaNet | 0.196 | 0.352 | 0.274
RetinaNet + Aug | 0.238 | 0.619 | 0.429
DA_RetinaNet | 0.347 | 0.655 | 0.501
AEC_RetinaNet | 0.289 | 0.448 | 0.369
AEC_RetinaNet + Pecp | 0.248 | 0.72 | 0.484

The count of mitotic figures is an important clinical goal. So, the
performance on the class of mitotic figures was our focused. The results in
the above table show that the newly designed end-to-end training architectures
performs better than the reference algorithm and the basic Retina-Net based
algorithms. The best performance is in terms of recall metric, which is
evident from the plot shown in figure 2.

The perceptual loss added at the output of the decoder helps in retaining the
semantic information. This information which helps in better object detection.
This is also validated by higher AP score obtained when perceptual loss
component is added.

As shown in figure 3 the modified domain homogenizer produced much more
plausible images than the original domain homogenizer [16].

Besides, figure 4 shows the detection accuracy of our proposed method.

Figure 2: The precision vs recall plot shows that the newly designed end-to-
end model performs better than the baselines especially for the recall values.

##  IV Conclusions

In this paper, we proposed a modified version of our previous domain
homogenizer proposed by us and tested it on the data from for the MIDOG 2021
challenge 2021. We showed that the great impact of the position of the domain
classifier has a significant impact on the performance of the homogenizer.
[EXPLAIN HOW AND WHY] Additionally, our experiments revealed that training the
homogenizer along with the object detection network end-to-end improves the
detection accuracy by a significant margin. Finally, we showed that our method
substantially improves upon the baseline of the MIDOG challenge in terms of
mitotic figures detection.

Figure 3: A visual comparison of the performances of the domain homogenizer
and the modified domain homogenizer(proposed method). Figure 4: Two examples
show the detection accuracy of our proposed method.

## References

  * [1] Wilm, Frauke, et al. ”Domain Adversarial RetinaNet as a Reference Algorithm for the MItosis DOmain Generalization Challenge.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [2] Marzahl, Christian, et al. ”Deep learning-based quantification of pulmonary hemosiderophages in cytology slides.” Scientific reports 10.1 (2020): 1-10.
  * [3] Breen, Jack, et al. ”Assessing domain adaptation techniques for mitosis detection in multi-scanner breast cancer histopathology images.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [4] Chung, Youjin, Jihoon Cho, and Jinah Park. ”Domain-Robust Mitotic Figure Detection with Style Transfer.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [5] Nateghi, Ramin, and Fattaneh Pourakpour. ”Two-Step Domain Adaptation for Mitotic Cell Detection in Histopathology Images.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [6] Girshick, Ross. ”Fast r-cnn.” Proceedings of the IEEE international conference on computer vision. 2015.
  * [7] Fick, Rutger HJ, et al. ”Domain-Specific Cycle-GAN Augmentation Improves Domain Generalizability for Mitosis Detection.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [8] Zhu, Jun-Yan, et al. ”Unpaired image-to-image translation using cycle-consistent adversarial networks.” Proceedings of the IEEE international conference on computer vision. 2017.
  * [9] He, Kaiming, et al. ”Mask r-cnn.” Proceedings of the IEEE international conference on computer vision. 2017.
  * [10] Jahanifar, Mostafa, et al. ”Stain-robust mitotic figure detection for the Mitosis Domain Generalization Challenge.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [11] Vahadane, Abhishek, et al. ”Structure-preserving color normalization and sparse stain separation for histological images.” IEEE transactions on medical imaging 35.8 (2016): 1962-1971.
  * [12] Dexl, Jakob, et al. ”MitoDet: Simple and robust mitosis detection.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [13] Long, Xi, et al. ”Domain Adaptive Cascade R-CNN for MItosis DOmain Generalization (MIDOG) Challenge.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [14] Reinhard, Erik, et al. ”Color transfer between images.” IEEE Computer graphics and applications 21.5 (2001): 34-41.
  * [15] Vahadane, Abhishek, et al. ”Structure-preserved color normalization for histological images.” 2015 IEEE 12th International Symposium on Biomedical Imaging (ISBI). IEEE, 2015.
  * [16] Almahfouz Nasser, Sahar, Nikhil Cherian Kurian, and Amit Sethi. ”Domain Generalisation for Mitosis Detection Exploting Preprocessing Homogenizers.” International Conference on Medical Image Computing and Computer-Assisted Intervention. Springer, Cham, 2021.
  * [17] StainTools Homepage. https://github.com/Peter554/StainTools. Accessed 03 Aug 2022
  * [18] Yaroslav Ganin and Victor Lempitsky. “Unsupervised Domain Adaptation by Backpropagation”. In: Proceedings of the 32nd International Conference on Machine Learning. Ed. by Francis Bach and David Blei. Vol. 37. Proceedings of Machine Learning Research. Lille, France: PMLR, July 2015, pp. 1180–1189. url: https://proceedings.mlr.press/v37/ganin15.html
  * [19] Justin Johnson, Alexandre Alahi, and Li Fei-Fei. “Perceptual losses for real-time style transfer and super-resolution”. In: European Conference on Computer Vision. 2016
  * [20] Marc Aubreville et al. MItosis DOmain Generalization Challenge. Mar. 2021. doi: 10.5281/zenodo.4573978. url: https://doi.org/10.5281/zenodo.4573978
  * [21] Adam Paszke et al. “PyTorch: An Imperative Style, High-Performance Deep Learning Library”. In: Advances in Neural Information Processing Systems. Ed. by H. Wallach et al. Vol. 32. Curran Associates, Inc., 2019. url: https://proceedings.neurips.cc/paper/2019/file/bdbca288fee7f92f2bfa9f7012727740-Paper.pdf
  * [22] Jeremy Howard et al. fastai. https://github.com/fastai/fastai. 2018
  * [23] Frauke Wilm et al. “Domain Adversarial RetinaNet as a Reference Algorithm for the MItosis DOmain Generalization Challenge”. In: Biomedical Image Registration, Domain Generalisation and Out-of-Distribution Analysis. Ed. by Marc Aubreville, David Zimmerer, and Mattias Heinrich. Cham: Springer International Publishing, 2022, pp. 5–13. isbn: 978-3-030-97281-3.
  * [24] Tsung-Yi Lin et al. “Focal Loss for Dense Object Detection”. In: 2017 IEEE International Conference on Computer Vision (ICCV). 2017, pp. 2999–3007. doi: 10.1109/ICCV.2017.324.


# Progress on Local Properties Problems of Difference Sets††thanks: This
research project was done as part of the 2020 NYC Discrete Math REU, supported
by NSF awards DMS-1802059, DMS-1851420, DMS-1953141, and DMS-2028892.

Anqi Li Massachusetts Institute of Technology, 77 Massachusetts Ave,
Cambridge, MA 02139<EMAIL_ADDRESS>Supported by MIT Department of Science.

###### Abstract

We derive several new bounds for the problem of difference sets with local
properties, such as establishing the super-linear threshold of the problem.
For our proofs, we develop several new tools, including a variant of higher
moment energies and a Ramsey-theoretic approach for the problem.

##  1 Introduction

Erdős and Shelah [3] initiated the study of graphs with local properties. For
parameters $n,k,$ and $\ell$, they considered edge colorings of the complete
graph $K_{n}$, such that every $K_{k}$ subgraph contains at least $\ell$
colors. They defined $f(n,k,\ell)$ as the minimum number of colors that such
an edge coloring can have. For example, $f(n,3,2)$ is the minimum number of
colors that is required to color $K_{n}$, so that it does not contain a
monochromatic triangle.

The value of $f(n,k,2)$ can be thought of as an inverse of Ramsey’s theorem.
In Ramsey’s theorem, we look for the largest $n$ such that there exists a
coloring of the edges of $K_{n}$ with $c$ colors and no monochromatic $K_{k}$.
When studying $f(n,k,2)$, we are given the number of vertices $n$, and instead
look for the number of colors $c$.

By definition, $1\leq f(n,k,\ell)\leq\binom{n}{2}$. We usually consider $n$ to
be asymptotically large, while $k$ and $\ell$ are fixed constants. For
asymptotically large $n$ and a fixed $k$, the _linear threshold_ is the
smallest $\ell$ for which $f(n,k,\ell)=\Omega(n)$. This value of $\ell$ is
expressed as a function of $k$. Similarly, the _quadratic threshold_ is the
smallest $\ell$ that satisfies $f(n,k,\ell)=\Theta(n^{2})$. The _polynomial
threshold_ is the smallest $\ell$ that satisfies
$f(n,k,\ell)=\Omega(n^{\varepsilon})$ for some ${\varepsilon}>0$.

Erdős and Gyárfás [4] identified the linear and quadratic thresholds to be
$\ell=\binom{k}{2}-k+3$ and $\ell=\binom{k}{2}-\lfloor k/2\rfloor+2$,
respectively. In the same paper, they also observed that $f(n,k,k)$ is
polynomial in $n$. Conlon, Fox, Lee and Sudakov [2] proved that $f(n,k,k-1)$
is sub-polynomial in $n$, which established the polynomial threshold $\ell=k$.
Beyond these thresholds, almost tight bounds for $f(n,k,\ell)$ are known in
other regimes. Particularly, Pohoata and Sheffer [9] showed that, for any
integers $k>m\geq 2$,

$f\left(n,k,\binom{k}{2}-m\cdot\left\lfloor\frac{k}{m+1}\right\rfloor+m+1\right)=\Omega\left(n^{1+\frac{1}{m}}\right).$
(1)

Probabilistic constructions of Erdős and Gyárfás [4] show that (1) is
asymptotically tight up to sub-polynomial factors.

Zeev Dvir recently suggested an additive combinatorics variant of the local
properties problem. As stated in [4, Section 9], Erdős and Sós also studied
this problem, but did not publish their results. We define the _difference
set_ of a set $A\subset\mathbb{R}$ as

$A-A=\\{a-a^{\prime}\ :\ a,a^{\prime}\in A\ \text{ and }\ a-a^{\prime}>0\\}.$

The standard definition of a difference set does not include the condition
$a-a^{\prime}>0$. However, this less common definition makes the following
local properties problem nicer to study.

For parameters $n,k,$ and $\ell$, we consider sets $A$ of $n$ real numbers,
such that every subset $A^{\prime}\subset A$ of size $k$ satisfies that
$|A^{\prime}-A^{\prime}|\geq\ell$. Let $g(n,k,\ell)$ be the minimum size of
$\lvert A-A\rvert$, over all such sets $A$. In the current work, we study
$g(n,k,\ell)$. The trivial bounds for this problem are $n-1\leq
g(n,k,\ell)\leq\binom{n}{2}$. As before, for a fixed $k$, the quadratic
threshold is the smallest $\ell$ for which $g(n,k,\ell)=\Theta(n^{2})$. We
define the _super-linear threshold_ as the largest $\ell$ for which
$g(n,k,\ell)=O(n)$.

Previous bounds. Currently, not much is known about the behavior of
$g(n,k,\ell)$. The unpublished work of Erdős and Sós proved that
$g(n,4,5)\geq\binom{n}{2}-n+2$. We also have the bound $g(n,k,\ell)\geq
f(n,k,\ell)$, for every $n,k,$ and $\ell$. For example, the bounds of (1) also
hold after replacing $f(\cdot)$ with $g(\cdot)$. Indeed, we can construct a
complete graph with a vertex for every element of $A$. The color of an edge
corresponds to the difference of the numbers that correspond to the two
vertices. If every subset $A^{\prime}\subset A$ of size $k$ satisfies that
$|A^{\prime}-A^{\prime}|\geq\ell$, then every subgraph $K_{k}$ spans at least
$\ell$ colors. Similarly, the total number of colors is $|A-A|$.

Fish, Pohoata, and Sheffer [6] observed that Roth’s theorem implies the
following bound.

######  Theorem 1.1.

For every $\epsilon>0$, there exists $c$ that satisfies the following. For
every sufficiently large integer $k$, we have that

$g\left(n,k,c\cdot k\cdot\log^{1/4-\epsilon}k\right)=n2^{O(\sqrt{\log n})}.$

Fish, Lund, and Sheffer [5] obtained the following result by projecting a
hypercube onto a line.

######  Theorem 1.2.

For every $n>k\geq 0$ where $n$ is a power of two, we have that

$g\left(n,k,\frac{k^{\log_{2}(3)}-1}{2}\right)=O\left(n^{\log_{2}(3)}\right).$

Our results. We derive several new bounds for $g(n,k,\ell)$. First, we
identify the super-linear threshold of $g(n,k,\ell)$. Recall that
$\omega(\cdot)$ means “asymptotically strictly larger than”.

######  Theorem 1.3.

For every $k$ and sufficiently large $n$, we have that

$\displaystyle g(n,k,k-1)=n-1\qquad\text{ and }\qquad g(n,k,k)=\omega(n).$

After establishing the super-linear threshold, it is natural to ask how
quickly the bound changes as $\ell$ grows. We obtain the following bound via a
probabilistic argument.

######  Theorem 1.4.

For every $c\geq 2$ and integer $k>(c^{2}+1)^{2}$, we have that

$g(n,k,ck+1)=O\Big{(}n^{1+\frac{c^{2}+1}{k}}\Big{)}.$

When fixing $c\geq 2$, the bound of Theorem 1.4 becomes arbitrarily close to
$O(n)$ as $k$ grows. We note that the assumption $k>(c^{2}+1)^{2}$ can be
removed from the statement of this theorem. Indeed, when $k\leq(c^{2}+1)^{2}$,
the bound of the theorem is trivial.

Additive combinatorics provides many tools for studying sets that have a small
difference set. We rely on such tools to study the case of small $\ell$, in
the proofs of Theorems 1.3 and 1.4. To study sets with larger values of
$\ell$, we have to develop new tools. In particular, we obtain the following
result by studying a new variant of higher moment energies. For the definition
of higher moment energies and of our new variant, see Section 2.

######  Theorem 1.5.

Every $k\geq 8$ that is a multiple of 8 satisfies

$g\left(n,k,\frac{9k^{2}}{32}-\frac{9k}{8}+5\right)=\Omega(n^{4/3}).$

By (1), for the graphs local properties problem, we have that

$f\left(n,k,\binom{k}{2}-3\cdot\left\lfloor\frac{k}{4}\right\rfloor+4\right)=\Omega\left(n^{4/3}\right).$

This bound is tight up to subpolynomial factors. Theorem 1.5 shows that, in
the additive combinatorics variant, a much weaker local restriction leads to
$\Omega(n^{4/3})$, up to subpolynomial factors. Unlike the graph variant, in
this case the coefficient of $k^{2}$ is smaller than $1/2$.

Theorem 1.2 provides an upper bound for the local properties problem by
introducing a construction. Surprisingly, we show that the same construction
can be used to obtain a proof for a lower bound.

######  Theorem 1.6.

For every $k\geq 8$ that is a power of two and sufficiently large $n$, we have
that

$g\left(n,k,\frac{k^{\log_{2}(3)}+1}{2}\right)=\Omega\left(n^{1+\frac{2}{k-2}}\right).$

The proof of Theorem 1.6 is in some sense Ramsey theoretic: We show that a set
with many repeated differences must contain a copy of the construction from
Theorem 1.2. Such a subset contradicts the local property, and thus cannot
exist.

Finally, we mention the best bound that we managed to obtain for the quadratic
threshold.

######  Claim 1.7.

When $k$ is a multiple of two, we have that

$g\left(n,k,\frac{3k^{2}}{8}-\frac{3k}{4}+2\right)=\Omega(n^{2}).$

It is not difficult to prove Claim 1.7, and it is possible that the quadratic
threshold is much smaller. We include Claim 1.7 for completeness. That is, to
document all the current best bounds for the arithmetic variant of the local
properties problem.

Lastly, we note that while most results in this paper apply to the setting of
a general Abelian group, we decided to not pursue this direction and leave
this to future work.

Outline. In Section 2, we define our new energy variant and use it to prove
Theorem 1.5. In Section 3, we prove our other results for large values of
$\ell$: Theorem 1.6 and Claim 1.7. In Section 4, we prove our bounds for small
values of $\ell$: Theorem 1.3 and Theorem 1.4. In Section 5, we pose some
questions for future work.

Acknowledgements. We would like to thank MIT Department of Science for the
generous support. We would also like to express our gratitude towards Adam
Sheffer for his mentorship and support throughout the NYC Discrete Math REU,
as well as his invaluable help in the preparation of this paper. In addition,
we would like to thank Sara Fish for many helpful discussions as well as Ilya
Shkredov for his enlightening suggestion that led to an improvement in the
bound of Theorem 1.5. Lastly, we thank the referees for their many useful
comments and suggestions.

##  2 Dumbbell energy and Theorem 1.5

In this section, we prove Theorem 1.5. Our proof relies on a new energy
variant. Before we introduce this energy, we briefly recall the notion of
higher moment energies.

The _additive energy_ of a finite set $A\subset\mathbb{R}$ is

$E^{+}(A)=\lvert\\{(a_{1},a_{2},a_{3},a_{4})\in A^{4}\ :\
a_{1}-a_{2}=a_{3}-a_{4}\\}\rvert.$

Additive energy is a common tool in additive combinatorics. For example, it
provides the following lower bound for the size of the difference set:

$|A-A|\geq\frac{|A|^{4}}{E^{+}(A)}.$

In the past decade, several variants of additive energy led to interesting new
results. One of those variants is _higher moment energies_. For an integer
$\ell>1$, the $\ell$th moment energy of $A$ is

$E_{\ell}^{+}(A)=\lvert\\{(a_{1},\ldots,a_{2\ell})\in A^{2\ell}\ :\
a_{1}-a_{2}=a_{3}-a_{4}=\cdots=a_{2\ell-1}-a_{2\ell}\\}\rvert.$

We note that $E_{2}^{+}(A)$ is the standard additive energy $E^{+}(A)$. For
applications of higher moment energies, see for example [11, 12].

Figure 1: (a) A dumbbell. (b) An arithmetic dumbbell.

We now define a new variant of additive energy, which we call _dumbbell
energy_. We say that a quadruple $(a_{1},a_{2},a_{3},a_{4})\in\mathbb{R}$
forms a _dumbbell_ if $a_{1}<a_{2}<a_{3}<a_{4}$ and $a_{2}-a_{1}=a_{4}-a_{3}$.
See Figure 1. For distances $d,d^{\prime}>0$, we define $D(d,d^{\prime})$ as
the congruence class of all dumbbells $(a_{1},a_{2},a_{3},a_{4})$ that satisfy
$a_{2}-a_{1}=a_{4}-a_{3}=d$ and $a_{3}-a_{2}=d^{\prime}$. That is, two
dumbbells are congruent if there exists a translation of $\mathbb{R}$ that
takes one dumbbell to the other.

We can think of the $\ell$th additive energy as the number of $\ell$-tuples of
congruent intervals. Similarly, we consider an energy variant that counts
$\ell$-tuples of congruent dumbbells. We define the $\ell$th _dumbbell energy_
of $A\subset\mathbb{R}$ as

$\displaystyle E^{D}_{\ell}(A)=\Big{|}\Big{\\{}(a_{1},\ldots,a_{4\ell})\in
A^{4\ell}\ :\ $ $\displaystyle\text{ For }1\leq i\leq\ell,\text{ the
quadruples }(a_{4i-3},a_{4i-2},a_{4i-1},a_{4i})$ $\displaystyle\text{ form
}\ell\text{ distinct dumbbells from the same congruence class
}\Big{\\}}\Big{|}.$

For $d,d^{\prime}\in A-A$, we set

$r^{D}_{A}(d,d^{\prime})=|\\{(a_{1},a_{2},a_{3},a_{4})\in A^{4}\ :\
a_{2}-a_{1}=a_{4}-b_{3}=d\text{ and }a_{3}-a_{2}=d^{\prime}\\}|.$

In other words, $r^{D}_{A}(d,d^{\prime})$ is the number of dumbbells in the
congruence class $D(d,d^{\prime})$ that are spanned by $A$. We note that a
dumbbell $(a_{1},a_{2},a_{3},a_{4})$ of $D(d,d^{\prime})$ is uniquely
determined by $a_{1}$. Thus, $r^{D}_{A}(d,d^{\prime})\leq|A|$ for all
$d,d^{\prime}\in A-A$. We also note that

$E^{D}_{\ell}(A)=\sum_{d,d^{\prime}\in
A-A}\binom{r^{D}_{A}(d,d^{\prime})}{\ell}.$

For a difference $d\in A-A$, we set

$r^{-}_{A}(d)=|\\{(a,a^{\prime})\in A^{2}\ :\ a-a^{\prime}=d\\}|.$

In other words, $r^{-}_{A}(d)$ is the number of representations that the
difference $d$ has in $A$.

The following lemma states a connection between the $\ell$th dumbbell energy
$E^{D}_{\ell}(A)$ and the size of the difference set $|A-A|$.

######  Lemma 2.1.

The following holds for every even constant $\ell\geq 2$. Every set $A$ of $n$
reals satisfies that $|A-A|=\Omega\left(n^{4/3}\right)$ or that

$E^{D}_{\ell}(A)=\Omega\left(\frac{n^{4\ell}}{|A-A|^{3\ell-2}}\right).$

###### Proof.

As a first step, we will prove that

$\sum_{d,d^{\prime}\in
A-A}r^{D}_{A}(d,d^{\prime})^{2}=\Omega\left(\frac{n^{8}}{|A-A|^{4}}\right).$

Let

$\mathbf{1}_{B}(x)=\begin{cases}1&\text{if }x\in B,\\\
0&\text{otherwise},\end{cases}$

be the indicator function for a set $B\subset\mathbb{R}$. We may write

$S:=\sum_{d,d^{\prime}\in A-A}r_{A}^{D}(d,d^{\prime})=\sum_{a\in
A}\sum_{d,d^{\prime}\in
A-A}\mathbf{1}_{A\cap(A-d)}(a)\mathbf{1}_{A\cap(A-d)}(a+d^{\prime})=\sum_{a\in
A}\sum_{d\in A-A}\mathbf{1}_{A\cap(A-d)}(a)r_{A}^{-}(d).$

Note that $\sum_{d\in A-A}r_{A}^{-}(d)=\sum_{a\in A}\sum_{d\in
A-A}\mathbf{1}_{A\cap(A-d)}(a)=\binom{|A|}{2}=\binom{n}{2}$.

Consider $\mathcal{D}=\left\\{d:|r_{A}^{-}(d)|\geq
S/4\cdot\binom{n}{2}^{-1}\right\\}$. It is not difficult to see that
$\mathcal{D}$ captures a large fraction of the above sum: since

$\sum_{a\in
A}\sum_{d\not\in\mathcal{D}}\mathbf{1}_{A\cap(A-d)}(a)r_{A}^{-}(d)<\max_{d\not\in\mathcal{D}}r_{A}^{-}(d)\cdot\binom{n}{2}=\frac{S}{4},$

it follows that

$\sum_{a\in
A}\sum_{d\in\mathcal{D}}\mathbf{1}_{A\cap(A-d)}(a)r_{A}^{-}(d)\geq\frac{3S}{4}.$

We also have the following bound

$|\mathcal{D}|\cdot S/4\cdot\binom{n}{2}^{-1}\leq\sum_{d\in
A-A}r_{A}^{-}(d)=\binom{n}{2}.$

That is, $|\mathcal{D}|\leq 4/S\cdot\binom{n}{2}^{2}$.

Let $\mathcal{B}\subset(A-A)\times(A-A)\subset\mathbb{R}^{2}$ be the set which
projects onto a copy of $\mathcal{D}$ on each coordinate axes. By the symmetry
in $d,d^{\prime}$, the above inequality implies that

$\sum_{d,d^{\prime}\in\mathcal{B}}r_{A}^{D}(d,d^{\prime})\geq\frac{3S}{4}.$

Furthermore, the Loomis-Whitney inequality gives the upper bound
$|\mathcal{B}|\leq|\mathcal{D}|^{2}\leq 16/S^{2}\cdot\binom{n}{2}^{4}$.
Consequently, the Cauchy-Schwarz inequality implies that

$\frac{9S^{2}}{16}\leq\left(\sum_{d,d^{\prime}\in\mathcal{B}}r_{A}^{D}(d,d^{\prime})\right)^{2}\leq|\mathcal{B}|\sum_{d,d^{\prime}\in\mathcal{B}}r_{A}^{D}(d,d^{\prime})^{2}\leq
16/S^{2}\cdot\binom{n}{2}^{4}\sum_{d,d^{\prime}\in
A}r_{A}^{D}(d,d^{\prime})^{2}.$

Equivalently,

$\sum_{d,d^{\prime}\in
A-A}r^{D}_{A}(d,d^{\prime})^{2}\geq\frac{9S^{4}}{256\cdot\binom{n}{2}^{4}}.$
(2)

By definition, we have that

$\displaystyle S=\sum_{d,d^{\prime}\in A-A}r^{D}_{A}(d,d^{\prime})=\sum_{d\in
A-A}\binom{r^{D}_{A}(d)}{2}$ $\displaystyle=\sum_{d\in
A-A}\frac{r^{D}_{A}(d)^{2}}{2}-\sum_{d\in A-A}\frac{r^{D}_{A}(d)}{2}$
$\displaystyle=\sum_{d\in
A-A}\frac{r^{D}_{A}(d)^{2}}{2}-\frac{1}{2}\binom{n}{2}.$

Combining the above with the Cauchy-Schwarz inequality leads to

$\sum_{d,d^{\prime}\in A-A}r^{D}_{A}(d,d^{\prime})\geq\frac{(\sum_{d\in
A-A}r^{D}_{A}(d))^{2}}{2|A-A|}-\frac{1}{2}\binom{n}{2}=\binom{n}{2}^{2}/2|A-A|-\frac{1}{2}\binom{n}{2}.$

If $|A-A|=\Theta(n^{2})$ then we are done. We may thus assume that

$S=\Omega\left(\frac{n^{4}}{|A-A|}\right).$ (3)

Combining this Equation 2, we get the desired lower bound

$\sum_{d,d^{\prime}\in
A-A}r^{D}_{A}(d,d^{\prime})^{2}=\Omega\left(\frac{n^{8}}{|A-A|^{4}}\right).$

Lastly, by Hölder’s inequality and since $\ell$ is constant, we obtain that

$\displaystyle E_{\ell}^{D}(A)$ $\displaystyle=\sum_{d,d^{\prime}\in
A-A}\binom{r_{A}^{D}(d,d^{\prime})}{\ell}\geq\sum_{d,d^{\prime}\in
A-A}\left(\frac{r_{A}^{D}(d,d^{\prime})}{\ell}\right)^{\ell}\geq\frac{(\sum_{d,d^{\prime}\in
A-A}r_{A}^{D}(d,d^{\prime})^{2})^{\ell/2}}{|A-A|^{2(\ell/2-1)}\ell^{\ell}}$
$\displaystyle=\Omega\left(\frac{(n^{8}/|A-A|^{4})^{\ell/2}}{|A-A|^{\ell-2}\ell^{\ell}}\right)=\Omega\left(\frac{n^{4\ell}}{|A-A|^{3\ell-2}}\right).$

∎

We next introduce a variant of the energy graph that is defined in [6]. For a
finite $A\subset\mathbb{R}$ and $\ell$ even, we define the $\ell$th _dumbell
energy graph_ $G$ of $A$, as follows. The graph $G$ has a vertex for every
$2\ell$-tuple from $A^{2\ell}$. There is an edge between the vertices
$(a_{1},\ldots,a_{2\ell})$ and $(b_{1},\ldots,b_{2\ell})$ if the tuple
$(a_{1},\ldots,a_{2\ell},b_{1},\ldots,b_{2\ell})$ contributes to
$E^{D}_{\ell}$. Equivalently, if each vertex consists of $\ell/2$ dumbbells
and all $\ell$ dumbbells are congruent. By definition, the number of edges in
$G$ is $E_{\ell}^{D}(A)$.

We are now ready to prove Theorem 1.5. We first recall the statement of this
theorem.

Theorem 1.5. _Every $k\geq 8$ that is a multiple of 8 satisfies_

$g\left(n,k,\frac{9k^{2}}{32}-\frac{9k}{8}+5\right)=\Omega(n^{4/3}).$

###### Proof.

Let $A$ be a set of $n$ reals, such that every subset $A^{\prime}\subset A$ of
size $k$ satisfies that $|A^{\prime}-A^{\prime}|\geq\frac{5k^{2}}{16}-k+5$.
Let $G$ be the $k/4$ dumbbell energy graph of $A$. Consider three vertices
$v_{1},v_{2},v_{3}$ of $G$, such that there is an edge between $v_{1}$ and
$v_{2}$ and another edge between $v_{2}$ and $v_{3}$. Then each of the three
vertices consists of $k/8$ dumbbells, and all $3k/8$ dumbbells are congruent.
Thus, there is also an edge between $v_{1}$ and $v_{3}$. We conclude that
every connected component of $G$ is a clique.

We may discard connected components with a single vertex without changing the
number of edges. Every remaining connected component corresponds to a distinct
dumbbell congruency class. Since there are $O(|A-A|^{2})$ distinct (non-
congruent) dumbbells, the number of remaining connected components in $G$ is
$O(|A-A|^{2})$.

Assume for contradiction that $A$ spans $k/4$ disjoint congruent dumbbells.
Let $A^{\prime}\subset A$ be the set of $k$ numbers that form these $k/4$
dumbbells. At most four distinct differences are spanned by pairs of numbers
from the same dumbbell. In Figure 1(b), these distances are
$d,d^{\prime},d+d^{\prime}$, and $2d+d^{\prime}$.

Figure 2: The nine distances between the two dumbbells are
$d_{3},d_{1}+d_{3},2d_{1}+d_{3},d_{1}+d_{2}+d_{3},2d_{1}+d_{2}+d_{3},3d_{1}+d_{2}+d_{3},2d_{1}+2d_{2}+d_{3},3d_{1}+2d_{2}+d_{3},4d_{1}+2d_{2}+d_{3}$.

There are $\binom{k/4}{2}$ pairs of distinct dumbbells as described above.
Each such pair spans at most 9 distinct differences with one number from each
dumbbell. See Figure 2. We conclude that

$|A^{\prime}-A^{\prime}|\leq 4+\binom{k/4}{2}\cdot
9=\frac{9k^{2}}{32}-\frac{9k}{8}+4.$

This contradicts the assumption, so $A$ does not span $k/4$ disjoint congruent
dumbbells.

Let $S\subset A$ be a dumbbell. We wish to derive an upper bound for the
number of dumbbells $S^{\prime}$ that are congruent to $S$ but are not
disjoint to it. There are at most four choices for the element of $S$ that
also appears in $S^{\prime}$. Then, there are at most three possible positions
for this element in $S^{\prime}$. Since $S^{\prime}$ is congruent to $S$, the
other three coordinates of $S^{\prime}$ are uniquely determined. Thus, at most
12 dumbbells are congruent to $S$ and not disjoint to it.

By combining the two preceding paragraphs, we conclude that $A$ cannot span
$3k$ congruent dumbbells. For a fixed dumbbell congruence class, every vertex
in the corresponding connected component of $G$ consists of $k/8$ copies of
that dumbbell, possibly with repetitions. Since there are fewer than $3k$ such
dumbbells to choose from, this connected component consists of fewer than
$(3k)^{k/8}$ vertices. The number of edges in the connected component is
smaller than $(3k)^{k/4}$. This holds for every connected component of $G$.
Recalling that the number of remaining connected components in $G$ is at most
$|A-A|^{2}$, we conclude that the number of edges in $G$ is
$O_{k}(|A-A|^{2})$.

Since the number of edge in $G$ is $E_{k/4}^{D}(A)$, we have that
$E_{k/4}^{D}(A)=O_{k}(|A-A|^{2})$. By Lemma 2.1, we have that

$E^{D}_{k/4}(A)=\Omega\left(\frac{n^{k}}{|A-A|^{3k/4-2}}\right).$

Combining the two above bounds for $E^{D}_{k/4}(A)$ implies that
$|A-A|=\Omega(n^{4/3})$. ∎

######  Remark 2.2.

When performing the above analysis with $E_{2}^{D}(A)$ instead of
$E^{D}_{k/4}(A)$, we obtain the weaker bound $|A-A|=\Omega(n^{8/7})$ with the
same local condition.

######  Remark 2.3.

We say that an 8-tuple
$(a_{1},a_{2},a_{3},a_{4},a_{5},a_{6},a_{7},a_{8})\in\mathbb{R}^{8}$ forms a
_double dumbbell_ if $a_{1}<a_{2}<a_{3}<a_{4}<a_{5}<a_{6}<a_{7}<a_{8}$ and
$a_{2}-a_{1}=a_{4}-a_{3}=a_{6}-a_{5}=a_{8}-a_{7}$ and
$a_{3}-a_{2}=a_{7}-a_{6}$. A natural generalization of the dumbbell energy
studied above is the $\ell$th _double dumbbell energy_ , defined for
$A\subset\mathbb{R}$ as

$\displaystyle\mathcal{E}^{D}_{\ell}(A)=\Big{|}\Big{\\{}(a_{1},\ldots,a_{8\ell})\in
A^{8\ell}\ :\ $ $\displaystyle\text{ For }1\leq i\leq\ell,\text{ the
quadruples }(a_{8i-7},a_{8i-6},\ldots,,a_{8i})$ $\displaystyle\text{ form
}\ell\text{ distinct double dumbbells from the same congruence class
}\Big{\\}}\Big{|}.$

As before, two double dumbbells are congruent if there exists a translation of
$\mathbb{R}$ that takes one double dumbbell to the other.

An identical argument as that for Theorem 1.5 gives the bound

$g\left(n,k,\frac{31k^{2}}{128}-\frac{31k}{16}+9\right)=\Omega(n^{8/7})$

for every $k$ a multiple of 16. Here we have slightly weaker local condition
than that in Theorem 1.5 at the expense of a worse exponent in
$\Omega\left(n^{8/7}\right)$. We chose to present Theorem 1.5 because it is
less calculation intensive and better illustrates the main ideas of the proof.

##  3 Additional proofs for large values of $\ell$

In this section, we prove our bounds for large values of $\ell$ that are not
related to dumbbell energy. That is, we prove Theorem Theorem 1.6 and Claim
1.7.

We begin with the proof of Claim 1.7, since this simple proof is a nice warm-
up. The proof relies on the observation that $a-b=c-d$ implies $a-c=b-d$.

Recall that for a set $A$ and a difference $d\in A-A$ we set

$r^{-}_{A}(d)=|\\{(a,a^{\prime})\in A^{2}\ :\ a-a^{\prime}=d\\}|.$

Claim 1.7. _When $k$ is a multiple of two, we have that_

$g\left(n,k,\frac{3k^{2}}{8}-\frac{3k}{4}+2\right)=\Omega(n^{2}).$

###### Proof.

Let $A$ be a set of $n$ reals, such that every subset $A^{\prime}\subset A$ of
size $k$ satisfies that
$|A^{\prime}-A^{\prime}|\geq\frac{3k^{2}}{8}-\frac{3k}{4}+2$. Assume for
contradiction that there exists $d\in A-A$ for which $r_{A}^{-}(d)\geq k$.
Since every number participates in at most two representations of $d$, there
exist distinct $a_{1},\ldots,a_{k/2},b_{1},\ldots,b_{k/2}$ such that
$a_{1}-b_{1}=\cdots=a_{k/2}-b_{k/2}=d$. We set
$S=\\{a_{1},\ldots,a_{k/2},b_{1},\ldots,b_{k/2}\\}$.

We may assume, without loss of generality, that $a_{1}>a_{2}>\cdots>a_{k/2}$.
This implies that $b_{1}>b_{2}>\cdots>b_{k/2}$. For every $1\leq i<j\leq k/2$,
we have that $a_{i}-b_{i}=a_{j}-b_{j}$, which in turn implies that
$a_{i}-a_{j}=b_{i}-b_{j}$. Since there are $\binom{k/2}{2}$ such choices of
$i$ and $j$, there are $\binom{k/2}{2}$ equations of the form
$a_{i}-a_{j}=b_{i}-b_{j}$. We conclude that

$|S-S|\leq\binom{k}{2}-\left(\frac{k}{2}-1\right)-\binom{k/2}{2}=\frac{3k^{2}}{8}-\frac{3k}{4}+1.$

Since the above contradicts the assumption about $A$, we get that every $d\in
A-A$ satisfies $r_{A}^{-}(d)<k$. Since $k$ is constant, we have that

$|A-A|>\frac{1}{k}\binom{n}{2}=\Theta(n^{2}).$

∎

We now move to prove Theorem 1.6. We rely on the following configuration from
[5]. Fish, Lund and Sheffer utilize the configuration to obtain an upper bound
on $g(n,k,k^{2/3})$. We will instead use this construction to prove a lower
bound on $g(n,k,\ell)$ where $\ell=\Theta(k^{2/3})$.

For an integer $i\geq 1$ and positive reals $a,\delta_{1},\ldots,\delta_{i}$,
we define a _projected- $i$-cube_ as

$P(a,\delta_{1},\ldots,\delta_{i})=\\{a+x_{1}\delta_{1}+x_{2}\delta_{2}+\cdots+x_{i}\delta_{i}\
:\ x_{1},\ldots,x_{i}\in\\{0,1\\}\\}.$

We note that a projected-$i$-cube is a set of at most $2^{i}$ real numbers. A
projected-$i$-cube can be thought of as a projection of an $i$-dimensional
hypercube onto $\mathbb{R}$, which explains the name of this object.

For $i>1$, every projected-$i$-cube is the union of two
projected-$(i-1)$-cubes that are identical up to a translation of distance
$p_{i}$. The following lemma states another useful property of
projected-$i$-cubes.

######  Lemma 3.1.

If $A$ is a projected-$i$-cube then

$\lvert A-A\rvert\leq\frac{3^{i}-1}{2}.$

For comparison, a set $A$ of $2^{i}$ random reals is expected to satisfy
$\lvert A-A\rvert=\Theta(4^{i})$.

###### Proof.

The proof is by induction on $i$. For the induction basis, we consider the
case of $i=1$. In this case $A$ is a set of two numbers, so
$|A-A|=1=(3^{1}-1)/2$.

For the induction step, we assume that the claim holds for projected-$i$-cubes
and consider a projected-$(i+1)$-cube $A=P(a,\delta_{1},\ldots,\delta_{i+1})$.
Then $A$ is the union of the two projected-$i$-cubes
$A_{1}=P(a,\delta_{1},\ldots,\delta_{i})$ and
$A_{2}=P(a+\delta_{i+1},\delta_{1},\ldots,\delta_{i})$. These two
projected-$i$-cubes have the same difference set $D=A_{1}-A_{1}=A_{2}-A_{2}$.
The induction hypothesis implies that $|D|\leq(3^{i}-1)/2$.

Next, we note that every difference in $(A-A)\setminus\\{\delta_{i+1}\\}$ is
either formed by two numbers from $A_{1}$ or by one number from $A_{1}$ and
another from $A_{2}$. By the preceding paragraph, there are at most
$(3^{i}-1)/2$ differences of the former type. Every difference of the latter
type is in $D\pm\delta_{i+1}$. The number of such differences is at most
$2\cdot|D|=3^{i}-1$. In total,

$|A-A|\leq(3^{i}-1)/2+(3^{i}-1)+1=(3^{i+1}-1)/2.$

This completes the proof of the induction step and thus the proof of the
theorem. ∎

We define the _left endpoint_ of a projected-$i$-cube as the smallest number
of that cube. The _right endpoint_ is the largest number of the cube.

Theorem 1.6. _For every $k\geq 8$ that is a power of two and sufficiently
large $n$, we have that_

$g\left(n,k,\frac{k^{\log_{2}(3)}+1}{2}\right)=\Omega\left(n^{1+\frac{2}{k-2}}\right).$

###### Proof.

We consider a set $A\subset\mathbb{R}$ such that $|A|=n$ and $|A-A|\leq
n^{1+\frac{2}{k-2}}/9$. We show that such a set must contain a
projected-$(\log_{2}(k)-2)$-cube. Then, Lemma 3.1 implies that $A$ does not
satisfy the local property in the statement of the theorem, which completes
the proof.

For an integer $i$, we set $\eta_{i}=1-(2^{i+1}-2)/(k-2)$. We prove by
induction on $1\leq i\leq\log_{2}(k)-2$ that $A$ contains at least
$n^{\eta_{i}}$ disjoint translated copies of a projected-$i$-cube with exactly
$2^{i}$ elements. Combining this with the preceding paragraph completes the
proof of the theorem.

There are $\binom{n}{2}>n^{2}/3$ pairs of elements from $A$ and $|A-A|\leq
n^{1+\frac{2}{k-2}}/9$. By the pigeonhole principle there exists a distance
that occurs at least $3n^{(k-4)/(k-2)}$ times. We arbitrarily fix one such
distance and denote it as $d_{1}$. We set $A_{1}$ to be the set of elements of
$A$ that are at distance $d_{1}$ from another element of $A$. Let $G_{1}$ be
the graph whose vertices are the elements of $A_{1}$. Two vertices are
connected by an edge if they span the difference $d_{1}$. We note that $G_{1}$
contains at least $3n^{(k-4)/(k-2)}$ edges. Since every vertex is of degree at
most two, we can obtain a matching by repeatedly choosing an arbitrary edge
$e$ and discarding at most two other edges that share a vertex with $e$. This
implies that $G_{1}$ contains a matching of size at least $n^{(k-4)/(k-2)}$.
Since a projected-1-cube consists of two points and $\eta_{1}=(k-4)/(k-2)$, we
obtain the case of $i=1$. This completes the induction basis.

For the induction step, we fix $1\leq i<\log_{2}(k)-2$ and assume that the
claim holds for $i$. That is, $A$ contains at least $n^{\eta_{i}}$ disjoint
translated copies of a projected-$i$-cube. We note that, in this range,
$\eta_{i}>0$. We fix exactly $n^{\eta_{i}}$ translated copies and set
$A_{i+1}$ to be the set of endpoints of these. By definition, we have that
$|A_{i+1}|=2n^{\eta_{i}}$. The number of pairs of endpoints that do not belong
to the same translated copy is

$\frac{1}{2}\cdot
2n^{\eta_{i}}\cdot\left(2n^{\eta_{i}}-2\right)=2n^{2\eta_{i}}-2n^{\eta_{i}}.$

Each difference is spanned by $A_{i+1}$ fewer than $2n^{\eta_{i}}$ times.
Thus, the number of above pairs that span a difference that is also spanned by
the projected-$i$-cube is $O(n^{\eta_{i}})$. When $n$ is sufficiently large,
we may assume that the number of pairs that span a distance that is not in the
projected-$i$-cube is at least $n^{2\eta_{i}}$. Since $A_{i+1}\subset A$ and
$|A-A|\leq n^{1+\frac{2}{k-2}}/9$, there exists a difference that is spanned
by at least

$9n^{2\eta_{i}-1-2/(k-2)}=9n^{\eta_{i+1}}$

of these pairs. We fix such a difference and denote it as $d_{i+1}$. In each
of the corresponding pairs, the difference $d_{i+1}$ occurs between the two
left endpoints, between the two right endpoints, or between one right endpoint
and one left endpoint. By the pigeonhole principle, at least one third of the
pairs are of the same type. Thus, $A_{i+1}$ contains at least
$3n^{\eta_{i+1}}$ translatd copies of the same projected-$(i+1)$-cube.

The above translated copies of a projected-$(i+1)$-cube might not be disjoint.
In particular, a projected projected-$i$-cube from $A_{i}$ might participate
in two projected-$(i+1)$-cubes. By repeating the matching argument from the
induction basis, we obtain that at least one third of the
projected-$(i+1)$-cubes are disjoint. That is $A_{i+1}$ contains at least
$n^{\eta_{i+1}}$ disjoint translated copies of the same
projected-$(i+1)$-cube. This concludes the proof of the induction step and
thus the proof of the theorem. ∎

##  4 Small values of $\ell$

In this section, we prove our bounds for small values of $\ell$: Theorem 1.3
and Theorem 1.4. We first briefly go over the tools that we require from
additive combinatorics.

Tools from additive combinatorics. Szemerédi’s theorem states that every
sufficiently large subset of $\\{1,2,\ldots,n\\}$ contains a long arithmetic
progression. We rely on the following variant of this result, due to Gowers
[7].

######  Theorem 4.1.

For every $k$, there exists $c>0$ that satisfies the following. Every set of
$n/(\log\log n)^{c}$ numbers from $\\{1,2,\ldots,n\\}$ contains a $k$-term
arithmetic progression. Moreover, $c$ can be taken to be $2^{-2^{k+9}}$.

A _generalized arithmetic progression of dimension_ $d$ is defined as

$\Big{\\{}a+\sum_{j=1}^{d}k_{j}b_{j}\ :\
a,b_{1},\ldots,b_{d}\in\mathbb{R}\text{ and with integer }0\leq k_{j}\leq
n_{j}-1\text{ for every }1\leq j\leq d\Big{\\}}.$ (4)

The size of a generalized arithmetic progression is the number of elements in
it. We note that an arithmetic progression is a generalized arithmetic
progression of dimension one.

One of the most common tools for studying sets with a small different set is
_Freiman’s theorem._ The following is a variant of this theorem over the
reals. For example, see Sanders [10, Theorem 1.3].

######  Theorem 4.2.

For every sufficiently large finite set $A\subset\mathbb{R}$ and sufficiently
large $d>0$, if $|A-A|\leq d|A|$ then $A$ is contained in a generalized
arithmetic progression of dimension at most $d\cdot\log^{4}d$ and size at most
$|A|\cdot e^{d\cdot\log^{4}d}$.

Similarly to a difference set $A-A$, we define the _sum set_ of a set
$A\subset\mathbb{R}$ as

$A+A=\\{a+a^{\prime}\ :\ a,a\in A\\}.$

The following _Plünnecke-Ruzsa estimate_ (for example, see [13, Corollary
6.29]) shows one connection between $A+A$ and $A-A$.

######  Lemma 4.3.

If a finite $A\subset\mathbb{R}$ satisfies $|A-A|\leq c|A|$ then

$|A+A|\leq c^{2}|A|.$

The following is a special case of a result of Green and Morris [8] about sum
sets.

######  Theorem 4.4.

For every $c>0$, every sufficiently large $m$ satisfies the following. For
every integer $n$, the number of subsets $A\subset\\{1,2,\ldots,n\\}$ that
satisfy $|A|=m$ and $|A+A|\leq c|A|$ is at most

$2^{m}\cdot n^{c+1}\cdot\binom{cm/2}{m}.$

Our proofs. We now derive the super-linear threshold for our local properties
problem. We first recall the statement of this result.

Theorem 1.3. _For every $k$ and sufficiently large $n$, we have that_

$\displaystyle g(n,k,k-1)=n-1\qquad\text{ and }\qquad g(n,k,k)=\omega(n).$

###### Proof.

To see that $g(n,k,k-1)=n-1$, we set $A=\\{1,2,\ldots,n\\}$ and note that
$|A-A|=n-1$. The local property trivially holds, since every $k$ numbers span
at least $k-1$ differences. It remains to prove that $g(n,k,k)=\omega(n)$.

For a constant $c>0$, we consider a set $A$ such that $|A|=n$ and $|A-A|\leq
cn$. By Theorem 4.2, the set $A$ is contained in a generalized arithmetic
progression $G$ of size at most $Cn$ and dimension at most $D$. The constants
$C$ and $D$ depend on $c$ but not on $n$. We define $G$ as in (4). Without
loss of generality, we may assume that $n_{1}\geq n^{1/D}$.

We may think of $G$ as the union of disjoint arithmetic progressions with step
$b_{1}$, each of size at least $n_{1}\geq n^{1/D}$. Since $|A|/|G|\geq 1/C$,
there exists such an arithmetic progression $S$ such that $|A\cap S|/|S|\geq
1/C$. We translate and scale $\mathbb{R}$ such that $S$ becomes
$\\{1,2,3,...,|S|\\}$. Then, $A$ contains at least $|S|/C$ elements of
$\\{1,2,3,...,|S|\\}$. Theorem 4.1 implies that $A$ contains a $k$-term
arithmetic progression.

We proved that the following holds for every constant $c>0$, when $n$ is
sufficiently large: Every set $A$ of $n$ reals that satisfies $|A-A|\leq cn$
contains $k$ numbers that span $k-1$ differences. Thus, a set that satisfies
the local restrictions of $g(n,k,\ell)$ also satisfies that $|A-A|>cn$ for
every $c$. ∎

######  Remark 4.5.

Quantitatively, the proof above gives the bound $g(n,k,k)\leq
n\cdot\sqrt{\log(\log\log n)^{c}}$, where $c=2^{-2^{k+9}}$.

For our probabilistic arguments, we recall the following Chernoff bounds (for
example, see [1, Corollary A.1.14]).

######  Theorem 4.6.

For every ${\varepsilon}>0$, there exists $c_{\varepsilon}$ that satisfies the
following. Let $Y$ be a sum of independent indicator random variables and let
$\mu$ be the expected value of $Y$. Then

$\Pr[|Y-\mu|>{\varepsilon}\mu]<2e^{-e_{\varepsilon}\mu}.$

We may set

$c_{\varepsilon}=\min\\{\ln(e^{-{\varepsilon}}(1+{\varepsilon})^{1+{\varepsilon}}),{\varepsilon}^{2}/2\\}.$

We now prove our upper bound for small values of $\ell$. We first recall the
statement of this result.

Theorem 1.4. _For every $c\geq 2$ and integer $k>(c^{2}+1)^{2}$, we have that_

$g(n,k,ck+1)=O\Big{(}n^{1+\frac{c^{2}+1}{k}}\Big{)}.$

###### Proof.

Let $N$ be a sufficiently large constant multiple of $n$, which is determined
below. We define the probability $p=3N^{-(c^{2}+1)/k}$ and set
$M=\big{\\{}1,2,\ldots,N^{1+(c^{2}+1)/k}\big{\\}}$. Let $A^{\prime}$ be a set
that is obtained by selecting each element of $M$ independently with
probability $p$. The expected size of $A^{\prime}$ is

$p\cdot N^{1+(c^{2}+1)/k}=3N.$

By applying Theorem 4.6 with $\mu=3N$ and ${\varepsilon}=1/2$, we obtain that

$\Pr\left[\frac{3N}{2}\leq\lvert A\rvert\leq\frac{9N}{2}\right]>1-2e^{-N/4}.$
(5)

By Theorem 4.4, the number of subsets $B\subset M$ that satisfy $|B|=k$ and
$|B+B|\leq c^{2}k$ is at most

$2^{k}\cdot(N^{1+(c^{2}+1)/k})^{c^{2}+1}\cdot\binom{c^{2}k/2}{k}=O_{c,k}(N^{c^{2}+1+(c^{2}+1)^{2}/k}).$

By the contrapositive of Lemma 4.3, the number of subsets $B\subset M$ that
satisfy $|B|=k$ and $|B-B|\leq ck$ is $O_{c,k}(N^{c^{2}+1+(c^{2}+1)^{2}/k})$.
We refer to such a set as a _set with small doubling_.

The probability that a fixed set with small doubling is in $A$ is $p^{k}$.
Thus, the expected number of sets with small doubling in $A$ is

$p^{k}\cdot
O_{c,k}(N^{c^{2}+1+(c^{2}+1)^{2}/k})=O_{c,k}(N^{(c^{2}+1)^{2}/k}).$

By the assumption $k>(c^{2}+1)^{2}$, the expected number of sets with small
doubling in $A$ is $o_{c,k}(N)$. Combining this with (5) implies that, with
positive probability, we have that $\frac{3N}{2}\leq\lvert
A\rvert\leq\frac{9N}{2}$ and that the number of sets with small doubling is
$o_{c,k}(N)$. Thus, there exists $A$ that satisfies both of these properties.
We fix such a set $A$ and arbitrarily remove one number from each of the
remaining sets with small doubling. This leads to $|A|=\Theta(N)$ and no sets
with small doubling in $A$. In other words, every $k$ elements from $A$ span
at least $ck+1$ distinct differences.

Since $A\subset M$, we have that $|A-A|<N^{1+(c^{2}+1)/k}$. By taking $N$ to
be a sufficiently large constant mulitple of $n$, we obtain that $|A|\geq n$.
We arbitrarily remove elements from $A$ until $|A|=n$. This leads to the
assertion of the theorem. ∎

##  5 Future work

We are still far from understanding the behavior of $g(n,k,\ell)$ an have more
questions than answers. One main open problem is to identify the quadratic
threshold of $g(n,k,\ell)$. Since this turned out to be challenging, we
suggest the following problem as a step towards the quadratic threshold.

######  Question 5.1.

For what values of $\ell$ can we prove a bound of the form
$g(n,k,\ell)=\Omega(n^{c})$ for some $4/3<c<2$?

New ideas would be needed for this problem: as mentioned in Remark 2.3, though
the idea of dumbbell energies can be generalized to “higher” dumbbell
energies, the bounds obtained that way would be of the form
$g(n,k,\ell)=\Omega(n^{c})$ for some $c<4/3$.

In terms of quadratic lower bounds, we pose the following question.

######  Question 5.2.

Is it true that when $k$ is a multiple of four, we have that

$g\left(n,k,\frac{k^{2}}{4}\right)=\Omega(n^{2})?$

There is also a natural generalization of the construction of the
projected-$(i+1)$-cube, where instead of projecting an $i$-dimensional Boolean
hypercube onto $\mathbb{R}$, we could instead project an $i$-dimensional
$b$-ary hypercube onto $\mathbb{R}$. Specifically, let
$A_{1}=\\{1,2,\ldots,b\\}$ and $D=\\{0,1,\ldots,b-1\\}$. For every $i>1$, we
let $s_{i}=4b\cdot\max\\{A_{i-1}-A_{i-1}\\}$ and $T_{i}=s_{i}\cdot D$. We then
set

$A_{i}=T_{i}+A_{i-1}.$

We note that $1\in A_{i}$ for every $i\geq 1$. This implies that $s_{i}\geq
4b(\max\\{A_{i}\\}-1)$. Since the nonzero elements of $T_{i}$ are
significantly larger than the elements of $A_{i}$, we get that
$|A_{i}|=b\cdot|A_{i-1}|$. Since $|A_{1}|=b$, we conclude that $|A_{i}|=b^{i}$
for every $i\geq 1$.

By definition, every element of $A_{i}-A_{i}$ can be represented as $x+y$
where $x\in T_{i}-T_{i}$ and $y\in A_{i-1}-A_{i-1}$. By our choice of $s_{i}$,
we have that $x,x^{\prime}\in T_{i}-T_{i}$ and $y,y^{\prime}\in
A_{i-1}-A_{i-1}$ satisfy that $x+y=x^{\prime}+y^{\prime}$ if and only if
$(x,y)=(x^{\prime},y^{\prime})$. Indeed, if $x\neq x^{\prime}$ then $\lvert
x-x^{\prime}\rvert\geq 4b\max\\{|y|,|y^{\prime}|\\}\geq 2b\lvert
y-y^{\prime}\rvert$. In particular, it can be easily checked that as a
consequence we have $\lvert A_{i}-A_{i}\rvert=\frac{(2b-1)^{i}-1}{2}$. We
conjecture that the natural generalization of [5] should hold in this case.

######  Conjecture 5.3.

When $k$ is a power of $b$,
$g\left(n,k,\frac{k^{\log_{b}(2b-1)}+1}{2}\right)=O\left(k^{\log_{b}(2b-1)}\right)$.

In the same flavor as Theorem 1.6, we may ask the following question.

######  Question 5.4.

Can we prove a lower bound for
$g\left(n,k,\frac{k^{\log_{b}(2b-1)}+1}{2}\right)$ when $k$ is a power of $b$?

## References

  * [1] Noga Alon and Joel H Spencer.  The probabilistic method.  John Wiley & Sons, 2004.
  * [2] David Conlon, Jacob Fox, Choongbum Lee, and Benny Sudakov.  The Erdős–Gyárfás problem on generalized Ramsey numbers.  Proceedings of the London Mathematical Society, 110(1):1–18, 2015\.
  * [3] Paul Erdos.  Problems and results on finite and infinite graphs.  In Recent advances in graph theory (Proc. Second Czechoslovak Sympos., Prague, 1974), pages 183–192, 1975.
  * [4] Paul Erdős and András Gyárfás.  A variant of the classical ramsey problem.  Combinatorica, 17(4):459–467, 1997.
  * [5] Sara Fish, Ben Lund, and Adam Sheffer.  A construction for difference sets with local properties.  European Journal of Combinatorics, 79:237–243, 2019.
  * [6] Sara Fish, Cosmin Pohoata, and Adam Sheffer.  Local properties via color energy graphs and forbidden configurations.  SIAM Journal on Discrete Mathematics, 34(1):177–187, 2020.
  * [7] William Timothy Gowers.  A new proof of Szemerédi’s theorem.  Geometric & Functional Analysis GAFA, 11(3):465–588, 2001.
  * [8] Ben Green and Robert Morris.  Counting sets with small sumset and applications.  Combinatorica, 36(2):129–159, 2016.
  * [9] Cosmin Pohoata and Adam Sheffer.  Local properties in colored graphs, distinct distances, and difference sets.  Combinatorica, 39(3):705–714, 2019.
  * [10] Tom Sanders.  The structure theory of set addition revisited.  Bull. Amer. Math. Soc. (N.S.), 50(1):93–127, 2013.
  * [11] Tomasz Schoen.  New bounds in Balog-Szemerédi-Gowers theorem.  Combinatorica, 35(6):695–701, 2015.
  * [12] Tomasz Schoen and Ilya D Shkredov.  Higher moments of convolutions.  Journal of Number Theory, 133(5):1693–1737, 2013.
  * [13] Terence Tao and Van H Vu.  Additive combinatorics, volume 105.  Cambridge University Press, 2006.


# Termination Analysis of Programs with Multiphase Control-Flow††thanks: This
paper is a summary of the corresponding invited talk of the second author
given at HCVS 2021, and is based on the PhD thesis of the first author [15]
and on collaborations with Amir M. Ben-Amram [9, 5] and John P. Gallagher
[16]. This work was funded partially by the Spanish MCIU, AEI and FEDER (EU)
project RTI2018-094403-B-C31, by the CM project S2018/TCS-4314 co-funded by
EIE Funds of the European Union, and by the UCM CT42/18-CT43/18 grant.

Jesús J. Domenech1 Samir Genaim1,2
1 Universidad Complutense de Madrid, Spain2 Instituto de Tecnología del
Conocimiento, Madrid, Spain<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Programs with multiphase control-flow are programs where the execution passes
through several (possibly implicit) phases. Proving termination of such
programs (or inferring corresponding runtime bounds) is often challenging
since it requires reasoning on these phases separately. In this paper we
discuss techniques for proving termination of such programs, in particular:
(1) using multiphase ranking functions, where we will discuss theoretical
aspects of such ranking functions for several kinds of program
representations; and (2) using control-flow refinement, in particular partial
evaluation of Constrained Horn Clauses, to simplify the control-flow allowing,
among other things, to prove termination with simpler ranking functions.

##  1 Introduction

Proving that a program will eventually terminate, i.e., that it does not go
into an infinite loop, is one of the most fundamental tasks of program
verification, and has been the subject of voluminous research. Perhaps the
best known, and often used, technique for proving termination is that of
_ranking functions_ , which has already been used by Alan Turing in his early
work on program verification [34]. This consists of finding a function $\rho$
that maps program states into the elements of a well-founded ordered set, such
that $\rho(s)\succ\rho(s^{\prime})$ holds for any consecutive states $s$ and
$s^{\prime}$. This implies termination since infinite descent is impossible in
a well-founded order. Besides proving termination, Turing [34] mentions that
ranking functions can be used to bound the length computations as well. This
is useful in applications such as cost analysis and loop optimisation [17, 4,
2, 12].

Unlike termination of programs in general, which is undecidable, the
algorithmic problems of detection (deciding the existence) or generation
(synthesis) of a ranking function can well be solvable, given certain choices
of the program representation, and the class of ranking functions. There is a
considerable amount of research in this direction, in which different kinds of
ranking functions for different kinds of program representations were
considered. In some cases, the algorithmic problems have been completely
settled, and efficient algorithms provided, while other cases remain open.

A common program representation in this context is _Single-path Linear-
Constraint_ (SLC) loops, where a state is described by the values of numerical
variables, and the effect of a transition (one iteration) is described by a
conjunction of _linear constraints_. Here is an example of this loop
representation; primed variables $x^{\prime}$ and $y^{\prime}$ refer to the
state following the transition:

$while\leavevmode\nobreak\ (x\leq y)\leavevmode\nobreak\
do\leavevmode\nobreak\ x^{\prime}=x+1,\,y^{\prime}\leq y$ (1)

Note that $x^{\prime}=x+1$ is an equation, not an assignment. The description
of a loop may involve linear inequalities rather than equations, such as
$y^{\prime}\leq y$ above, and consequently, be non-deterministic. Note that
for a SLC loop with $n$ variables, a transition can be seen as a point
$\bigl{(}\begin{smallmatrix}{\mathbf{x}}\hfill\\\
{\mathbf{x}^{\prime}}\hfill\end{smallmatrix}\bigr{)}\in\mathbb{Q}^{2n}$, where
its first $n$ components correspond to $\mathbf{x}$ and its last $n$
components to $\mathbf{x}^{\prime}$. We denote the set of all transitions by
${\mathcal{Q}}$, which is a polyhedron.

A more general program representation is _Transition Systems_ (TSs), which are
defined by _Control-Flow Graphs_ (CFGs) with numerical variables, consisting
of nodes representing program locations and edges annotated with linear
constraints (polyhedra) describing how values of variables change when moving
from one location to another. Figure 1 includes a program and its
corresponding TS ${\cal T}$ to its right. Primed variables in the linear
constraints refer to the state following the transition, exactly as in the
case of SLC loops.

In both program representations mentioned above, the domain of variables is
also important as it typically affects the complexity of the underlying
decision and synthesis problems. Although these program representations allow
only numerical variables and linear constraints, data structures can be
handled using _size abstractions_ , e.g., length of lists, depth of trees,
etc. [27, 24, 13, 33, 28, 20]. In such case, variables represent sizes of
corresponding data structures.

⬇

1void phases1(int x, int y, int z) {

2 while( x >= 1 ){

3 if ( y <= z - 1 ) {

4 y = y + 1;

5 } else {

6 x = x - 1;

7 }

8 }

9}

$\mathtt{n_{\\_}0}$

$\mathtt{n_{\\_}1}$

$\mathtt{n_{\\_}2}$

$\mathtt{n_{\\_}3}$

${\cal T}$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}0$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}1$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}2$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}3$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}4$

$\mathtt{n_{\\_}0}$

$\mathtt{n_{\\_}1^{3}}$

$\mathtt{n_{\\_}3^{2}}$

$\mathtt{n_{\\_}2^{2}}$

$\mathtt{n_{\\_}1^{2}}$

${\cal T}_{\\_}{pe}$

$\mathtt{n_{\\_}2^{1}}$

$\mathtt{n_{\\_}3^{1}}$

$\mathtt{n_{\\_}1^{1}}$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}0$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}1$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}2$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}6$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}5$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}7$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}8$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}{6}$

$\scriptscriptstyle{\mathcal{Q}}_{\\_}{1}$

$\begin{array}[]{r@{}llllll}{\mathcal{Q}}_{\\_}0\equiv&\\{&&x^{\prime}=x,&y^{\prime}=y,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}1\equiv&\\{x\geq
1,&&x^{\prime}=x,&y^{\prime}=y,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}2\equiv&\\{x\leq
0,&&x^{\prime}=x,&y^{\prime}=y,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}3\equiv&\\{y\leq
z-1,&&x^{\prime}=x,&y^{\prime}=y+1,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}4\equiv&\\{y\geq
z,&&x^{\prime}=x-1,&y^{\prime}=y,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}5\equiv&\\{x\geq 1,&y\leq
z-1,&x^{\prime}=x,&y^{\prime}=y+1,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}6\equiv&\\{x\geq 1,&y\geq
z,&x^{\prime}=x-1,&y^{\prime}=y,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}7\equiv&\\{x\geq 1,&y\geq
z,&x^{\prime}=x,&y^{\prime}=y,&z^{\prime}=z&\\}\\\
{\mathcal{Q}}_{\\_}8\equiv&\\{x\leq 0,&y\geq
z,&x^{\prime}=x,&y^{\prime}=y,&z^{\prime}=z&\\}\\\ \end{array}$

Figure 1: A loop with $2$ phases, it corresponding TS ${\cal T}$, and the TS
${\cal T}_{\\_}{pe}$ after applying CFR.

Due to practical considerations, termination analysis tools typically focus on
classes of ranking functions that can be synthesised efficiently. This,
however, does not mean that theoretical aspects of such classes are put aside,
as understanding theoretical limits and properties of the underlying problems
is necessary for developing practical algorithms. The most popular class of
ranking functions in this context is probably that of _Linear Ranking
Functions_ (LRFs). A LRF is a function
$\rho(x_{\\_}1,\dots,x_{\\_}n)=a_{\\_}1x_{\\_}1+\dots+a_{\\_}nx_{\\_}n+a_{\\_}0$
such that any transition from $\mathbf{x}$ to $\mathbf{x}^{\prime}$ satisfies
(i) $\rho(\mathbf{x})\geq 0$; and  (ii)
$\rho(\mathbf{x})-\rho(\mathbf{x}^{\prime})\geq 1$.  For example,
$\rho(x,y)=y-x$ is a LRF for Loop (1). Several polynomial-time algorithms to
find a LRF using linear programming exist [4, 14, 17, 29, 30, 32]. These
algorithms are complete111Complete means that if there is a LRF, they will
find one. for TSs with rational-valued variables, but not with integer-valued
variables. Ben-Amram and Genaim [6] showed how completeness for the integer
case can be achieved, and also classified the corresponding decision problem
as co-NP complete.

Despite their popularity, LRFs do not suffice for all programs, and a natural
question is what to do when a LRF does not exist; and a natural answer is to
try a richer class of ranking functions. Of particular importance is the class
of _Lexicographic-Linear Ranking Functions_ (LLRFs). These are tuples of
linear functions that decrease lexicographically over a corresponding well-
founded ordered set. For example, the program depicted in Figure 1 does not
have a LRF, but it has the LLRF $\langle z-y,x\rangle$ since: for the _then_
branch $z-y$ decreases and for the _else_ branch $x$ decreases while $z-y$
does not change. LLRFs might be necessary even for SLC loops. For example, the
following SLC loop

$while\leavevmode\nobreak\ (x\geq 0)\leavevmode\nobreak\
do\leavevmode\nobreak\ x^{\prime}=x+y,\,y^{\prime}=y+z,z^{\prime}=z-1$ (2)

does not have a LRF, but can be proved terminating using the LLRF $\langle
z,y,x\rangle$.

There are several definitions for LLRFs in the literature [4, 7, 11, 23] and
they have different power, i.e., some can prove termination of a program while
others fail. They have corresponding polynomial-time synthesis algorithms for
the case of rational variables, and the underlying decision problems are co-NP
complete for the case of integer variables [7, 8]. The definition of Larraz et
al. [23] is the most general in this spectrum of LLRFs, its complexity
classification is not known yet and corresponding complete synthesis
algorithms do not exist.

The LLRF $\langle z,y,x\rangle$ used above for Loop (2) belongs to a class of
LLRFs that is know as _Multiphase-Linear Ranking Functions_ (M$\Phi$RFs).
Ranking functions in this class are characterised by the following behaviour:
the first component _always_ decreases, and when it becomes negative the
second component starts to decrease (and will keep decreasing during the rest
of the execution), and when it becomes negative the third component starts to
decrease, and so on. This behaviour defines phases through which executions
pass. This is different from LLRFs in general since once a component becomes
negative it cannot be used anymore. Also the LLRF $\langle z-y,x\rangle$ for
the program of Figure 1 induces a similar multiphase behaviour, since once
$z-y$ becomes negative it cannot be used anymore. However, it is not a
M$\Phi$RF since $z-y$ stops decreasing once we move to the second phase.

In the rest of this paper we overview works on termination analysis of
multiphase programs, in particular: in Section 2 we discuss techniques for
proving termination using M$\Phi$RFs; and in Section 3 we discuss techniques
for proving termination using _Control-Flow Refinement_ (CFR). Section 4 ends
the paper with some concluding remarks and discusses further research
directions.

##  2 Termination analysis using multiphase ranking functions

A M$\Phi$RF is a tuple $\langle\rho_{\\_}1,\ldots,\rho_{\\_}d\rangle$ of
linear functions that define phases of the program that are linearly ranked,
where $d$ is the _depth_ of the M$\Phi$RF, intuitively the number of phases.
The decision problem _Existence of a M $\Phi$RF_ asks to determine whether a
program has a M$\Phi$RF. The _bounded_ decision problem restricts the search
to M$\Phi$RFs of depth $d$, where $d$ is part of the input.

For the case of SLC loops, the complexity and algorithmic aspects of the
bounded version of the M$\Phi$RF problem were settled by Ben-Amram and Genaim
[9]. The decision problem is $\mathtt{PTIME}$ for SLC loops with rational-
valued variables, and $\mathtt{coNP}$-complete for SLC loops with integer-
valued variables; synthesising M$\Phi$RFs, when they exist, can be performed
in polynomial and exponential time, respectively. We note that the proof of
the rational case is done by showing that M$\Phi$RFs and _nested_ ranking
functions [25] (a strict subclass of M$\Phi$RFs for which a polynomial-time
algorithm exists) have the same power for SLC loops. Besides, they show that
for SLC loops M$\Phi$RFs have the same power as general lexicographic-linear
ranking functions, and that M$\Phi$RFs induce linear iteration bounds. The
problem of deciding if a given SLC loop admits a M$\Phi$RF, without a given
bound on the depth, is still open.

In practice, termination analysis tools search for M$\Phi$RFs incrementally,
starting by depth $1$ and increase the depth until they find one, or reach a
predefined limit, after which the returned answer is _don’t know_. Finding a
theoretical upper-bound on the depth of a M$\Phi$RF, given the loop, would
also settle this problem, however, as shown by Ben-Amram and Genaim [9] such
bound must depend not only on the number of constraints or variables, as for
other classes of LLRFs [4, 7, 11], but also on the coefficients used in the
corresponding constraints. Yuan et al. [35] proposed an incomplete method to
bound the depth of M$\Phi$RFs for SLC loops.

Ben-Amram et al. [5] have done a significant progress towards solving the
problem of _existence of a M $\Phi$RF_ for SLC loop, i.e., seeking a M$\Phi$RF
without a given bound on the depth. In particular, they present an algorithm
for seeking M$\Phi$RFs that reveals novel insights on the structure of these
ranking functions. In a nutshell, the algorithm starts from the set of
transitions of the given SLC loop, which is a polyhedron, and iteratively
removes transitions $\bigl{(}\begin{smallmatrix}{\mathbf{x}}\hfill\\\
{\mathbf{x}^{\prime}}\hfill\end{smallmatrix}\bigr{)}$ such that
$\rho(\mathbf{x})-\rho(\mathbf{x}^{\prime})>0$ for some function
$\rho(\mathbf{x})=\vec{a}\cdot\mathbf{x}+b$ that is _non-negative on all
enabled states_. The process continues iteratively, since after removing some
transitions, more functions $\rho$ may satisfy the non-negativity condition,
and they may eliminate additional transitions in the next iteration. When all
transitions are eliminated in a finite number of iterations, one can construct
a M$\Phi$RF using the $\rho$ functions; and when reaching a situation in which
no transition can be eliminated, the remaining set of transitions, which is a
polyhedron, is actually a recurrent set that witnesses non-termination. The
algorithm always finds a M$\Phi$RF if one exists, and in many cases, it finds
a recurrent set when the loop is non-terminating, however, it is not a
decision procedure as it diverges in some cases. Nonetheless, the algorithm
provides important insights into the structure of M$\Phi$RFs. Apart from
revealing a relation between seeking M$\Phi$RFs and seeking recurrent sets,
these insights are useful for finding classes of SLC loops for which, when
terminating, there is always a M$\Phi$RF and thus have linear run-time bound.
This result was proven for two kinds of SLC loops, both considered in previous
work, namely _octagonal relations_ and _affine relations with the finite-
monoid property_ – for both classes, termination has been proven decidable
[22].

Ben-Amram et al. [5] have also suggested a new representation for SLC loops,
called the _displacement_ representation, that provides new tools for studying
termination of SLC loops in general, and the existence of a M$\Phi$RF in
particular. In this representation, a transition
$\bigl{(}\begin{smallmatrix}{\mathbf{x}}\hfill\\\
{\mathbf{x}^{\prime}}\hfill\end{smallmatrix}\bigr{)}$ is represented as
$\bigl{(}\begin{smallmatrix}{\mathbf{x}}\hfill\\\
{\mathbf{y}}\hfill\end{smallmatrix}\bigr{)}$ where
$\mathbf{y}=\mathbf{x}^{\prime}-\mathbf{x}$. Using this representation the
algorithm described above can be formalised in a simple way that avoids
computing the $\rho$ functions mentioned above, and reduces the existence of a
M$\Phi$RF of depth $d$ to unsatisfiability of a certain linear constraint
system. Moreover, any satisfying assignment for this linear constraint system
is a witness that explains why the loop has no M$\Phi$RF of depth $d$. As an
evidence on the usefulness of this representation in general, they showed that
some non-trivial observations on termination of bounded SLC loops (i.e., the
set of transitions is a bounded polyhedron) are made straightforward in this
representation, while they are not easy to see in the normal representation,
in particular: a bounded SLC loop terminates if and only if it has a LRF, and
it does not terminate if and only if it has a fixpoint transition
$\bigl{(}\begin{smallmatrix}{\mathbf{x}}\hfill\\\
{\mathbf{x}}\hfill\end{smallmatrix}\bigr{)}$.

The works discussed above are limited to the case of SLC loops. The case of
general TSs has been considered by Leike and Heizmann [25] and Li et al. [26],
where both translate the existence of a M$\Phi$RF of a given depth $d$ to
solving a corresponding non-linear constraint problem, which is complete for
the case of rational variables. However, while complete, these approaches do
not provide any insights on the complexity of the underlying decision
problems. The technique of Borralleras et al. [10] can be used to infer, among
other things, M$\Phi$RFs for TSs without a given bound on the depth. It is
based on solving corresponding safety problems using Max-SMT, and it is not
complete.

##  3 Termination analysis using control-flow refinement

As we have seen in Section 1, there are TSs with multiphase behaviour that do
not admit M$\Phi$RFs, but rather a different notion of LLRF that does not
require the components to keep decreasing after turning negative. To prove
termination of such TSs one can use other classes of LLRFs [4, 7, 11, 23],
however, this might not be enough due to complex control-flow where abstract
properties of several implicit execution paths are merged. To overcome this
imprecision, not only for termination but for program analysis in general, one
approach is to simplify the control-flow in order to make implicit execution
paths explicit, and thus makes it possible to infer the desired properties
with a weaker version of the analysis. This is known as _Control-Flow
Refinement_ (CFR).

Let us see how CFR can simplify the kind of ranking functions needed to proved
termination, and thus improve the precision of the underlying termination
analyser. Consider the program depicted Figure 1 again, and recall that we
failed to prove its termination when using only LRFs. Examining this program
carefully, we can see that any execution passes in two phases: in the first
one, $\mathtt{y}$ is incremented until it reaches the value of $\mathtt{z}$,
and in the second phase $\mathtt{x}$ is decremented until it reaches
$\mathtt{0}$. Lets us transform the program into a semantically equivalent one
such that the two phases are separate and explicit:

⬇

1 while (x >= 0 and y <= z-1) y = y + 1;

2 while (x >= 0 and y >= z) x = x - 1;

Now we can prove termination of this program using LRFs only: for the first
loop $z-y$ is a LRF, and for the second loop $x$ is a LRF. Moreover, cost
analysis tools that are based on bounding loop iterations using LRFs [2] would
infer a linear bound for this program while they would fail on the original
one.

Apart from simplifying the termination proof, there are also cases where it is
not possible to prove termination without such transformations even when using
LLRFs. In addition, CFR can help in inferring more precise invariants, without
the need for expensive disjunctive abstract domains, which can benefit any
analysis that uses such invariants, e.g., termination and cost analysis.

CFR has been considered by Gulwani et al. [21] and Flores-Montoya and Hähnle
[18] to improve the precision of cost analysis, and by Sharma et al. [31] to
improve the precision of invariants in order to prove program assertions.
While all these techniques can automatically obtain the transformed program
above, they are developed from scratch and tailored to some analysis of
interest. Recently, CFR has also been considered by Albert et al. [3] to
improve cost analysis as well, but from a different perspective that uses
termination witnesses to guide CFR.

Since CFR is, in principle, a program transformation that specialises programs
to distinguish different execution scenarios, Domenech et al. [16] explored
the use of general-purpose specialisation techniques for CFR, in particular
the techniques of Gallagher [19] for partial evaluation of Constrained Horn
Clauses (CHCs). Basing CFR on partial evaluation has the clear advantage that
soundness comes for free because partial evaluation guarantees semantic
equivalence between the original program and its transformed version.
Moreover, this way we obtain a CFR procedure that is not tailored for a
particular purpose, but rather can be tuned depending on the application
domain.

Domenech et al. [16] developed such a CFR procedure for TSs, by transforming
TSs into CHCs and using the partial evaluator of Gallagher [19], and
integrated it in a termination analysis algorithm in a way that allows
applying CFR at different levels of granularity, and thus controlling the
trade-off between precision and performance. This is done by suggesting
different schemes for applying CFR, not only as a preprocessing step but also
on specific parts of the TS which we could not prove terminating. Moreover,
they developed heuristics for automatically configuring partial evaluation
(i.e., inferring properties to guides specialisation) in order to achieve the
desired CFR. Experimental evaluation provides a clear evidence to that their
CFR procedure significantly improves the precision of termination analysis,
cost analysis, and invariants generation.

Let use demonstrate this CFR procedure on the TS ${\cal T}$ that is depicted
in Figure 1. In a first step, the TS ${\cal T}$ is translated into the
following (semantically) equivalent CHC program:

$\begin{array}[]{rlllll}q_{\\_}{\mathtt{n_{\\_}0}}(x,y,z)\leftarrow&q_{\\_}{\mathtt{n_{\\_}1}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}1}}(x,y,z)\leftarrow&\\{x\geq
1\\},&q_{\\_}{\mathtt{n_{\\_}2}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}1}}(x,y,z)\leftarrow&\\{x\leq
0\\},&q_{\\_}{\mathtt{n_{\\_}3}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}2}}(x,y,z)\leftarrow&\\{y\leq
z-1,&y^{\prime}=y+1\\},&q_{\\_}{\mathtt{n_{\\_}1}}(x,y^{\prime},z).\\\
q_{\\_}{\mathtt{n_{\\_}2}}(x,y,z)\leftarrow&\\{y\geq
z,&x^{\prime}=x-1\\},&q_{\\_}{\mathtt{n_{\\_}1}}(x^{\prime},y,z).\\\
\end{array}$

Then the partial evaluator of Gallagher [19] is applied, using the
(automatically inferred) properties $\\{x\geq 1,y\geq z\\}$ for the loop head
predicate $q_{\\_}{\mathtt{n_{\\_}1}}(x,y,z)$, which results in the following
CHC program:

$\begin{array}[]{rllllll}q_{\\_}{\mathtt{n_{\\_}0}}(x,y,z)\leftarrow&q_{\\_}{\mathtt{n_{\\_}1^{3}}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}1^{3}}}(x,y,z)\leftarrow&\\{x\leq
0\\},&q_{\\_}{\mathtt{n_{\\_}3^{2}}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}1^{3}}}(x,y,z)\leftarrow&\\{x\geq
1\\},&q_{\\_}{\mathtt{n_{\\_}2^{2}}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}2^{2}}}(x,y,z)\leftarrow&\\{x\geq 1,&y\leq
z-1,&y^{\prime}=y+1\\},&q_{\\_}{\mathtt{n_{\\_}1^{2}}}(x,y^{\prime},z).\\\
q_{\\_}{\mathtt{n_{\\_}2^{2}}}(x,y,z)\leftarrow&\\{x\geq 1,&y\geq
z,&x^{\prime}=x-1\\},&q_{\\_}{\mathtt{n_{\\_}1^{1}}}(x^{\prime},y,z).\\\
q_{\\_}{\mathtt{n_{\\_}1^{2}}}(x,y,z)\leftarrow&\\{x\geq
1\\},&q_{\\_}{\mathtt{n_{\\_}2^{2}}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}1^{1}}}(x,y,z)\leftarrow&\\{x\leq 0,&y\geq
z\\},&q_{\\_}{\mathtt{n_{\\_}3^{1}}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}1^{1}}}(x,y,z)\leftarrow&\\{x\geq 1,&y\geq
z\\},&q_{\\_}{\mathtt{n_{\\_}2^{1}}}(x,y,z).\\\
q_{\\_}{\mathtt{n_{\\_}2^{1}}}(x,y,z)\leftarrow&\\{x\geq 1,&y\geq
z,&x^{\prime}=x-1\\},&q_{\\_}{\mathtt{n_{\\_}1^{1}}}(x^{\prime},y,z).\\\
\end{array}$

Now translating this CHC program into a TS results in the TS ${\cal
T}_{\\_}{pe}$ that is depicted in Figure 1. Note that the two phases are now
separated into two different strongly connected components, which can be
proven terminating using only LRFs.

##  4 Concluding Remarks

In this paper we have discussed techniques for proving termination of programs
with multiphase control-flow, where the execution passes through several
(possibly implicit) phases. In particular, we have discussed techniques that
correspond to our recent work: (1) the use of multiphase ranking functions [9,
5]; and (2) the use of control-flow refinement [16]. As a byproduct of our
research, we have developed an open-source termination analyser called
iRankFinder 222http://irankfinder.loopkiller.com that implements all these
techniques as well as other state-of-the-art techniques. Some of the
components of iRankFinder can be used independently, in particular the CFR
component that can be used to incorporate CFR in static analysers with little
effort.

### Future Work.

For M$\Phi$RFs, an obvious future direction is to study the problem of
deciding whether a TS has a M$\Phi$RF, both from algorithmic and theoretical
complexity perspectives. In initial unpublished work, we have proven that the
corresponding decision problem is NP-hard for the rational setting, but we
could not obtain a further classification. Further exploration of the
M$\Phi$RF problem for SLC loops is also required since it is not solved for
the general case yet. For CFR, we have developed some heuristics for the
automatic inference of properties, which is crucial for obtaining the desired
transformations, but further research in this direction is required. We
concentrated on CFR of TSs, and in a future direction one could apply our CFR
techniques for program representations that allow recursion as well.
Technically, this would not require much work since the partial evaluation
techniques of Gallagher [19] specialise CHCs that include recursion already.
We also concentrated on numerical programs, and a possible future direction
can concentrate on using CFR for program analysis tools where the data is not
necessarily numerical. Here one should also adapt the partial evaluation
techniques to support such specialisations, which seems doable for the partial
evaluation techniques of Gallagher [19] since it is based on using abstract
properties like those used in abstract domains of program analysis.

## References

  * [1]
  * [2] Elvira Albert, Puri Arenas, Samir Genaim & Germán Puebla (2011): _Closed-Form Upper Bounds in Static Cost Analysis_.  Journal of Automated Reasoning 46(2), pp. 161–203, 10.1007/s10817-010-9174-1.
  * [3] Elvira Albert, Miquel Bofill, Cristina Borralleras, Enrique Martin-Martin & Albert Rubio (2019): _Resource Analysis driven by (Conditional) Termination Proofs_.  Theory and Practice of Logic Programming 19(5-6), pp. 722–739, 10.1017/S1471068419000152.
  * [4] Christophe Alias, Alain Darte, Paul Feautrier & Laure Gonnord (2010): _Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs_.  In Radhia Cousot & Matthieu Martel, editors: Static Analysis Symposium, SAS’10, LNCS 6337, Springer, pp. 117–133, 10.1007/978-3-642-15769-18.
  * [5] Amir M. Ben-Amram, Jesús J. Doménech & Samir Genaim (2019): _Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets_.  In Bor-Yuh Evan Chang, editor: Proceedings of the 26th International Symposium on Static Analysis, SAS’19, Lecture Notes in Computer Science 11822, Springer, pp. 459–480, 10.1007/978-3-030-32304-222.
  * [6] Amir M. Ben-Amram & Samir Genaim (2013): _On the Linear Ranking Problem for Integer Linear-Constraint Loops_.  In: Principles of programming languages, POPL’13, ACM, pp. 51–62, 10.1145/2480359.2429078.
  * [7] Amir M. Ben-Amram & Samir Genaim (2014): _Ranking Functions for Linear-Constraint Loops_.  Journal of the ACM 61(4), pp. 26:1–26:55, 10.1145/2629488.
  * [8] Amir M. Ben-Amram & Samir Genaim (2015): _Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions_.  In Daniel Kroening & Corina S. Păsăreanu, editors: Computer Aided Verification, CAV’14, LNCS 9207, Springer, pp. 304–321, 10.1007/978-3-319-21668-318.
  * [9] Amir M. Ben-Amram & Samir Genaim (2017): _On Multiphase-Linear Ranking Functions_.  In Rupak Majumdar & Viktor Kuncak, editors: Computer Aided Verification, CAV’17, LNCS 10427, Springer, pp. 601–620, 10.1007/978-3-319-63390-932.
  * [10] Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell & Albert Rubio (2017): _Proving Termination Through Conditional Termination_.  In Axel Legay & Tiziana Margaria, editors: Tools and Algorithms for the Construction and Analysis of Systems, TACAS’17, LNCS 10205, pp. 99–117, 10.1007/978-3-662-54577-56.
  * [11] Aaron R. Bradley, Zohar Manna & Henny B. Sipma (2005): _Linear Ranking with Reachability_.  In Kousha Etessami & Sriram K. Rajamani, editors: Computer Aided Verification, CAV’05, LNCS 3576, Springer, pp. 491–504, 10.1007/1151398848.
  * [12] Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs & Jürgen Giesl (2016): _Analyzing Runtime and Size Complexity of Integer Programs_.  ACM Transactions on Programming Languages and Systems, TOPLAS’16 38(4), pp. 13:1–13:50.  Available at https://doi.org/10.1145/2866575.
  * [13] Maurice Bruynooghe, Michael Codish, John P. Gallagher, Samir Genaim & Wim Vanhoof (2007): _Termination analysis of logic programs through combination of type-based norms_.  ACM Transactions on Programming Languages and Systems, TOPLAS’07 29(2), pp. 10–54.  Available at https://doi.org/10.1145/1216374.1216378.
  * [14] Michael Colón & Henny Sipma (2001): _Synthesis of Linear Ranking Functions_.  In Tiziana Margaria & Wang Yi, editors: Tools and Algorithms for the Construction and Analysis of Systems, TACAS’01, LNCS 2031, Springer, pp. 67–81, 10.1007/3-540-45319-96.
  * [15] Jesús J. Domenech (2021): _Termination Analysis of Programs with Complex Control-Flow_.  Ph.D. thesis, Facultad de Informática, Universidad Complutense de Madrid.
  * [16] Jesús J. Doménech, John P. Gallagher & Samir Genaim (2019): _Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis_.  Theory Pract. Log. Program. 19(5-6), pp. 990–1005, 10.1017/S1471068419000310.
  * [17] Paul Feautrier (1992): _Some efficient solutions to the affine scheduling problem. I. One-dimensional time_.  International Journal of Parallel Programming 21(5), pp. 313–347.  Available at https://doi.org/10.1007/BF01407835.
  * [18] Antonio Flores-Montoya & Reiner Hähnle (2014): _Resource Analysis of Complex Programs with Cost Equations_.  In Jacques Garrigue, editor: Asian Symposium on Programming Languages and Systems, APLAS’14, LNCS 8858, Springer, pp. 275–295.  Available at https://doi.org/10.1007/978-3-319-12736-1_15.
  * [19] John P. Gallagher (2019): _Polyvariant program specialisation with property-based abstraction_.  In Alexei Lisitsa & Andrei P. Nemytykh, editors: Verification and Program Transformation, VPT’19, 299, Open Publishing Association, pp. 34–48.  Available at https://doi.org/10.4204/eptcs.299.6.
  * [20] Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski & René Thiemann (2017): _Analyzing Program Termination and Complexity Automatically with AProVE_.  Journal of Automated Reasoning 58(1), pp. 3–31.  Available at https://doi.org/10.1007/s10817-016-9388-y.
  * [21] Sumit Gulwani, Sagar Jain & Eric Koskinen (2009): _Control-flow refinement and progress invariants for bound analysis_.  In Michael Hind & Amer Diwan, editors: Programming Language Design and Implementation, PLDI’09, 44, ACM, pp. 375–385.  Available at https://doi.org/10.1145/1542476.1542518.
  * [22] Radu Iosif, Filip Konečný & Marius Bozga (2014): _Deciding Conditional Termination_.  Logical Methods in Computer Science 10(3), 10.2168/lmcs-10(3:8)2014.  Available at http://doi.org/10.2168/LMCS-10(3:8)2014.
  * [23] Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell & Albert Rubio (2013): _Proving termination of imperative programs using Max-SMT_.  In: Formal Methods in Computer-Aided Design, FMCAD’13, IEEE, pp. 218–225.  Available at https://doi.org/10.1109/FMCAD.2013.6679413.
  * [24] Chin Soon Lee, Neil D. Jones & Amir M. Ben-Amram (2001): _The size-change principle for program termination_.  In Chris Hankin & Dave Schmidt, editors: Principles of Programming Languages, POPL’01, ACM, pp. 81–92.  Available at https://doi.org/10.1145/360204.360210.
  * [25] Jan Leike & Matthias Heizmann (2015): _Ranking Templates for Linear Loops_.  Logical Methods in Computer Science 11(1), pp. 1–27, 10.2168/LMCS-11(1:16)2015.
  * [26] Yi Li, Guang Zhu & Yong Feng (2016): _The L-Depth Eventual Linear Ranking Functions for Single-Path Linear Constraint Loops_.  In: Theoretical Aspects of Software Engineering, TASE’16, IEEE, pp. 30–37.  Available at https://doi.org/10.1109/TASE.2016.8.
  * [27] Naomi Lindenstrauss & Yehoshua Sagiv (1997): _Automatic Termination Analysis of Logic Programs_.  In Lee Naish, editor: International Conference on Logic Programming, ICLP’97, MIT Press, pp. 64–77.  Available at https://ieeexplore.ieee.org/document/6279160.
  * [28] Stephen Magill, Ming-Hsien Tsai, Peter Lee & Yih-Kuen Tsay (2010): _Automatic numeric abstractions for heap-manipulating programs_.  In Manuel V. Hermenegildo & Jens Palsberg, editors: Principles of Programming Languages, POPL’10, ACM, pp. 211–222.  Available at https://doi.org/10.1145/1706299.1706326.
  * [29] Frédéric Mesnard & Alexander Serebrenik (2008): _Recurrence with affine level mappings is P-time decidable for CLP(R)_.  Theory and Practice of Logic Programming, TPLP’08 8(1), pp. 111–119.  Available at https://doi.org/10.1017/S1471068407003122.
  * [30] Andreas Podelski & Andrey Rybalchenko (2004): _A Complete Method for the Synthesis of Linear Ranking Functions_.  In Bernhard Steffen & Giorgio Levi, editors: Verification, Model Checking, and Abstract Interpretation, VMCAI’04, LNCS 2937, Springer, pp. 239–251, 10.1007/978-3-540-24622-020.
  * [31] Rahul Sharma, Isil Dillig, Thomas Dillig & Alex Aiken (2011): _Simplifying Loop Invariant Generation Using Splitter Predicates_.  In Ganesh Gopalakrishnan & Shaz Qadeer, editors: Computer Aided Verification, CAV’11, LNCS 6806, Springer, pp. 703–719, 10.1007/s10990-006-8609-1.
  * [32] Kirack Sohn & Allen Van Gelder (1991): _Termination Detection in Logic Programs using Argument Sizes_.  In Daniel J. Rosenkrantz, editor: Principles of Database Systems, PoDS’91, ACM Press, pp. 216–226.  Available at https://doi.org/10.1145/113413.113433.
  * [33] Fausto Spoto, Fred Mesnard & Étienne Payet (2010): _A termination analyzer for Java bytecode based on path-length_.  ACM Transactions on Programming Languages and Systems, TOPLAS’10 32(3).  Available at https://doi.org/10.1145/1709093.1709095.
  * [34] Alan M. Turing (1949): _Checking a Large Routine_.  In: Report on a Conference on High Speed Automatic Computation, June 1949, University Mathematical Laboratory, Cambridge University, pp. 67–69.  Available at http://www.turingarchive.org/browse.php/B/8.
  * [35] Yue Yuan, Yi Li & Wenchang Shi (2021): _Detecting multiphase linear ranking functions for single-path linear-constraint loops_.  Int. J. Softw. Tools Technol. Transf. 23(1), pp. 55–67, 10.1007/s10009-019-00527-1.