@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",
)
@article(DBLP:journals/iandc/BagnaraMPZ12,
 author       = "Roberto Bagnara and Fred Mesnard and Andrea Pescetti and Enea Zaffanella",
 year         = "2012",
 title        = "A new look at the automatic synthesis of linear ranking functions",
 journal      = "Inf. Comput.",
 volume       = "215",
 pages        = "47--67",
 doi          = "10.1016/j.ic.2012.03.003",
)
@article(Ben-AmramG13jv,
 author       = "Amir M. Ben-Amram and Samir Genaim",
 year         = "2014",
 title        = "Ranking Functions for Linear-Constraint Loops",
 journal      = "Journal of the ACM",
 note         = "Accepted",
)
@article(Ben-AmramGM:toplas2012,
 author       = "Amir M. Ben-Amram and Samir Genaim and Abu Naser Masud",
 year         = "2012",
 title        = "On the Termination of Integer Loops",
 journal      = "ACM Trans. Program. Lang. Syst.",
 volume       = "34",
 number       = "4",
 pages        = "16:1--16:24",
 doi          = "10.1145/2400676.2400679",
)
@techreport(BIKtacas2012jv,
 author       = "Marius Bozga and Radu Iosif and Filip Konecn{\'y}",
 year         = "2014",
 title        = "Deciding Conditional Termination",
 type         = "Technical Report",
 url          = "http://arxiv.org/abs/1302.2762",
)
@incollection(BMS:LexLinear,
 author       = "Aaron Bradley and Zohar Manna and Henny Sipma",
 year         = "2005",
 title        = "Linear Ranking with Reachability",
 editor       = "Kousha Etessami and Sriram Rajamani",
 booktitle    = "Computer Aided Verification",
 series       = "Lecture Notes in Computer Science",
 volume       = "3576",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "247--250",
 doi          = "10.1007/11513988\_48",
)
@inproceedings(BMS:Polyranking,
 author       = "Aaron R. Bradley and Zohar Manna and Henny B. Sipma",
 year         = "2005",
 title        = "The Polyranking Principle",
 editor       = "Lu\'{\i }s Caires and Giuseppe F. Italiano and Lu\'{\i }s Monteiro and Catuscia Palamidessi and Moti Yung",
 booktitle    = "Proc. 32nd International Colloquium on , Languages and Programming",
 series       = "Lecture Notes in Computer Science",
 volume       = "3580",
 publisher    = "Springer Verlag",
 pages        = "1349--1361",
 doi          = "10.1007/11523468\_109",
)
@inproceedings(DBLP:conf/cav/BrockschmidtCF13,
 author       = "Marc Brockschmidt and Byron Cook and Carsten Fuhs",
 year         = "2013",
 title        = "Better Termination Proving through Cooperation",
 editor       = "Natasha Sharygina and Helmut Veith",
 booktitle    = "Computer Aided Verification, CAV 2013",
 series       = "Lecture Notes in Computer Science",
 volume       = "8044",
 publisher    = "Springer",
 pages        = "413--429",
 doi          = "10.1007/978-3-642-39799-8\_28",
)
@inproceedings(CS:01,
 author       = "Michael Col{\'o}n and Henny Sipma",
 year         = "2001",
 title        = "Synthesis of Linear Ranking Functions",
 booktitle    = "7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
 series       = "Lecture Notes in Computer Science",
 volume       = "2031",
 publisher    = "Springer",
 pages        = "67--81",
 doi          = "10.1007/3-540-45319-9\_6",
)
@inproceedings(cookGLRS2008,
 author       = "Byron Cook and Sumit Gulwani and Tal Lev-Ami and Andrey Rybalchenko and Mooly Sagiv",
 year         = "2008",
 title        = "Proving conditional termination",
 booktitle    = "Computer Aided Verification, CAV'08",
 series       = "Lecture Notes in Computer Science",
 volume       = "5123",
 publisher    = "Springer",
 pages        = "328--340",
 doi          = "10.1007/978-3-540-70545-1\_32",
)
@inproceedings(CPR06,
 author       = "Byron Cook and Andreas Podelski and Andrey Rybalchenko",
 year         = "2006",
 title        = "Termination proofs for systems code",
 editor       = "Michael I. Schwartzbach and Thomas Ball",
 booktitle    = "Programming Language Design and Implementation, PLDI'06",
 publisher    = "ACM",
 pages        = "415--426",
 doi          = "10.1145/1133981.1134029",
)
@inproceedings(DBLP:conf/tacas/CookSZ13,
 author       = "Byron Cook and Abigail See and Florian Zuleger",
 year         = "2013",
 title        = "Ramsey vs. Lexicographic Termination Proving",
 editor       = "Nir Piterman and Scott A. Smolka",
 booktitle    = "Tools and Algorithms for the Construction and Analysis of Systems,TACAS 2013",
 series       = "Lecture Notes in Computer Science",
 volume       = "7795",
 publisher    = "Springer",
 pages        = "47--61",
 doi          = "10.1007/978-3-642-36742-7\_4",
)
@inproceedings(CousotHalbwachs:1978,
 author       = "Patrick Cousot and Nicholas Halbwachs",
 year         = "1978",
 title        = "Automatic Discovery of Linear Restraints Among Variables of a Program",
 booktitle    = "Conference Record of the Fifth annual {ACM} Symposium on Principles of Programming Languages",
 organization = "ACM",
 publisher    = "ACM",
 pages        = "84--96",
 doi          = "10.1145/512760.512770",
)
@misc(demri-esslli2010,
 author       = "St{\'e}phane Demri",
 year         = "2011",
 title        = "Decidable Problems for Counter Systems",
 url          = "http://www.lsv.ens-cachan.fr/~demri/esslli2010-lecture-notes.pdf",
 note         = "Revised lecture notes from a course at ESSLLI 2010, Copenhagen",
)
@incollection(Esparza98,
 author       = "Javier Esparza",
 year         = "1998",
 title        = "Decidability and Complexity of {P}etri Net Problems---An Introduction",
 editor       = "Wolfgang Reisig and Grzegorz Rozenberg",
 booktitle    = "Lectures on {P}etri Nets, Vol. {I}: Basic Models",
 series       = "LNCS",
 volume       = "1491",
 publisher    = "Springer-Verlag (New York)",
 address      = "Dagstuhl, Germany",
 pages        = "374--428",
 doi          = "10.1007/3-540-65306-6\_20",
)
@techreport(Esparza94,
 author       = "Javier Esparza and Mogens Nielsen",
 year         = "1994",
 title        = "Decidability Issues for Petri Nets",
 type         = "Technical Report",
 number       = "RS-94-8",
 institution  = "BRICS, Department of Computer Science, University of Aarhus",
)
@phdthesis(Hack79thesis,
 author       = "Michel H. T. Hack",
 year         = "1979",
 booktitle    = "Decidability questions for {Petri} Nets",
 school       = "MIT",
)
@incollection(harris2011alternation,
 author       = "William R Harris and Akash Lal and Aditya V Nori and Sriram K Rajamani",
 year         = "2011",
 title        = "Alternation for termination",
 booktitle    = "Static Analysis Symposium, SAS 2011",
 series       = "LNCS",
 volume       = "6337",
 publisher    = "Springer",
 pages        = "304--319",
 doi          = "10.1007/978-3-642-15769-1\_19",
)
@incollection(HeizmannHLP:ATVA2013,
 author       = "Matthias Heizmann and Jochen Hoenicke and Jan Leike and Andreas Podelski",
 year         = "2013",
 title        = "Linear Ranking for Linear Lasso Programs",
 editor       = "Dang Hung and Mizuhito Ogawa",
 booktitle    = "Automated Technology for Verification and Analysis",
 series       = "Lecture Notes in Computer Science",
 volume       = "8172",
 publisher    = "Springer International Publishing",
 pages        = "365--380",
 doi          = "10.1007/978-3-319-02444-8\_26",
)
@book(Jo:97,
 author       = "Neil D. Jones",
 year         = "1997",
 booktitle    = "Computability and Complexity From a Programming Perspective",
 series       = "Foundations of Computing Series",
 publisher    = "{MIT} {P}ress",
)
@article(KM69,
 author       = "Richard M Karp and Raymond E Miller",
 year         = "1969",
 title        = "Parallel program schemata",
 journal      = "Journal of Computer and system Sciences",
 volume       = "3",
 number       = "2",
 pages        = "147--195",
 doi          = "10.1016/S0022-0000(69)80011-5",
)
@inproceedings(LarrazORR13,
 author       = "Daniel Larraz and Albert Oliveras and Enric Rodr\'{\i }guez-Carbonell and Albert Rubio",
 year         = "2013",
 title        = "Proving termination of imperative programs using {Max-SMT}",
 booktitle    = "Formal Methods in Computer-Aided Design, FMCAD 2013",
 publisher    = "IEEE",
 pages        = "218--225",
 doi          = "10.1109/FMCAD.2013.6679413",
)
@inproceedings(Leroux:2011:VAS,
 author       = "J{\'e}r\^{o}me Leroux",
 year         = "2011",
 title        = "{V}ector {A}ddition {S}ystem Reachability Problem: A Short Self-contained Proof",
 booktitle    = "Proceedings of the 38th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages",
 series       = "POPL '11",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "307--316",
 doi          = "10.1145/1926385.1926421",
)
@techreport(Lipton76,
 author       = "Richard J. Lipton",
 year         = "1976",
 title        = "The Reachability Problem Requires Exponential Space",
 type         = "Technical Report",
 number       = "63",
 institution  = "Yale University",
)
@article(MS:08,
 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      = "TPLP",
 volume       = "8",
 number       = "1",
 pages        = "111--119",
 doi          = "10.1017/S1471068407003122",
)
@inproceedings(OuaknineWorrell:SODA2014,
 author       = "Jo{\"e}l Ouaknine and James Worrell",
 year         = "2014",
 title        = "Positivity problems for low-order linear recurrence sequences",
 booktitle    = "Proceedings of the Twenty-Fifth Annual ACM-SIAM Symposium on Discrete Algorithms",
 series       = "SODA '14",
 publisher    = "SIAM",
 doi          = "10.1137/1.9781611973402.27",
)
@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(PR2007armc,
 author       = "Andreas Podelski and Andrey Rybalchenko",
 year         = "2007",
 title        = "{ARMC}: the logical choice for software model checking with abstraction refinement",
 booktitle    = "Practical Aspects of Declarative Languages",
 series       = "LNCS",
 volume       = "4354",
 publisher    = "Springer",
 pages        = "245--259",
 doi          = "10.1007/978-3-540-69611-7\_16",
)
@inproceedings(SohnVanGelder:91,
 author       = "Kirack Sohn and Allen {Van Gelder}",
 year         = "1991",
 title        = "Termination detection in logic programs using argument sizes (extended abstract)",
 booktitle    = "Proceedings of the Tenth {ACM} {SIGACT-SIGMOD-SOGART} Symposium on Principles of Database Systems (PODS), May 1991, Denver, Colorado",
 publisher    = "ACM Press",
 pages        = "216--226",
 doi          = "10.1145/113413.113433",
)