@article {1792,
title = {Reverse mathematical bounds for the Termination Theorem},
journal = {Annals of Pure and Applied Logic},
year = {2016},
abstract = {Abstract In 2004 Podelski and Rybalchenko expressed the termination of transition-based programs as a property of well-founded relations. The classical proof by Podelski and Rybalchenko requires Ramsey{\textquoteright}s Theorem for pairs which is a purely classical result, therefore extracting bounds from the original proof is non-trivial task. Our goal is to investigate the termination analysis from the point of view of Reverse Mathematics. By studying the strength of Podelski and Rybalchenko{\textquoteright}s Termination Theorem we can extract some information about termination bounds.},
issn = {0168-0072},
doi = {10.1016/j.apal.2016.06.001},
url = {http://www.iam.unibe.ch/ltgpub/2016/styo16.pdf},
author = {Silvia Steila and Keita Yokoyama}
}