Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes

Autor: Fabian Meyer, Jürgen Giesl, Marcel Hark

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030720155
TACAS (1)
Cham : Springer International Publishing, Lecture Notes in Computer Science 12651, 250-269 (2021). doi:10.1007/978-3-030-72016-2_14
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings / Editors: Jan Friso GrooteKim Guldstrand Larsen.-Part I
Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings / Editors: Jan Friso GrooteKim Guldstrand Larsen.-Part I27. International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, online, 2021-03-27-2021-04-0124. European Joint Conferences on Theory and Practice of Software, ETAPS 2021, online, 2021-03-27-2021-04-01

Tools and Algorithms for the Construction and Analysis of Systems : 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – Ap

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4538826dd51d8c79b602b414f85f4dfc
http://europepmc.org/articles/PMC7979164

Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)

Autor: Florian Frohn, Jürgen Giesl

Publikováno v: Automated Reasoning ISBN: 9783031107689

We present the Loop Acceleration Tool (), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on the novel calculus from [10, 11] for loop acceleration, i.e., transforming loops into

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::b5e04fa91225ff118b33df73b84d7049
https://doi.org/10.1007/978-3-031-10769-6_41

Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops

Autor: Nils Lommen, Fabian Meyer, Jürgen Giesl

Publikováno v: Automated Reasoning ISBN: 9783031107689
Cham : Springer, Lecture notes in computer science 13385, 734-754 (2022). doi:10.1007/978-3-031-10769-6_43
Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, proceedings / Jasmin Blanchette, Laura Kovács, Dirk Pattinson (eds.)
Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, proceedings / Jasmin Blanchette, Laura Kovács, Dirk Pattinson (eds.)11. International Joint Conference on Automated Reasoning, IJCAR 2022, Haifa, Israel, 2022-08-08-2022-08-10

There exist several results on deciding termination and computing runtime bounds for triangular weakly non-linear loops (twn-loops). We show how to use results on such subclasses of programs where complexity bounds are computable within incomplete ap

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::046989eba7b2070be3c5485a884dd79b

Loops under Strategies ... Continued

Autor: René Thiemann, Christian Sternagel, Jürgen Giesl, Peter Schneider-Kamp

Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 44, Iss Proc. IWS 2010, Pp 51-65 (2010)

While there are many approaches for automatically proving termination of term rewrite systems, up to now there exist only few techniques to disprove their termination automatically. Almost all of these techniques try to find loops, where the existenc

Externí odkaz: https://doaj.org/article/33ed69423c9d42c7b70bd630b80b8b29

Aiming low is harder: induction for lower bounds in probabilistic program verification

Autor: Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen

Publikováno v: Proceedings of the ACM on Programming Languages

We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule is simple in the sense that loop body semantics need to be applie

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be9d1b5b74b04e8117cef930f441cc9a