paradyx/ma-tex - Change JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC

WIP

Created by paradyx on April 28, 2023

JCK77YLTPL6VV5ZOTMGUJSFZ5DNMS3MZGP5UQLXYW6WSMEK6GAQAC

Dependencies

In channels

main

Change contents

Deletion in main.tex at line 32 [3.6845]
B:BD[3.7328] → [3.7328:7336]
```
    Foo
```

File addition: literature.bib.sav (----------)

[4.1]

@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{Brockschmidt16,
  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{DBLP:journals/scp/BagnaraHZ08,
  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},
  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{DBLP:conf/cade/GieslBEFFOPSSST14,
  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},
  timestamp = {Sat, 05 Sep 2020 18:05:20 +0200},
  url       = {https://doi.org/10.1007/978-3-319-08587-6\_13},
}
@Article{DBLP:journals/jar/GieslABEFFHOPSS17,
  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},
  timestamp = {Sat, 05 Sep 2020 17:51:29 +0200},
  url       = {https://doi.org/10.1007/s10817-016-9388-y},
}
@InProceedings{benamram2017,
  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{meyer21,
  author  = {Fabian Meyer, Marcel Hark, Jürgen Giesl},
  journal = {Tools and Algorithmsfor the Constructionand Analysis of Systems},
  title   = {Inferring Expected Runtimes of ProbabilisticInteger Programs Using Expected Sizes},
  year    = {2021},
  file    = {:/home/paradyx/MA/literatur/TACAS2021.pdf:PDF},
  url     = {https://verify.rwth-aachen.de/giesl/papers/TACAS2021.pdf},
}
@Book{alma2011,
  author    = {Billingsley, Patrick},
  publisher = {Wiley},
  title     = {Probability and measure},
  year      = {2011},
  address   = {New York [u.a},
  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},
  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},
  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    = {CoFloCo},
  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},
  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},
}

File addition: literature.bib (----------)

[4.1]

@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{Brockschmidt16,
  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{DBLP:journals/scp/BagnaraHZ08,
  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},
  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},
}
<<<<<<< HEAD
@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{DBLP:conf/cade/GieslBEFFOPSSST14,
  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},
  timestamp = {Sat, 05 Sep 2020 18:05:20 +0200},
  url       = {https://doi.org/10.1007/978-3-319-08587-6\_13},
}
@Article{DBLP:journals/jar/GieslABEFFHOPSS17,
  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},
  timestamp = {Sat, 05 Sep 2020 17:51:29 +0200},
  url       = {https://doi.org/10.1007/s10817-016-9388-y},
}
@InProceedings{benamram2017,
  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{meyer21,
  author  = {Fabian Meyer, Marcel Hark, Jürgen Giesl},
  journal = {Tools and Algorithmsfor the Constructionand Analysis of Systems},
  title   = {Inferring Expected Runtimes of ProbabilisticInteger Programs Using Expected Sizes},
  year    = {2021},
  file    = {:/home/paradyx/MA/literatur/TACAS2021.pdf:PDF},
  url     = {https://verify.rwth-aachen.de/giesl/papers/TACAS2021.pdf},
}
@Book{alma2011,
  author    = {Billingsley, Patrick},
  publisher = {Wiley},
  title     = {Probability and measure},
  year      = {2011},
  address   = {New York [u.a},
  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},
  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},
  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    = {CoFloCo},
  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},
  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},
}
@Comment{jabref-meta: databaseType:bibtex;}

Replacement in latexmkrc at line 2 [3.7445]
B:BD[3.7477] → [3.7477:7497]
```
$out_dir = 'build';
```
[3.7477]
[3.7497]
```
# $out_dir = 'build';
```
Deletion in ch5_conclusion.tex at line 4 [3.7661]
B:BD[3.7706] → [3.7706:7714]
```
\lipsum
```
Deletion in ch5_conclusion.tex at line 5 [3.7661]
B:BD[3.7736] → [3.7736:7744]
```
\lipsum
```

Replacement in ch4_implementation.tex at line 4 [3.7792]

B:BD[3.7841] → [3.7841:7849]

\lipsum

[3.7841]

[3.7849]

\begin{comment}
    Base Algorithm 
    fun find_loops_in(P)
        loop_heads = {}
        // Dijkstra
        on loop_back from l' -> l_h:
            loop_heads := loop_heads + l_h
        return loop_heads
    end
    fun heuristic(L: Loop)
        // same as original paper
    end
    fun partial_evaluation(Program P = (PV, L, GT, l_0))
        let lh := loop_heads(P)
        let properties := heuristic(P)
        let initial_state := (l_0, [])
        let P' := ({l_0}, l_0, {locations: P.l_0, {}) // todo
        for gt in GT: 
            let gt' = {}
            for t in gt: 
                (s', l_t') := evaluate(P, s, t)
                if l_t \in lh:
                    
                else : 
                gt' := gt' + 
            end
        end
    Claims: 
    Every path in P has an equivalent path in the evaluation graph EG
    Every path in EG has an equivalent path in P'
    SCC Algorithm:
    similar to above but stops at SCC boundaries. 
