@techreport{TR-IC-14-14,
   number = {IC-14-14},
   author = {Rachid Rebiha and Arnaldo V. Moura and Nadir Matringe},
   title  = {On the Termination of Linear and Affine Programs over the
                   Integers},
   month = {July},
   year = {2014},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 27 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       The   termination   problem   for   affine  programs  over  the 
       \emph{integers}  was  left open in [1]. For more that a decade,
       it has been considered and cited as a challenging open problem.
       To the best of our knowledge, we present here the most complete
       response  to  this  issue:  we show that termination for affine
       programs  over  $\mathbb{Z}$  is  decidable under an assumption
       holding for almost all affine programs, except for an extremely
       small  class  of  zero  Lesbegue  measure. We use the notion of
       \emph{asymptotically  non-terminating  initial variable values}
       ($ANT$,  for short) for linear loop programs over $\mathbb{Z}$.
       Those values are directly associated to initial variable values
       for  which  the  corresponding  program  does not terminate. We
       reduce  the  termination problem of linear affine programs over
       the  integers to the emptiness check of a specific $ANT$ set of
       initial  variable  values.  For  this class of linear or affine
       programs,  we  prove  that  the  corresponding  $ANT$  set is a
       semi-linear  space  and  we  provide  a  powerful computational
       methods  allowing the automatic generation of these $ANT$ sets.
       Moreover,  we  are  able to address the conditional termination
       problem  too.  In other words, by taking $ANT$ set complements,
       we  obtain  a  precise under-approximation of the set of inputs
       for which the program does terminate.
  }
}