@article(AlbertAGP11,
 author       = {Elvira Albert and Puri Arenas and Samir Genaim and Germ{\'{a}}n Puebla},
 year         = {2011},
 title        = {Closed-Form Upper Bounds in Static Cost Analysis},
 journal      = {Journal of Automated Reasoning},
 volume       = {46},
 number       = {2},
 pages        = {161--203},
 doi          = {10.1007/s10817-010-9174-1},
)
@article(AlbertBBMR19,
 author       = {Elvira Albert and Miquel Bofill and Cristina Borralleras and Martin{-}Martin, Enrique and Albert Rubio},
 year         = {2019},
 title        = {Resource Analysis driven by (Conditional) Termination Proofs},
 journal      = {Theory and Practice of Logic Programming},
 volume       = {19},
 number       = {5-6},
 pages        = {722--739},
 doi          = {10.1017/S1471068419000152},
)
@inproceedings(ADFG:2010,
 author       = {Christophe Alias and Alain Darte and Paul Feautrier and Laure Gonnord},
 year         = {2010},
 title        = {Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs},
 editor       = {Radhia Cousot and Matthieu Martel},
 booktitle    = {Static Analysis Symposium, SAS'10},
 series       = {LNCS},
 volume       = {6337},
 publisher    = {Springer},
 pages        = {117--133},
 doi          = {10.1007/978-3-642-15769-1_8},
)
@inproceedings(Ben-AmramDG19,
 author       = {Ben{-}Amram, Amir~M. and Jes{\'{u}}s~J. Dom{\'{e}}nech and Samir Genaim},
 year         = {2019},
 title        = {{M}ultiphase-{L}inear {R}anking {F}unctions and {T}heir {R}elation to {R}ecurrent {S}ets},
 editor       = {Bor{-}Yuh~Evan Chang},
 booktitle    = {Proceedings of the 26th International Symposium on Static Analysis, SAS'19},
 series       = {Lecture Notes in Computer Science},
 volume       = {11822},
 publisher    = {Springer},
 pages        = {459--480},
 doi          = {10.1007/978-3-030-32304-2_22},
)
@inproceedings(Ben-AmramG13popl,
 author       = {Ben-Amram, Amir~M. and Samir Genaim},
 year         = {2013},
 title        = {On the Linear Ranking Problem for Integer Linear-Constraint Loops},
 booktitle    = {Principles of programming languages, POPL'13},
 publisher    = {ACM},
 pages        = {51--62},
 doi          = {10.1145/2480359.2429078},
)
@article(Ben-AmramG13jv,
 author       = {Ben-Amram, Amir~M. and Samir Genaim},
 year         = {2014},
 title        = {Ranking Functions for Linear-Constraint Loops},
 journal      = {Journal of the ACM},
 volume       = {61},
 number       = {4},
 pages        = {26:1--26:55},
 doi          = {10.1145/2629488},
)
@inproceedings(Ben-AmramG15,
 author       = {Ben{-}Amram, Amir~M. and Samir Genaim},
 year         = {2015},
 title        = {Complexity of {Bradley-Manna-Sipma} Lexicographic Ranking Functions},
 editor       = {Daniel Kroening and P{\u{a}}s{\u{a}}reanu, Corina~S.},
 booktitle    = {Computer Aided Verification, CAV'14},
 series       = {LNCS},
 volume       = {9207},
 publisher    = {Springer},
 pages        = {304--321},
 doi          = {10.1007/978-3-319-21668-3_18},
)
@inproceedings(Ben-AmramG17,
 author       = {Ben{-}Amram, Amir~M. and Samir Genaim},
 year         = {2017},
 title        = {On Multiphase-Linear Ranking Functions},
 editor       = {Rupak Majumdar and Viktor Kuncak},
 booktitle    = {Computer Aided Verification, CAV'17},
 series       = {LNCS},
 volume       = {10427},
 publisher    = {Springer},
 pages        = {601--620},
 doi          = {10.1007/978-3-319-63390-9_32},
)
@inproceedings(BorrallerasBLOR17,
 author       = {Cristina Borralleras and Marc Brockschmidt and Daniel Larraz and Albert Oliveras and Rodr{\'{\i}}guez{-}Carbonell, Enric and Albert Rubio},
 year         = {2017},
 title        = {Proving Termination Through Conditional Termination},
 editor       = {Axel Legay and Tiziana Margaria},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems, TACAS'17},
 series       = {LNCS},
 volume       = {10205},
 pages        = {99--117},
 doi          = {10.1007/978-3-662-54577-5_6},
)
@inproceedings(DBLP:conf/cav/BradleyMS05,
 author       = {Aaron~R. Bradley and Zohar Manna and Henny~B. Sipma},
 year         = {2005},
 title        = {Linear Ranking with Reachability},
 editor       = {Kousha Etessami and Sriram~K. Rajamani},
 booktitle    = {Computer Aided Verification, CAV'05},
 series       = {LNCS},
 volume       = {3576},
 publisher    = {Springer},
 pages        = {491--504},
 doi          = {10.1007/11513988_48},
)
@article(BrockschmidtE0F16,
 author       = {Marc Brockschmidt and Fabian Emmes and Stephan Falke and Carsten Fuhs and J{\"{u}}rgen Giesl},
 year         = {2016},
 title        = {Analyzing Runtime and Size Complexity of Integer Programs},
 journal      = {{ACM} Transactions on Programming Languages and Systems, {TOPLAS}'16},
 volume       = {38},
 number       = {4},
 pages        = {13:1--13:50},
 url          = {https://doi.org/10.1145/2866575},
)
@article(DBLP:journals/toplas/BruynoogheCGGV07,
 author       = {Maurice Bruynooghe and Michael Codish and John~P. Gallagher and Samir Genaim and Wim Vanhoof},
 year         = {2007},
 title        = {Termination analysis of logic programs through combination of type-based norms},
 journal      = {{ACM} Transactions on Programming Languages and Systems, {TOPLAS}'07},
 volume       = {29},
 number       = {2},
 pages        = {10--54},
 url          = {https://doi.org/10.1145/1216374.1216378},
)
@inproceedings(DBLP:conf/tacas/ColonS01,
 author       = {Michael Col{\'o}n and Henny Sipma},
 year         = {2001},
 title        = {Synthesis of Linear Ranking Functions},
 editor       = {Tiziana Margaria and Wang Yi},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems, TACAS'01},
 series       = {LNCS},
 volume       = {2031},
 publisher    = {Springer},
 pages        = {67--81},
 doi          = {10.1007/3-540-45319-9_6},
)
@phdthesis(Domenech21,
 author       = {Jes\'us~J. Domenech},
 year         = {2021},
 title        = {Termination Analysis of Programs with Complex Control-Flow},
 school       = {Facultad de Inform\'atica, Universidad Complutense de Madrid},
)
@article(DomenechGG19,
 author       = {Jes{\'{u}}s~J. Dom{\'{e}}nech and John~P. Gallagher and Samir Genaim},
 year         = {2019},
 title        = {Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis},
 journal      = {Theory Pract. Log. Program.},
 volume       = {19},
 number       = {5-6},
 pages        = {990--1005},
 doi          = {10.1017/S1471068419000310},
)
@article(Feautrier92.1,
 author       = {Paul Feautrier},
 year         = {1992},
 title        = {Some efficient solutions to the affine scheduling problem. {I}. {O}ne-dimensional time},
 journal      = {International Journal of Parallel Programming},
 volume       = {21},
 number       = {5},
 pages        = {313--347},
 url          = {https://doi.org/10.1007/BF01407835},
)
@inproceedings(Flores-MontoyaH14,
 author       = {Flores{-}Montoya, Antonio and Reiner H{\"{a}}hnle},
 year         = {2014},
 title        = {Resource Analysis of Complex Programs with Cost Equations},
 editor       = {Jacques Garrigue},
 booktitle    = {Asian Symposium on Programming Languages and Systems, {APLAS}'14},
 series       = {LNCS},
 volume       = {8858},
 publisher    = {Springer},
 pages        = {275--295},
 url          = {https://doi.org/10.1007/978-3-319-12736-1_15},
)
@inproceedings(Gallagher19,
 author       = {John~P. Gallagher},
 year         = {2019},
 title        = {Polyvariant program specialisation with property-based abstraction},
 editor       = {Alexei Lisitsa and Andrei~P. Nemytykh},
 booktitle    = {Verification and Program Transformation, VPT'19},
 volume       = {299},
 publisher    = {Open Publishing Association},
 pages        = {34--48},
 url          = {https://doi.org/10.4204/eptcs.299.6},
)
@article(aprove17,
 author       = {J{\"u}rgen Giesl and Cornelius Aschermann and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Jera Hensel and Carsten Otto and Martin Pl{\"u}cker and Schneider-Kamp, Peter and Thomas Str{\"o}der and Stephanie Swiderski and Ren{\'e} Thiemann},
 year         = {2017},
 title        = {Analyzing Program Termination and Complexity Automatically with {AProVE}},
 journal      = {Journal of Automated Reasoning},
 volume       = {58},
 number       = {1},
 pages        = {3--31},
 url          = {https://doi.org/10.1007/s10817-016-9388-y},
)
@inproceedings(GulwaniJK09,
 author       = {Sumit Gulwani and Sagar Jain and Eric Koskinen},
 year         = {2009},
 title        = {Control-flow refinement and progress invariants for bound analysis},
 editor       = {Michael Hind and Amer Diwan},
 booktitle    = {Programming Language Design and Implementation, {PLDI}'09},
 volume       = {44},
 publisher    = {{ACM}},
 pages        = {375--385},
 url          = {https://doi.org/10.1145/1542476.1542518},
)
@article(BIKtacas2012jv,
 author       = {Radu Iosif and Kone{\v{c}}n{\'y}, Filip and Marius Bozga},
 year         = {2014},
 title        = {Deciding Conditional Termination},
 journal      = {Logical Methods in Computer Science},
 volume       = {10},
 number       = {3},
 doi          = {10.2168/lmcs-10(3:8)2014},
 url          = {http://doi.org/10.2168/LMCS-10(3:8)2014},
)
@inproceedings(LarrazORR13,
 author       = {Daniel Larraz and Albert Oliveras and Rodr\'{\i}guez-Carbonell, Enric and Albert Rubio},
 year         = {2013},
 title        = {Proving termination of imperative programs using {Max-SMT}},
 booktitle    = {Formal Methods in Computer-Aided Design, FMCAD'13},
 publisher    = {IEEE},
 pages        = {218--225},
 url          = {https://doi.org/10.1109/FMCAD.2013.6679413},
)
@inproceedings(DBLP:conf/popl/LeeJB01,
 author       = {Chin~Soon Lee and Neil~D. Jones and Ben-Amram, Amir~M.},
 year         = {2001},
 title        = {The size-change principle for program termination},
 editor       = {Chris Hankin and Dave Schmidt},
 booktitle    = {Principles of Programming Languages, POPL'01},
 publisher    = {{ACM}},
 pages        = {81--92},
 url          = {https://doi.org/10.1145/360204.360210},
)
@article(LeikeHeizmann15,
 author       = {Jan Leike and Matthias Heizmann},
 year         = {2015},
 title        = {Ranking Templates for Linear Loops},
 journal      = {Logical Methods in Computer Science},
 volume       = {11},
 number       = {1},
 pages        = {1--27},
 doi          = {10.2168/LMCS-11(1:16)2015},
)
@inproceedings(li2016depth,
 author       = {Yi~Li and Guang Zhu and Yong Feng},
 year         = {2016},
 title        = {The {L}-Depth Eventual Linear Ranking Functions for Single-Path Linear Constraint Loops},
 booktitle    = {Theoretical Aspects of Software Engineering, TASE'16},
 organization = {IEEE},
 pages        = {30--37},
 url          = {https://doi.org/10.1109/TASE.2016.8},
)
@inproceedings(LS:97,
 author       = {Naomi Lindenstrauss and Yehoshua Sagiv},
 year         = {1997},
 title        = {Automatic Termination Analysis of {L}ogic Programs},
 editor       = {Lee Naish},
 booktitle    = {International Conference on Logic Programming, ICLP'97},
 publisher    = {{MIT} {P}ress},
 pages        = {64--77},
 url          = {https://ieeexplore.ieee.org/document/6279160},
)
@inproceedings(DBLP:conf/popl/MagillTLT10,
 author       = {Stephen Magill and Ming-Hsien Tsai and Peter Lee and Yih-Kuen Tsay},
 year         = {2010},
 title        = {Automatic numeric abstractions for heap-manipulating programs},
 editor       = {Manuel~V. Hermenegildo and Jens Palsberg},
 booktitle    = {Principles of Programming Languages, POPL'10},
 publisher    = {{ACM}},
 pages        = {211--222},
 url          = {https://doi.org/10.1145/1706299.1706326},
)
@article(DBLP:journals/tplp/MesnardS08,
 author       = {Fr{\'e}d{\'e}ric Mesnard and Alexander Serebrenik},
 year         = {2008},
 title        = {Recurrence with affine level mappings is {P}-time decidable for {CLP(R)}},
 journal      = {{Theory and Practice of Logic Programming, TPLP'08}},
 volume       = {8},
 number       = {1},
 pages        = {111--119},
 url          = {https://doi.org/10.1017/S1471068407003122},
)
@inproceedings(DBLP:conf/vmcai/PodelskiR04,
 author       = {Andreas Podelski and Andrey Rybalchenko},
 year         = {2004},
 title        = {A Complete Method for the Synthesis of Linear Ranking Functions},
 editor       = {Bernhard Steffen and Giorgio Levi},
 booktitle    = {Verification, Model Checking, and Abstract Interpretation, VMCAI'04},
 series       = {LNCS},
 volume       = {2937},
 publisher    = {Springer},
 pages        = {239--251},
 doi          = {10.1007/978-3-540-24622-0_20},
)
@inproceedings(SharmaDDA11,
 author       = {Rahul Sharma and Isil Dillig and Thomas Dillig and Alex Aiken},
 year         = {2011},
 title        = {Simplifying Loop Invariant Generation Using Splitter Predicates},
 editor       = {Ganesh Gopalakrishnan and Shaz Qadeer},
 booktitle    = {Computer Aided Verification, {CAV}'11},
 series       = {LNCS},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {703--719},
 doi          = {10.1007/s10990-006-8609-1},
)
@inproceedings(DBLP:conf/pods/SohnG91,
 author       = {Kirack Sohn and Allen~Van Gelder},
 year         = {1991},
 title        = {Termination Detection in Logic Programs using Argument Sizes},
 editor       = {Daniel~J. Rosenkrantz},
 booktitle    = {Principles of Database Systems, PoDS'91},
 publisher    = {ACM Press},
 pages        = {216--226},
 url          = {https://doi.org/10.1145/113413.113433},
)
@article(DBLP:journals/toplas/SpotoMP10,
 author       = {Fausto Spoto and Fred Mesnard and {\'E}tienne Payet},
 year         = {2010},
 title        = {A termination analyzer for Java bytecode based on path-length},
 journal      = {{ACM} Transactions on Programming Languages and Systems, {TOPLAS}'10},
 volume       = {32},
 number       = {3},
 url          = {https://doi.org/10.1145/1709093.1709095},
)
@inproceedings(Turing:1949:CLR,
 author       = {Alan~M. Turing},
 year         = {1949},
 title        = {Checking a Large Routine},
 booktitle    = {Report on a Conference on High Speed Automatic Computation, June 1949},
 publisher    = {University Mathematical Laboratory, Cambridge University},
 pages        = {67--69},
 url          = {http://www.turingarchive.org/browse.php/B/8},
)
@article(YuanLS21,
 author       = {Yue Yuan and Yi~Li and Wenchang Shi},
 year         = {2021},
 title        = {Detecting multiphase linear ranking functions for single-path linear-constraint loops},
 journal      = {Int. J. Softw. Tools Technol. Transf.},
 volume       = {23},
 number       = {1},
 pages        = {55--67},
 doi          = {10.1007/s10009-019-00527-1},
)