\end{comment}

Deletion in ch4_implementation.tex at line 42 [3.7792]
B:BD[3.7871] → [3.7871:7879]
```
\lipsum
```
Deletion in ch4_implementation.tex at line 43 [3.7792]
B:BD[3.7901] → [3.7901:7909]
```
\lipsum
```
Deletion in ch3_theory.tex at line 4 [3.7949]
B:BD[3.7990] → [3.7990:7998]
```
\lipsum
```
Deletion in ch3_theory.tex at line 5 [3.7949]
B:BD[3.8020] → [3.8020:8068]
```
\lipsum
\section{Non-probabilistic ITS}
\lipsum
```
Deletion in ch2_preliminaries.tex at line 242 [3.8115]
B:BD[2.4794] → [2.4794:4795]
Deletion in ch2_preliminaries.tex at line 243 [3.8115]
B:BD[5.3342] → [2.4796:4797]

Replacement in ch2_preliminaries.tex at line 282 [3.8115]

∅:D[5.4731] → [3.9345:9425]

B:BD[3.9345] → [3.9345:9425]

In general, an \textit{integer programs} is a programs that only uses variables

[5.4731]

[3.9425]

In general, an \textit{integer programs} is a program that only uses variables

Replacement in ch2_preliminaries.tex at line 299 [3.8115]

B:BD[3.10442] → [3.10442:10729]

\textit{general transitions} A general transition is a set of transitions with
the probabilities adding up to 1 acting as a single transition for the
non-determinism. Non-determinism can only occur between general transitions and
it is resolved first before probabilities are resolved.

[3.10442]

[3.10729]

\textit{general transitions}: they are sets of (conventional) transitions with
the probabilities adding up to 1, acting as a single transition for the
resolution of non-determinism. Non-determinism can only occur between general
transitions and it is resolved first before probabilities are resolved.

Replacement in ch2_preliminaries.tex at line 304 [3.8115]

B:BD[3.10730] → [3.10730:10935]

deterministic and non-probabilistic programs are a special case of
probabilistic programs, where very general transition consist of a single
transition and all general transitions are mutually exclusive.

[3.10730]

[3.10935]

Deterministic and non-probabilistic programs are a special case of probabilistic
programs, where every general transition consist of a single transition and all
general transitions are mutually exclusive.

Replacement in ch2_preliminaries.tex at line 308 [3.8115]

B:BD[3.10936] → [3.10936:11085]

