@incollection(ALBERT08,
 author       = {{Albert, E. and Arenas, P. and Genaim, S. and Puebla, G. and Zanardini, D.}},
 year         = {2008},
 title        = {{COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode}},
 booktitle    = {{Formal Methods for Components and Objects: 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, October 24-26, 2007, Revised Lectures}},
 publisher    = {{Springer-Verlag}},
 pages        = {{113---132}},
 doi          = {10.1007/978-3-540-92188-2\_5},
)
@phdthesis(ARTS97,
 author       = {T. Arts},
 year         = {1997},
 title        = {{Automatically Proving Termination and Innermost Normalisation of Term Rewriting Systems}},
 school       = {{Universiteit Utrecht}},
)
@inproceedings(BERDINE06,
 author       = {J. Berdine and B. Cook and D. Distefano and P. W. O'Hearn},
 year         = {2006},
 title        = {{Automatic Termination Proofs for Programs with Shape-Shifting Heaps}},
 booktitle    = {{International Conference on Computer Aided Verification}},
 pages        = {{386---400}},
 doi          = {10.1007/11817963\_35},
)
@inproceedings(BRADLEY05B,
 author       = {A. Bradley and Z. Manna and H.B. Sipma},
 year         = {2005},
 title        = {{Linear Ranking with Reachability}},
 booktitle    = {17th International Conference on Computer Aided Verification,},
 pages        = {{491--504}},
 doi          = {10.1007/11513988\_48},
)
@inproceedings(BRADLEY05A,
 author       = {A. R. Bradley and Z. Manna and H. B. Sipma},
 year         = {2005},
 title        = {{Termination of Polynomial Programs}},
 booktitle    = {{International Conference on Verification, Model Checking, and Abstract Interpretation}},
 pages        = {{113--129}},
 doi          = {10.1007/978-3-540-30579-8\_8},
)
@inproceedings(BROTHERSTON08,
 author       = {J. Brotherston and R. Bornat and C. Calcagno},
 year         = {2008},
 title        = {{Cyclic Proofs of Program Termination in Separation Logic}},
 booktitle    = {{ACM Symposium on Principles of Programming Languages}},
 pages        = {{101--112}},
 doi          = {10.1145/1328897.1328453},
)
@inproceedings(CODISH97,
 author       = {M. Codish and C. Taboch},
 year         = {1997},
 title        = {{A Semantic Basis for Termination Analysis of Logic Programs and its Realization Using Symbolic Norm Constraints}},
 booktitle    = {{International Joint Conference on Algebraic and Logic Programming}},
 series       = {Lecture Notes in Computer Science},
 volume       = {1298},
 pages        = {{31--45}},
 doi          = {10.1007/BFb0027001},
)
@article(COOK06,
 author       = {B. Cook and A. Podelski and A. Rybalchenko},
 year         = {2006},
 title        = {{Termination Proofs for Systems Code}},
 journal      = {{SIGPLAN Notices}},
 volume       = {41},
 number       = {6},
 pages        = {{415---426}},
 doi          = {10.1145/1133255.1134029},
)
@article(COOK11,
 author       = {B. Cook and A. Podelski and A. Rybalchenko},
 year         = {2011},
 title        = {{Proving Program Termination}},
 journal      = {{Communications of the ACM}},
 volume       = {54},
 number       = {5},
 pages        = {{88---98}},
 doi          = {10.1145/1941487.1941509},
)
@article(DERSHOWITZ87,
 author       = {N. Dershowitz},
 year         = {1987},
 title        = {{Termination of Rewriting}},
 journal      = {{Journal of Symbolic Computation}},
 volume       = {3},
 pages        = {{69--116}},
 doi          = {10.1016/S0747-7171(87)80022-6},
)
@inproceedings(FLOYD67,
 author       = {R.W. Floyd},
 year         = {1967},
 title        = {Assigning Meanings to Programs},
 booktitle    = {Proceedings of the American Mathematical Society Symposia on Applied Mathematics},
 volume       = {19},
 pages        = {19--32},
 doi          = {10.1007/978-94-011-1793-7\_4},
)
@inproceedings(GEISL95,
 author       = {J. Geisl},
 year         = {1995},
 title        = {{Termination Analysis for Functional Programs Using Term Orderings}},
 booktitle    = {{Second International Static Analysis Symposium}},
 series       = {Lecture Notes in Computer Science},
 volume       = {983},
 pages        = {{154--171}},
 doi          = {10.1007/3-540-60360-3\_38},
)
@inproceedings(GEISL14,
 author       = {J. Giesl and M. Brockschmidt and F. Emmes and C. Frohn, F. Fuhs and C. Otto and M. Pl{\"u}cker and Schneider-Kamp, P. and T. Str{\"o}der and S. Swiderski and R Thiemann.},
 year         = {2014},
 title        = {{Proving Termination of Programs Automatically with AProVE}},
 booktitle    = {{International Joint Conference on Automated Reasoning}},
 pages        = {{184--191}},
 doi          = {10.1007/978-3-319-08587-6\_13},
)
@inproceedings(GEISL06,
 author       = {J. Giesl and S. Swiderski and Schneider-Kamp, P. and R. Thiemann},
 year         = {2006},
 title        = {{Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages.}},
 booktitle    = {{International Conference on Rewriting Techniques and Applications}},
 pages        = {{297--312}},
 doi          = {10.1007/11805618\_23},
)
@inproceedings(HAMILTON07A,
 author       = {G.W. Hamilton},
 year         = {2007},
 title        = {{D}istillation: {E}xtracting the {E}ssence of {P}rograms},
 booktitle    = {Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation},
 pages        = {61--70},
 doi          = {10.1145/1244381.1244391},
)
@inproceedings(HAMILTON12,
 author       = {G.W. Hamilton and N.D. Jones},
 year         = {2012},
 title        = {Distillation With Labelled Transition Systems},
 booktitle    = {Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation},
 publisher    = {ACM},
 pages        = {15--24},
 doi          = {10.1145/2103746.2103753},
)
@inproceedings(LEE01,
 author       = {C.S. Lee and N.D. Jones and Ben-Amram, A.M.},
 year         = {2001},
 title        = {{The Size-Change Principle for Program Termination}},
 booktitle    = {{The 28th ACM Symposium on Principles of Programming Languages}},
 pages        = {{81--92}},
 doi          = {10.1145/360204.360210},
)
@inproceedings(LINDENSTRAUSS97,
 author       = {N. Lindenstrauss and Y. Sagiv},
 year         = {1997},
 title        = {{Automatic Termination Analysis of Prolog Programs}},
 booktitle    = {{International Conference on Logic Programming}},
 pages        = {{64--77}},
)
@inproceedings(MANOLIOS06,
 author       = {P. Manolios and D. Vroon},
 year         = {2006},
 title        = {{Termination Analysis with Calling Context Graphs}},
 booktitle    = {{International Conference on Computer Aided Verification}},
 pages        = {{401--414}},
 doi          = {10.1007/11817963\_36},
)
@inproceedings(SAGIV91,
 author       = {Y. Sagiv},
 year         = {1991},
 title        = {{A Termination Test for Logic Programs}},
 booktitle    = {{International Symposium on Logic Programming}},
 pages        = {{518--532}},
)
@inproceedings(SERENI05,
 author       = {D. Sereni D. and N.D. Jones},
 year         = {2005},
 title        = {Termination Analysis of Higher-Order Functional Programs},
 booktitle    = {Asian Symposium on Programming Languages and Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {3780},
 pages        = {281--297},
 doi          = {10.1007/11575467\_19},
)
@article(SORENSEN96,
 author       = {S{\o}rensen, M.H. and R. Gl{\"u}ck and N.D. Jones},
 year         = {1996},
 title        = {{A Positive Supercompiler}},
 journal      = {Journal of Functional Programming},
 volume       = {6},
 number       = {6},
 pages        = {811--838},
 doi          = {10.1017/S0956796800002008},
)
@article(SPOTO10,
 author       = {{Spoto, F. and Mesnard, F. and Payet, E.}},
 year         = {2010},
 title        = {{A Termination Analyzer for Java Bytecode Based on Path-Length}},
 journal      = {{ACM Transaction on Programming Languages and Systems}},
 volume       = {32},
 number       = {3},
 pages        = {{8:1--8:70}},
 doi          = {10.1145/1709093.1709095},
)
@inproceedings(STEINBACH95,
 author       = {J. Steinbach},
 year         = {1995},
 title        = {{Automatic Termination Proofs With Transformation Orderings}},
 booktitle    = {{International Conference on Rewriting Techniques and Applications}},
 series       = {Lecture Notes in Computer Science},
 volume       = {914},
 pages        = {{11--25}},
 doi          = {10.1007/3-540-59200-8\_44},
)
@article(TURCHIN86,
 author       = {V.F. Turchin},
 year         = {1986},
 title        = {{The Concept of a Supercompiler}},
 journal      = {ACM Transactions on Programming Languages and Systems},
 volume       = {8},
 number       = {3},
 pages        = {90--121},
 doi          = {10.1145/5956.5957},
)
@article(TURING36,
 author       = {A.M. Turing},
 year         = {1936},
 title        = {{On Computable Numbers, with an Application to the Entscheidungsproblem}},
 journal      = {{Proceedings of the London Mathematical Society, 2}},
 volume       = {42},
 number       = {1},
 pages        = {{230--265}},
 doi          = {10.1112/plms/s2-42.1.230},
)
@inproceedings(TURING48,
 author       = {A.M. Turing},
 year         = {1948},
 title        = {{Checking a Large Routine}},
 booktitle    = {{The Early British Computer Conferences}},
 pages        = {{70--72}},
 doi          = {10.5555/94938.94952},
)