@Article{Domenech19,
author = {Jes{\'{u}}s J. Dom{\'{e}}nech and John P. Gallagher and Samir Genaim},
journal = {Theory Pract. Log. Program.},
title = {Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis},
year = {2019},
number = {5-6},
pages = {990--1005},
volume = {19},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/tplp/DomenechGG19.bib},
comment = {iRankFinder
https://github.com/costa-group/iRankFinder},
doi = {10.1017/S1471068419000310},
file = {:/home/paradyx/MA/literatur/Domenech-control-flow-refinement-by-partial-evaluation-and-its-application-to-termination-and-cost-analysis.pdf:PDF},
groups = {Partial Evaluation},
qualityassured = {qualityAssured},
ranking = {rank5},
relevance = {relevant},
timestamp = {Thu, 13 Feb 2020 14:39:32 +0100},
url = {https://doi.org/10.1017/S1471068419000310},
}
@Article{brockschmidt2016acm,
author = {Marc Brockschmidt and Fabian Emmes and Stephan Falke and Carsten Fuhs and J{\"{u}}rgen Giesl},
journal = {{ACM} Trans. Program. Lang. Syst.},
title = {Analyzing Runtime and Size Complexity of Integer Programs},
year = {2016},
number = {4},
pages = {13:1--13:50},
volume = {38},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/toplas/BrockschmidtE0F16.bib},
comment = {KOAT Paper},
file = {:/home/paradyx/MA/literatur/brockschmidt2016.pdf:PDF},
groups = {KoAT},
priority = {prio2},
ranking = {rank4},
timestamp = {Tue, 03 Jan 2017 13:49:06 +0100},
url = {http://dl.acm.org/citation.cfm?id=2866575},
}
@InProceedings{DBLP:conf/concur/NeumannO020,
author = {Eike Neumann and Jo{\"{e}}l Ouaknine and James Worrell},
booktitle = {31st International Conference on Concurrency Theory, {CONCUR} 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)},
title = {On Ranking Function Synthesis and Termination for Polynomial Programs},
year = {2020},
editor = {Igor Konnov and Laura Kov{\'{a}}cs},
pages = {15:1--15:15},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
series = {LIPIcs},
volume = {171},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/concur/NeumannO020.bib},
doi = {10.4230/LIPIcs.CONCUR.2020.15},
priority = {prio2},
timestamp = {Mon, 21 Dec 2020 13:23:22 +0100},
url = {https://doi.org/10.4230/LIPIcs.CONCUR.2020.15},
}
@InProceedings{DBLP:conf/pldi/GulwaniJK09,
author = {Sumit Gulwani and Sagar Jain and Eric Koskinen},
booktitle = {Proceedings of the 2009 {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2009, Dublin, Ireland, June 15-21, 2009},
title = {Control-flow refinement and progress invariants for bound analysis},
year = {2009},
editor = {Michael Hind and Amer Diwan},
pages = {375--385},
publisher = {{ACM}},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/pldi/GulwaniJK09.bib},
comment = {Referenced by Doménech for CFR},
doi = {10.1145/1542476.1542518},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
url = {https://doi.org/10.1145/1542476.1542518},
}
@InProceedings{DBLP:conf/cav/SharmaDDA11,
author = {Rahul Sharma and Isil Dillig and Thomas Dillig and Alex Aiken},
booktitle = {Computer Aided Verification - 23rd International Conference, {CAV} 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings},
title = {Simplifying Loop Invariant Generation Using Splitter Predicates},
year = {2011},
editor = {Ganesh Gopalakrishnan and Shaz Qadeer},
pages = {703--719},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6806},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cav/SharmaDDA11.bib},
comment = {How to compute the splitter predicate:
The weakest precondition computation step in the algorithm is implemented by using the quantifier
elimination capabilities of Mistral. More specifically, to compute the weakest precondition of C with
respect to code fragment B, we first convert B to single static assignment (SSA) form [9].},
doi = {10.1007/978-3-642-22110-1_57},
file = {:/home/paradyx/MA/literatur/cav11.pdf:PDF},
ranking = {rank5},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
url = {https://doi.org/10.1007/978-3-642-22110-1_57},
}
@Article{bagnara2008socp,
author = {Roberto Bagnara and Patricia M. Hill and Enea Zaffanella},
journal = {Sci. Comput. Program.},
title = {The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems},
year = {2008},
number = {1-2},
pages = {3--21},
volume = {72},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/scp/BagnaraHZ08.bib},
comment = {Projection of linear constraints},
doi = {10.1016/j.scico.2007.08.001},
file = {:/home/paradyx/MA/literatur/bagnara-the-parma-polyhedra-library.pdf:PDF},
groups = {Tools, Polyhedra, Octagons, Boxes},
timestamp = {Wed, 17 Feb 2021 21:55:47 +0100},
url = {https://doi.org/10.1016/j.scico.2007.08.001},
}
@InProceedings{DBLP:journals/corr/abs-1908-07189,
author = {John P. Gallagher},
booktitle = {Proceedings Seventh International Workshop on Verification and Program Transformation, VPT@Programming 2019, Genova, Italy, 2nd April 2019},
title = {Polyvariant Program Specialisation with Property-based Abstraction},
year = {2019},
editor = {Alexei Lisitsa and Andrei P. Nemytykh},
pages = {34--48},
series = {{EPTCS}},
volume = {299},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/corr/abs-1908-07189.bib},
comment = {partial evaluation on Constraint Horn Clauses (CHC) programs},
doi = {10.4204/EPTCS.299.6},
priority = {prio1},
relevance = {relevant},
timestamp = {Fri, 27 Dec 2019 21:15:10 +0100},
url = {https://doi.org/10.4204/EPTCS.299.6},
}
@InProceedings{DBLP:conf/sas/AliasDFG10,
author = {Christophe Alias and Alain Darte and Paul Feautrier and Laure Gonnord},
booktitle = {Static Analysis - 17th International Symposium, {SAS} 2010, Perpignan, France, September 14-16, 2010. Proceedings},
title = {Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs},
year = {2010},
editor = {Radhia Cousot and Matthieu Martel},
pages = {117--133},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6337},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/sas/AliasDFG10.bib},
comment = {Introduced Ranking functions
with Definitions},
doi = {10.1007/978-3-642-15769-1\_8},
file = {:/home/paradyx/MA/literatur/alias-rankingfunctions-2010.pdf:PDF},
ranking = {rank4},
timestamp = {Tue, 14 May 2019 10:00:52 +0200},
url = {https://doi.org/10.1007/978-3-642-15769-1\_8},
}
@InProceedings{giesl2014ijcar,
author = {J{\"{u}}rgen Giesl and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Carsten Otto and Martin Pl{\"{u}}cker and Peter Schneider{-}Kamp and Thomas Str{\"{o}}der and Stephanie Swiderski and Ren{\'{e}} Thiemann},
booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 19-22, 2014. Proceedings},
title = {Proving Termination of Programs Automatically with AProVE},
year = {2014},
editor = {St{\'{e}}phane Demri and Deepak Kapur and Christoph Weidenbach},
pages = {184--191},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8562},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cade/GieslBEFFOPSSST14.bib},
doi = {10.1007/978-3-319-08587-6_13},
file = {Full Conference:/home/paradyx/MA/literatur/ijcar2014full.pdf:PDF;Paper Only:/home/paradyx/MA/literatur/giesl2014ijcar.pdf:PDF},
groups = {AProVE, Complexity Tools},
timestamp = {Sat, 05 Sep 2020 18:05:20 +0200},
url = {https://doi.org/10.1007/978-3-319-08587-6_13},
}
@Article{giesl2017aprove,
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 Peter Schneider{-}Kamp and Thomas Str{\"{o}}der and Stephanie Swiderski and Ren{\'{e}} Thiemann},
journal = {J. Autom. Reason.},
title = {Analyzing Program Termination and Complexity Automatically with AProVE},
year = {2017},
number = {1},
pages = {3--31},
volume = {58},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/jar/GieslABEFFHOPSS17.bib},
doi = {10.1007/s10817-016-9388-y},
file = {:/home/paradyx/MA/literatur/giesl-approve-2017.pdf:PDF},
groups = {AProVE, Complexity Tools},
timestamp = {Sat, 05 Sep 2020 17:51:29 +0200},
url = {https://doi.org/10.1007/s10817-016-9388-y},
}
@InProceedings{:wq,
author = {Amir M. Ben{-}Amram and Samir Genaim},
booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
title = {On Multiphase-Linear Ranking Functions},
year = {2017},
editor = {Rupak Majumdar and Viktor Kuncak},
pages = {601--620},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10427},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cav/Ben-AmramG17.bib},
doi = {10.1007/978-3-319-63390-9\_32},
file = {:/home/paradyx/MA/literatur/ben-amram-rankingfunctions-2017.pdf:PDF},
timestamp = {Mon, 03 Jan 2022 22:13:45 +0100},
url = {https://doi.org/10.1007/978-3-319-63390-9\_32},
}
@Article{meyer2021tacas,
author = {Fabian Meyer and Marcel Hark and Jürgen Giesl},
journal = {Tools and Algorithmsfor the Constructionand Analysis of Systems},
title = {Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes},
year = {2021},
file = {:/home/paradyx/MA/literatur/TACAS2021.pdf:PDF},
groups = {KoAT},
url = {https://verify.rwth-aachen.de/giesl/papers/TACAS2021.pdf},
}
@Book{billingsley2011,
author = {Billingsley, Patrick},
publisher = {Wiley},
title = {Probability and measure},
year = {2011},
address = {New York},
edition = {3. ed., anniversary ed.},
isbn = {9781118122372},
series = {Wiley series in probability and mathematical statistics},
file = {:/home/paradyx/MA/literatur/billingsley.pdf:PDF},
groups = {Probability},
language = {eng},
ranking = {rank5},
url = {https://katalog.ub.rwth-aachen.de/permalink/49HBZ_UBA/l7n8rv/alma991005910089706448},
}
@Article{meyer20arxiv,
author = {Fabian Meyer and Marcel Hark and J{\"{u}}rgen Giesl},
journal = {CoRR},
title = {Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes},
year = {2020},
volume = {abs/2010.06367},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/corr/abs-2010-06367.bib},
eprint = {2010.06367},
eprinttype = {arXiv},
file = {:/home/paradyx/MA/literatur/meyer20arxiv.pdf:PDF},
groups = {KoAT},
timestamp = {Tue, 20 Oct 2020 15:08:10 +0200},
url = {https://arxiv.org/abs/2010.06367},
}
@InProceedings{brockschmidt2014tacas,
author = {Marc Brockschmidt and Fabian Emmes and Stephan Falke and Carsten Fuhs and Jürgen Giesl},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, {TACAS} 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2014, Grenoble, France, April 5-13, 2014. Proceedings},
title = {Alternating Runtime and Size Complexity Analysis of Integer Programs},
year = {2014},
editor = {Erika Ábrahám and Klaus Havelund},
pages = {140--155},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8413},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/tacas/BrockschmidtEFFG14.bib},
doi = {10.1007/978-3-642-54862-8_10},
file = {KoAT 1 Basepaper:/home/paradyx/MA/literatur/brockschmidt2014.pdf:PDF},
groups = {KoAT},
timestamp = {Sat, 05 Sep 2020 18:01:53 +0200},
url = {https://doi.org/10.1007/978-3-642-54862-8_10},
}
@InProceedings{montoya2014aplas,
author = {Antonio Flores{-}Montoya and Reiner Hähnle},
booktitle = {Programming Languages and Systems - 12th Asian Symposium, {APLAS} 2014, Singapore, November 17-19, 2014, Proceedings},
title = {Resource Analysis of Complex Programs with Cost Equations},
year = {2014},
editor = {Jacques Garrigue},
pages = {275--295},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8858},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/aplas/Flores-MontoyaH14.bib},
doi = {10.1007/978-3-319-12736-1_15},
file = {Full Conference:/home/paradyx/MA/literatur/aplas2014full.pdf:PDF;Paper Only:/home/paradyx/MA/literatur/montoyahähnle2014aplas.pdf:PDF},
groups = {CoFloCo, Complexity Tools},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
url = {https://doi.org/10.1007/978-3-319-12736-1_15},
}
@PhdThesis{montoya2017phd,
author = {Antonio Flores{-}Montoya},
school = {Darmstadt University of Technology, Germany},
title = {Cost Analysis of Programs Based on the Refinement of Cost Relations},
year = {2017},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/phd/dnb/Montoya17.bib},
groups = {Complexity Tools},
timestamp = {Sat, 17 Jul 2021 09:03:08 +0200},
url = {http://tuprints.ulb.tu-darmstadt.de/6746/},
urn = {urn:nbn:de:tuda-tuprints-67465},
}
@Article{domenech2019arxiv,
author = {Jesús J. Doménech and John P. Gallagher and Samir Genaim},
journal = {CoRR},
title = {Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis},
year = {2019},
volume = {abs/1907.12345},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/corr/abs-1907-12345.bib},
eprint = {1907.12345},
eprinttype = {arXiv},
file = {Paper Only:/home/paradyx/MA/literatur/domenech2019arxiv.pdf:PDF},
groups = {Partial Evaluation},
timestamp = {Thu, 01 Aug 2019 08:59:33 +0200},
url = {http://arxiv.org/abs/1907.12345},
}
@Misc{irankfinder-github,
howpublished = {\url{https://github.com/costa-group/iRankFinder}},
title = {iRankFinder},
year = {2020},
commit = {2dd473018abf30c6920ace54ae675dc06295e1e4},
groups = {Partial Evaluation},
journal = {GitHub repository},
publisher = {GitHub},
}
@InProceedings{irankfinder2018wst,
author = {Jesús J. Doménech and Samir Genaim},
booktitle = {Proceedings of the 16th International Workshop on Termination},
title = {iRankFinder},
year = {2018},
address = {Oxford, UK},
editor = {Salvador Lucas},
month = jul,
pages = {83},
file = {Full Proceedings:/home/paradyx/MA/literatur/wst2018proceedings.pdf:PDF},
groups = {Partial Evaluation, Complexity Tools},
url = {https://wst2018.webs.upv.es/index.html},
}
@InProceedings{giesl2022wst,
author = {Jürgen Giesl and Nils Lommen and Marcel Hark and Fabian Meyer},
booktitle = {Proceedings of the 19th International Workshop on Termination},
title = {Improved Automatic Complexity Analysis of Integer Programs},
year = {2022},
address = {Haifa, Israel},
editor = {Cynthia Kop},
month = aug,
pages = {83},
file = {Full Proceedings:/home/paradyx/MA/literatur/wst2018proceedings.pdf:PDF},
groups = {KoAT},
url = {https://wst2018.webs.upv.es/index.html},
}
@InProceedings{frohn2022ijcar,
author = {Florian Frohn and Jürgen Giesl},
booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings},
title = {Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)},
year = {2022},
editor = {Jasmin Blanchette and Laura Kovàcs and Dirk Pattinson},
pages = {712--722},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {13385},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cade/FrohnG22.bib},
doi = {10.1007/978-3-031-10769-6_41},
file = {Full Conference:/home/paradyx/MA/literatur/ijcar2022full.pdf:PDF},
groups = {LoAT},
timestamp = {Mon, 24 Oct 2022 16:36:35 +0200},
url = {https://doi.org/10.1007/978-3-031-10769-6_41},
}
@Misc{foo,
author = {Jes{\'{u}}s J. Dom{\'{e}}nech and Samir Genaim and John P. Gallagher},
month = jul,
title = {Control-Flow Renementvia Partial Evaluation},
year = {2018},
file = {Slides:/home/paradyx/MA/literatur/domenech2018slides.pdf:PDF},
groups = {Partial Evaluation},
ranking = {rank2},
}
@InProceedings{termcomp2015,
author = {J{\"{u}}rgen Giesl and Fr{\'{e}}d{\'{e}}ric Mesnard and Albert Rubio and Ren{\'{e}} Thiemann and Johannes Waldmann},
booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
title = {Termination Competition (termCOMP 2015)},
year = {2015},
editor = {Amy P. Felty and Aart Middeldorp},
pages = {105--108},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {9195},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cade/GieslMRTW15.bib},
doi = {10.1007/978-3-319-21401-6_6},
file = {Full Conference:/home/paradyx/MA/literatur/cade2015full.pdf:PDF},
groups = {Competitions},
timestamp = {Wed, 25 Sep 2019 18:19:14 +0200},
url = {https://doi.org/10.1007/978-3-319-21401-6_6},
}
@InProceedings{termcomp2019,
author = {J{\"{u}}rgen Giesl and Albert Rubio and Christian Sternagel and Johannes Waldmann and Akihisa Yamada},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {III}},
title = {The Termination and Complexity Competition},
year = {2019},
editor = {Dirk Beyer and Marieke Huisman and Fabrice Kordon and Bernhard Steffen},
pages = {156--166},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {11429},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/tacas/GieslRSWY19.bib},
doi = {10.1007/978-3-030-17502-3_10},
file = {Full Conference:/home/paradyx/MA/literatur/tacas2019full.pdf:PDF},
groups = {Competitions},
timestamp = {Fri, 09 Apr 2021 18:45:37 +0200},
url = {https://doi.org/10.1007/978-3-030-17502-3_10},
}
@InProceedings{alarcon2017muterm,
author = {Beatriz Alarc{\'{o}}n and Ra{\'{u}}l Guti{\'{e}}rrez and Jos{\'{e}} Iborra and Salvador Lucas},
booktitle = {Proceedings of the Sixth Spanish Conference on Programming and Languages, {PROLE} 2006, Sitges, Barcelona, Spain, October 4-6, 2006},
title = {Proving Termination of Context-Sensitive Rewriting with {MU-TERM}},
year = {2006},
editor = {Paqui Lucio and Fernando Orejas},
pages = {105--115},
publisher = {Elsevier},
series = {Electronic Notes in Theoretical Computer Science},
volume = {188},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/entcs/AlarconGIL07.bib},
doi = {10.1016/j.entcs.2007.05.041},
groups = {Complexity Tools},
timestamp = {Tue, 31 Jan 2023 15:28:53 +0100},
url = {https://doi.org/10.1016/j.entcs.2007.05.041},
}
@Online{termcomp2022url,
groups = {Competitions},
title = {Termination Competition 2022},
url = {https://termination-portal.org/wiki/Termination_Competition_2022},
urldate = {2023-05-09},
year = {2022},
}
@InProceedings{frohn2017ifm,
author = {Florian Frohn and J{\"{u}}rgen Giesl},
booktitle = {Integrated Formal Methods - 13th International Conference, {IFM} 2017, Turin, Italy, September 20-22, 2017, Proceedings},
title = {Complexity Analysis for Java with AProVE},
year = {2017},
editor = {Nadia Polikarpova and Steve A. Schneider},
pages = {85--101},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {10510},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/ifm/FrohnG17.bib},
doi = {10.1007/978-3-319-66845-1_6},
file = {Full Conference:/home/paradyx/MA/literatur/ifm2017full.pdf:PDF},
groups = {AProVE},
timestamp = {Fri, 07 Aug 2020 17:57:32 +0200},
url = {https://doi.org/10.1007/978-3-319-66845-1_6},
}
@Article{giesel2011rsst,
author = {J{\"{u}}rgen Giesl and Matthias Raffelsieper and Peter Schneider{-}Kamp and Stephan Swiderski and Ren{\'{e}} Thiemann},
journal = {{ACM} Trans. Program. Lang. Syst.},
title = {Automated termination proofs for haskell by term rewriting},
year = {2011},
number = {2},
pages = {7:1--7:39},
volume = {33},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/toplas/GieslRSST11.bib},
doi = {10.1145/1890028.1890030},
groups = {AProVE},
timestamp = {Wed, 25 Sep 2019 17:52:01 +0200},
url = {https://doi.org/10.1145/1890028.1890030},
}
@Article{giesl2022arxiv,
author = {J{\"{u}}rgen Giesl and Nils Lommen and Marcel Hark and Fabian Meyer},
journal = {CoRR},
title = {Improving Automatic Complexity Analysis of Integer Programs},
year = {2022},
volume = {abs/2202.01769},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/corr/abs-2202-01769.bib},
eprint = {2202.01769},
eprinttype = {arXiv},
file = {:/home/paradyx/MA/literatur/giesl2022arxiv.pdf:PDF},
groups = {KoAT},
timestamp = {Wed, 09 Feb 2022 15:43:35 +0100},
url = {https://arxiv.org/abs/2202.01769},
}
@InProceedings{giesl2022lncs,
author = {J{\"{u}}rgen Giesl and Nils Lommen and Marcel Hark and Fabian Meyer},
booktitle = {The Logic of Software. {A} Tasting Menu of Formal Methods - Essays Dedicated to Reiner H{\"{a}}hnle on the Occasion of His 60th Birthday},
title = {Improving Automatic Complexity Analysis of Integer Programs},
year = {2022},
editor = {Wolfgang Ahrendt and Bernhard Beckert and Richard Bubel and Einar Broch Johnsen},
pages = {193--228},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {13360},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/birthday/GieslLHM20.bib},
doi = {10.1007/978-3-031-08166-8_10},
file = {Full Conference:/home/paradyx/MA/literatur/thelogicofsoftware2022full.pdf:PDF},
groups = {KoAT},
timestamp = {Tue, 18 Oct 2022 22:17:02 +0200},
url = {https://doi.org/10.1007/978-3-031-08166-8_10},
}
@Misc{kraaikamp2005modern,
author = {C. Kraaikamp and F.M. Dekking and H.P. Lopuhaä and L.E. Meester},
title = {A Modern Introduction to Probability and Statistics Understanding Why and How},
year = {2005},
doi = {https://doi.org/10.1007/1-84628-168-7},
file = {Full Book:/home/paradyx/MA/literatur/kraaikamp2005modern.pdf:PDF},
groups = {Probability},
publisher = {springer publication},
}
@Book{vanderbei2020lp,
author = {Robert J. Vanderbei},
publisher = {Springer},
title = {Linear Programming Foundations and Extensions},
year = {2020},
edition = {5},
isbn = {978-3-030-39414-1},
series = {International Series in Operations Research and Management Science},
volume = {285},
doi = {https://doi.org/10.1007/978-3-030-39415-8},
file = {Full Book:/home/paradyx/MA/literatur/vanderbei2020lp.pdf:PDF},
groups = {Linear Programming},
timestamp = {Mon, 22 Jul 2019 16:40:55 +0200},
}
@Book{pan2023lpcomputation,
author = {Ping{-}Qi Pan},
publisher = {Springer},
title = {Linear Programming Computation, Second Edition},
year = {2023},
isbn = {978-981-19-0146-1},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/books/sp/Pan23.bib},
doi = {10.1007/978-981-19-0147-8},
file = {Full Book:/home/paradyx/MA/literatur/pan2023lpcomputation.pdf:PDF},
groups = {Linear Programming},
timestamp = {Mon, 16 Jan 2023 12:10:53 +0100},
url = {https://doi.org/10.1007/978-981-19-0147-8},
}
@Article{bagnara2005convexpolyhedron,
author = {Roberto Bagnara and Patricia M. Hill and Enea Zaffanella},
journal = {Formal Aspects Comput.},
title = {Not necessarily closed convex polyhedra and the double description method},
year = {2005},
number = {2},
pages = {222--257},
volume = {17},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/fac/BagnaraHZ05.bib},
doi = {10.1007/s00165-005-0061-1},
file = {:/home/paradyx/MA/literatur/bagnara2005convexpolyhedron.pdf:PDF},
groups = {Polyhedra, Octagons, Boxes},
timestamp = {Mon, 09 May 2022 16:20:12 +0200},
url = {https://doi.org/10.1007/s00165-005-0061-1},
}
@InProceedings{mine2001wcre,
author = {Antoine Min{\'{e}}},
booktitle = {Proceedings of the Eighth Working Conference on Reverse Engineering, WCRE'01, Stuttgart, Germany, October 2-5, 2001},
title = {The Octagon Abstract Domain},
year = {2001},
editor = {Elizabeth Burd and Peter Aiken and Rainer Koschke},
pages = {310},
publisher = {{IEEE} Computer Society},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/wcre/Mine01.bib},
doi = {10.1109/WCRE.2001.957836},
file = {:/home/paradyx/MA/literatur/mine2001wcre.pdf:PDF},
groups = {Polyhedra, Octagons, Boxes},
timestamp = {Fri, 24 Mar 2023 00:04:44 +0100},
url = {https://doi.org/10.1109/WCRE.2001.957836},
}
@Article{mine2007arxiv,
author = {Antoine Min{\'{e}}},
journal = {CoRR},
title = {The Octagon Abstract Domain},
year = {2007},
volume = {abs/cs/0703084},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/corr/abs-cs-0703084.bib},
eprint = {cs/0703084},
eprinttype = {arXiv},
file = {:/home/paradyx/MA/literatur/mine2007arxiv.pdf:PDF},
groups = {Polyhedra, Octagons, Boxes},
timestamp = {Mon, 13 Aug 2018 16:47:22 +0200},
url = {http://arxiv.org/abs/cs/0703084},
}
@Article{mine2006hosc,
author = {Antoine Min{\'{e}}},
journal = {High. Order Symb. Comput.},
title = {The octagon abstract domain},
year = {2006},
number = {1},
pages = {31--100},
volume = {19},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/lisp/Mine06.bib},
doi = {10.1007/s10990-006-8609-1},
file = {:/home/paradyx/MA/literatur/mine2006hosc.pdf:PDF},
groups = {Polyhedra, Octagons, Boxes},
timestamp = {Thu, 05 Mar 2020 12:04:59 +0100},
url = {https://doi.org/10.1007/s10990-006-8609-1},
}
@InProceedings{truchet2010synacs,
author = {Charlotte Truchet and Marie Pelleau and Fr{\'{e}}d{\'{e}}ric Benhamou},
booktitle = {12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, {SYNASC} 2010, Timisoara, Romania, 23-26 September 2010},
title = {Abstract Domains for Constraint Programming, with the Example of Octagons},
year = {2010},
editor = {Tetsuo Ida and Viorel Negru and Tudor Jebelean and Dana Petcu and Stephen M. Watt and Daniela Zaharie},
pages = {72--79},
publisher = {{IEEE} Computer Society},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/synasc/TruchetPB10.bib},
doi = {10.1109/SYNASC.2010.69},
file = {:/home/paradyx/MA/literatur/truchet2010synacs.pdf:PDF},
groups = {Polyhedra, Octagons, Boxes},
timestamp = {Fri, 24 Mar 2023 00:01:58 +0100},
url = {https://doi.org/10.1109/SYNASC.2010.69},
}
@InCollection{karp2010reducibility,
author = {Richard M. Karp},
booktitle = {50 Years of Integer Programming 1958-2008 - From the Early Years to the State-of-the-Art},
publisher = {Springer},
title = {Reducibility Among Combinatorial Problems},
year = {2010},
editor = {Michael J{\"{u}}nger and Thomas M. Liebling and Denis Naddef and George L. Nemhauser and William R. Pulleyblank and Gerhard Reinelt and Giovanni Rinaldi and Laurence A. Wolsey},
pages = {219--241},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/books/daglib/p/Karp10.bib},
doi = {10.1007/978-3-540-68279-0_8},
file = {Old Book:/home/paradyx/MA/literatur/karp1972reducibility.pdf:PDF},
timestamp = {Wed, 14 Nov 2018 10:12:21 +0100},
url = {https://doi.org/10.1007/978-3-540-68279-0\_8},
}
@InProceedings{gulwani2009,
author = {Sumit Gulwani and Sagar Jain and Eric Koskinen},
booktitle = {Proceedings of the 2009 {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation, {PLDI} 2009, Dublin, Ireland, June 15-21, 2009},
title = {Control-flow refinement and progress invariants for bound analysis},
year = {2009},
editor = {Michael Hind and Amer Diwan},
pages = {375--385},
publisher = {{ACM}},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/pldi/GulwaniJK09.bib},
doi = {10.1145/1542476.1542518},
file = {:/home/paradyx/MA/literatur/gulwani2009.pdf:PDF},
groups = {Partial Evaluation},
timestamp = {Fri, 25 Jun 2021 14:48:54 +0200},
url = {https://doi.org/10.1145/1542476.1542518},
}
@InProceedings{gallagher2019eptcs,
author = {John P. Gallagher},
booktitle = {Proceedings Seventh International Workshop on Verification and Program Transformation, VPT@Programming 2019, Genova, Italy, 2nd April 2019},
title = {Polyvariant Program Specialisation with Property-based Abstraction},
year = {2019},
editor = {Alexei Lisitsa and Andrei P. Nemytykh},
pages = {34--48},
series = {{EPTCS}},
volume = {299},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/corr/abs-1908-07189.bib},
doi = {10.4204/EPTCS.299.6},
file = {:/home/paradyx/MA/literatur/gallagher2019eptcs.pdf:PDF},
groups = {Partial Evaluation},
timestamp = {Fri, 03 Jun 2022 08:18:12 +0200},
url = {https://doi.org/10.4204/EPTCS.299.6},
}
@Article{johnson1975,
author = {Johnson, Donald B.},
journal = {SIAM Journal on Computing},
title = {Finding All the Elementary Circuits of a Directed Graph},
year = {1975},
number = {1},
pages = {77-84},
volume = {4},
abstract = {An algorithm is presented which finds all the elementary circuits of a directed graph in time bounded by \$O((n + e)(c + 1))\$ and space bounded by \$O(n + e)\$, where there are n vertices, e edges and c elementary circuits in the graph. The algorithm resembles algorithms by Tiernan and Tarjan, but is faster because it considers each edge at most twice between any one circuit and the next in the output sequence.},
doi = {10.1137/0204007},
eprint = {https://doi.org/10.1137/0204007},
url = {https://doi.org/10.1137/0204007},
}
@Article{puterman1990markov,
author = {Puterman, Martin L.},
journal = {Handbooks in operations research and management science},
title = {Markov decision processes},
year = {1990},
pages = {331--434},
volume = {2},
file = {:/home/paradyx/MA/literatur/putermann1990markov.pdf:PDF},
groups = {Probability},
publisher = {Elsevier},
}
@Book{puterman1994markov,
author = {Puterman, Martin L.},
publisher = {John Wiley \& Sons, Inc},
title = {Markov Decision Processes: Discrete Stochastic Dynamic Programming},
year = {1994},
edition = {1},
isbn = {9780470316887},
series = {Wiley Series in Probability and Statistics},
file = {:/home/paradyx/MA/literatur/puterman1994markov.pdf:PDF},
groups = {Probability},
keywords = {Statistics},
language = {eng},
}
@InProceedings{llvm2kittel,
author = {Stephan Falke and Deepak Kapur and Carsten Sinz},
booktitle = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, {RTA} 2011, May 30 - June 1, 2011, Novi Sad, Serbia},
title = {Termination Analysis of {C} Programs Using Compiler Intermediate Languages},
year = {2011},
editor = {Manfred Schmidt{-}Schau{\ss}},
pages = {41--50},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
series = {LIPIcs},
volume = {10},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/rta/FalkeKS11.bib},
doi = {10.4230/LIPIcs.RTA.2011.41},
groups = {Tools},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
url = {https://doi.org/10.4230/LIPIcs.RTA.2011.41},
}
@Misc{tpdb,
note = {Available at \url{https://termination-portal.org/wiki/TPDB}; Version 11.0 (2019)},
title = {The Termination Problems Data Base},
groups = {Tools},
url = {https://termination-portal.org/wiki/TPDB},
}
@InProceedings{z3,
author = {Leonardo Mendon{\c{c}}a de Moura and Nikolaj S. Bj{\o}rner},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, {TACAS} 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings},
title = {{Z3:} An Efficient {SMT} Solver},
year = {2008},
editor = {C. R. Ramakrishnan and Jakob Rehof},
pages = {337--340},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4963},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/tacas/MouraB08.bib},
doi = {10.1007/978-3-540-78800-3_24},
timestamp = {Mon, 03 Apr 2023 17:23:33 +0200},
url = {https://doi.org/10.1007/978-3-540-78800-3_24},
}
@InProceedings{apron,
author = {Bertrand Jeannet and Antoine Min{\'{e}}},
booktitle = {Computer Aided Verification, 21st International Conference, {CAV} 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings},
title = {Apron: {A} Library of Numerical Abstract Domains for Static Analysis},
year = {2009},
editor = {Ahmed Bouajjani and Oded Maler},
pages = {661--667},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {5643},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cav/JeannetM09.bib},
doi = {10.1007/978-3-642-02658-4_52},
groups = {Polyhedra, Octagons, Boxes},
timestamp = {Tue, 14 May 2019 10:00:43 +0200},
url = {https://doi.org/10.1007/978-3-642-02658-4_52},
}
@InCollection{barwise1977,
author = {Jon Barwise},
booktitle = {HANDBOOK OF MATHEMATICAL LOGIC},
publisher = {Elsevier},
title = {An Introduction to First-Order Logic},
year = {1977},
editor = {Jon Barwise},
pages = {5-46},
series = {Studies in Logic and the Foundations of Mathematics},
volume = {90},
abstract = {Publisher Summary
This chapter discusses the formulas that are certain finite strings of symbols. The “first” in the phrase “first-order logic” is to distinguish this form of logic from stronger logics, such as second-order or weak second-order logic, where certain extralogical notions (set or natural number) are taken as given in advance. The chapter provides information of what can and what cannot be expressed in first-order logic. Most of the examples are taken from the wealth of notions in modern algebra with which most mathematicians have at least a nodding acquaintance. The chapter also discusses many-sorted first-order logic, ω-logic, weak second-order logic, Infinitary logic, Logic with new quantifiers, and abstract model theory.},
doi = {https://doi.org/10.1016/S0049-237X(08)71097-8},
file = {:/home/paradyx/MA/literatur/introductiontofo.pdf:PDF},
issn = {0049-237X},
url = {https://www.sciencedirect.com/science/article/pii/S0049237X08710978},
}
@InProceedings{gurfinkel2010,
author = {Arie Gurfinkel and Sagar Chaki},
booktitle = {Static Analysis - 17th International Symposium, {SAS} 2010, Perpignan, France, September 14-16, 2010. Proceedings},
title = {Boxes: {A} Symbolic Abstract Domain of Boxes},
year = {2010},
editor = {Radhia Cousot and Matthieu Martel},
pages = {287--303},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6337},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/sas/GurfinkelC10.bib},
doi = {10.1007/978-3-642-15769-1_18},
groups = {Polyhedra, Octagons, Boxes},
timestamp = {Mon, 03 Jan 2022 22:21:24 +0100},
url = {https://doi.org/10.1007/978-3-642-15769-1_18},
}
@InCollection{barett2009smt,
author = {Clark W. Barrett and Roberto Sebastiani and Sanjit A. Seshia and Cesare Tinelli},
booktitle = {Handbook of Satisfiability},
publisher = {{IOS} Press},
title = {Satisfiability Modulo Theories},
year = {2009},
editor = {Armin Biere and Marijn Heule and Hans van Maaren and Toby Walsh},
pages = {825--885},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {185},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/series/faia/BarrettSST09.bib},
doi = {10.3233/978-1-58603-929-5-825},
file = {:/home/paradyx/MA/literatur/walsh2009sat.pdf:PDF},
timestamp = {Fri, 06 May 2022 08:00:40 +0200},
url = {https://doi.org/10.3233/978-1-58603-929-5-825},
}
@InProceedings{abraham17smt,
author = {Erika {\'{A}}brah{\'{a}}m and Gereon Kremer},
booktitle = {19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, {SYNASC} 2017, Timisoara, Romania, September 21-24, 2017},
title = {{SMT} Solving for Arithmetic Theories: Theory and Tool Support},
year = {2017},
editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephen M. Watt},
pages = {1--8},
publisher = {{IEEE} Computer Society},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/synasc/AbrahamK17.bib},
doi = {10.1109/SYNASC.2017.00009},
timestamp = {Fri, 24 Mar 2023 00:01:57 +0100},
url = {https://doi.org/10.1109/SYNASC.2017.00009},
}
@Book{walsh2009smt,
editor = {Armin Biere and Marijn Heule and Hans van Maaren and Toby Walsh},
publisher = {{IOS} Press},
title = {Handbook of Satisfiability},
year = {2009},
isbn = {978-1-58603-929-5},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {185},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/series/faia/2009-185.bib},
file = {:/home/paradyx/MA/literatur/walsh2009sat.pdf:PDF},
timestamp = {Fri, 06 May 2022 08:00:40 +0200},
}
@Article{dijkstra1959,
author = {Edsger W. Dijkstra},
journal = {Numerische Mathematik},
title = {A note on two problems in connexion with graphs},
year = {1959},
pages = {269--271},
volume = {1},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/journals/nm/Dijkstra59.bib},
doi = {10.1007/BF01386390},
timestamp = {Mon, 29 Jul 2019 15:59:06 +0200},
url = {https://doi.org/10.1007/BF01386390},
}
@InProceedings{kremer2016lncs,
author = {Gereon Kremer and Florian Corzilius and Erika {\'{A}}brah{\'{a}}m},
booktitle = {Computer Algebra in Scientific Computing - 18th International Workshop, {CASC} 2016, Bucharest, Romania, September 19-23, 2016, Proceedings},
title = {A Generalised Branch-and-Bound Approach and Its Application in {SAT} Modulo Nonlinear Integer Arithmetic},
year = {2016},
editor = {Vladimir P. Gerdt and Wolfram Koepf and Werner M. Seiler and Evgenii V. Vorozhtsov},
pages = {315--335},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {9890},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/casc/KremerCA16.bib},
doi = {10.1007/978-3-319-45641-6_21},
timestamp = {Thu, 23 Sep 2021 11:48:04 +0200},
url = {https://doi.org/10.1007/978-3-319-45641-6_21},
}
@InProceedings{lommen2022twn,
author = {Nils Lommen and Fabian Meyer and J{\"{u}}rgen Giesl},
booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR} 2022, Haifa, Israel, August 8-10, 2022, Proceedings},
title = {Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops},
year = {2022},
editor = {Jasmin Blanchette and Laura Kov{\'{a}}cs and Dirk Pattinson},
pages = {734--754},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {13385},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/cade/LommenMG22.bib},
doi = {10.1007/978-3-031-10769-6_43},
timestamp = {Mon, 24 Oct 2022 16:36:35 +0200},
url = {https://doi.org/10.1007/978-3-031-10769-6_43},
}
@InProceedings{DBLP:conf/sas/Ben-AmramDG19,
author = {Amir M. Ben{-}Amram and Jes{\'{u}}s J. Dom{\'{e}}nech and Samir Genaim},
booktitle = {Static Analysis - 26th International Symposium, {SAS} 2019, Porto, Portugal, October 8-11, 2019, Proceedings},
title = {Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets},
year = {2019},
editor = {Bor{-}Yuh Evan Chang},
pages = {459--480},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {11822},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/conf/sas/Ben-AmramDG19.bib},
doi = {10.1007/978-3-030-32304-2\_22},
timestamp = {Mon, 03 Jan 2022 22:21:24 +0100},
url = {https://doi.org/10.1007/978-3-030-32304-2\_22},
}