Let's get to the formal definitions. We will follow the definition of F. Meyer
\cite{https://link.springer.com/chapter/10.1007/978-3-319-66167-4_8}.

[3.10936]

[3.11085]

This thesis will closely follow the definitions of F. Meyer \cite{https://link.springer.com/chapter/10.1007/978-3-319-66167-4_8}.
For the following the set of all variables is split into the program variables
$\PV$ and temporary variables $TV$. Program variables are assigned at the start
of a program and can get values assigned during the run of a program, wheras
temporary variables are only existentially quantified for every transition.
Hence, they do not \enquote{carry over} between states.

Replacement in ch2_preliminaries.tex at line 316 [3.8115]

B:BD[3.11353] → [3.11353:11429]

    $(\V, L, \GT, l_0)$ is a probabilistic integer transition system where

[3.11137]

[3.11429]

    $(\PV, L, \GT, l_0)$ is a probabilistic integer transition system where

Replacement in ch2_preliminaries.tex at line 318 [3.8115]

B:BD[3.11451] → [3.11451:11507]

        \item $\V$ is a finite set of program variables

[3.11451]

[3.11507]

        \item $\PV$ is a finite set of program variables

Replacement in ch2_preliminaries.tex at line 328 [3.8115]

B:BD[3.12054] → [5.4732:4807]

                \item an update function $η : \PV \mapsto \Z[\V] \cup D$,

[3.12054]

[5.4807]

                \item an update function $η : \PV \mapsto \Z[\PV] \cup D$,

Replacement in ch2_preliminaries.tex at line 340 [3.8115]

B:BD[3.12661] → [3.12661:12766]

B:BD[3.12766] → [5.5018:5035]

In this thesis we will see a log of integer programs, so let's get familiar 
with a couple of examples. 
% TODO: examples

[3.12661]

[5.5035]

\todo{examples}
\begin{figure}\label{fig:pip1}
    \caption{A simple probabilistic integer program.}
\end{figure}
\fref{fig:pip1} gives an example for a very simple probabilistic integer
program. 
\todo{give an example for temporary variables}
Unsurprisingly, a PIP is executed starting at the start location with a given
assignment $\sigma_0 : \PV \rightarrow \N$. A pair of location and assignment
$(l, \sigma) \in \L \times \Sigma$ is called a configuration and represents
specific state of a program during an execution.

Replacement in ch2_preliminaries.tex at line 353 [3.8115]

B:BD[5.5036] → [5.5036:5213]

\subsection{Semantics}
A configuration is a tuple of a location and a variable assignment $(l, \sigma)$
that stands for a specific state of a running program. Given a starting

[5.5036]

[5.5213]

Given a configuration

Replacement in ch2_preliminaries.tex at line 358 [3.8115]

B:BD[5.5425] → [5.5425:5523]

∅:D[5.5523] → [3.12766:12767]

B:BD[3.12766] → [3.12766:12767]

B:BD[3.12767] → [5.5524:5755]

configuration is the starting configuration. Note that at this point it is 
unclear what a valid 
One can take two vies to the evaluation of 
Let's define the semantics of propabilistic integer programs. We will take two
views onto the semantics of integer programs. First the intuitive one and second
a more formal definition.

[5.5425]

[5.5755]

configuration is the starting configuration.

Deletion in ch2_preliminaries.tex at line 360 [3.8115]
B:BD[5.5756] → [5.5756:5822]
```
\todo{introduce variables, assignments, constraints, polyhedron}
```

Insertion in ch2_preliminaries.tex at line 401 [3.8115]

[3.13047]


During this thesis we will transform programs. The goal is to find equivalent
programs that are easier to analyize by Koat2. But what does equivalence mean?
On non probabilistic programs one would expect, that while beeing structurally
different, the outcome of the new program is the same as the old one.
In addition the new program should take the same time as the old one. Since
costs are represented as a variable, this is part of the outcome. But the
runtime of a program is calculated by ranking-functions and they count the
number of visits to a location. In order for the runtime to be the same, bounds
shall remain the same. \todo{doesn't realy make sence!}

Insertion in ch2_preliminaries.tex at line 412 [3.8115]

[3.13048]

[5.6913]

In probabilistic programs, a the run is non-deterministic and hence calculating
the runtime is impossible. Instead we have expected runtime-bounds. So the new
program should have the same expected runtime-bounds and the same expected
costs, as the old program. Let's give a more formal definition. 
\begin{definition}[Program equivalence]
    Given two PIP $P = (\V, L, \GT, l_0)$ and $P' = (\V, L', \GT', l_0)$
    are equivalent if and only if the following properties hold:
    \begin{enumerate}
        \item \todo{continue}
    \end{enumerate}
\end{definition}

Insertion in ch1_introduction.tex at line 4 [3.14309]

[3.14357]

\subsection{Background}
\subsection{Related Works}
    Koat was first presented in \cite{brockschmidt2014tacas}
\begin{comment}
\end{comment}

Deletion in ch0_frontmatter.tex at line 48 [3.14402]

B:BD[3.16028] → [3.16028:16239]

    Hallo Welt dies ist ein tolles Abstract Es aktualisiert sogar, wenn man im Buffer Dinge schreibt. 
    Heheheheheheheheheheh!
    \begin{itemize}
        \item Fooooooo!
    \end{itemize}
    \lipsum[1-3]

File addition: .ignore (----------)
[4.1]
```
.git
.DS_Store
build
*.aux
*.pdf
*.bbl
*.log
```

WIP

Dependencies

In channels

Change contents

Deletion in main.tex at line 32 [3.6845]

File addition: literature.bib.sav (----------)

File addition: literature.bib (----------)

Replacement in latexmkrc at line 2 [3.7445]

Deletion in ch5_conclusion.tex at line 4 [3.7661]

Deletion in ch5_conclusion.tex at line 5 [3.7661]

Replacement in ch4_implementation.tex at line 4 [3.7792]

Deletion in ch4_implementation.tex at line 42 [3.7792]

Deletion in ch4_implementation.tex at line 43 [3.7792]

Deletion in ch3_theory.tex at line 4 [3.7949]

Deletion in ch3_theory.tex at line 5 [3.7949]

Deletion in ch2_preliminaries.tex at line 242 [3.8115]

Deletion in ch2_preliminaries.tex at line 243 [3.8115]