@article{CGBFG:11:TPLP,
  author = {Codish, Michael and Gonopolskiy, Igor and Ben-Amram, Amir M. and Fuhs, Carsten and Giesl, J{\"u}rgen},
  title = {{SAT}-Based Termination Analysis Using Monotonicity Constraints over the Integers},
  journal = {Theory and Practice of Logic Programming, 26th Int'l.
Conference on Logic Programming (ICLP'11) Special Issue},
  editor = {M.~Hermenegildo and T.~Schaub},
  volume = {11},
  number = {Special Issue 4-5},
  pages = {503-520},
  year = {2011},
  month = {July},
  publisher = {Cambridge University Press},
 doi = {10.1017/S1471068411000147},
  URL = {http://dx.doi.org/10.1017/S1471068411000147},
  eprint = {http://journals.cambridge.org/article_S1471068411000147},
  abstract = { We describe an algorithm for proving termination of programs abstracted to systems of monotonicity constraints. 
      While deciding termination for this model is PSPACE complete, we focus on a subset, which we call MCNP 
      (``monotonicity constraints in {NP}"�),  amenable to a SAT-based solution. 
      We describe the application of our approach to the termination analysis of Java Bytecode. 
      As the front end, we two different termination analyzers: {AProVE} and {COSTA}.}
}