Zobrazeno 1 - 10
of 70
pro vyhledávání: '"Florian Frohn"'
Publikováno v:
ACM Transactions on Programming Languages and Systems. 42:1-50
We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-recursion. Our technique constructs symbolic representations of program e
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::bdf0e2862e27e26857d67641c9cd834a
https://doi.org/10.1145/3410331
https://doi.org/10.1145/3410331
Autor:
Florian Frohn
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030451899
TACAS (1)
Lecture Notes in Computer Science
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030451899
TACAS (1)
Lecture Notes in Computer Science
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs operating on integers. To this end, a variety of acceleration techniques has been proposed. However, all of them are monolithic: Either the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::10b8baf62872f973a39c471956458107
http://europepmc.org/articles/PMC7439733
http://europepmc.org/articles/PMC7439733
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
https://doi.org/10.1007/978-3-031-10769-6_41
Publikováno v:
LPAR
LPAR-23
EasyChair Proceedings in Computing
LPAR-23
EasyChair Proceedings in Computing
In the last years, several works were concerned with identifying classes of programswhere termination is decidable. We consider triangular weakly non-linear loops(twn-loops) over a ring Z ≤ S ≤ R_A , where R_A is the set of all real algebraicnumb
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::eb34949914edd962ced4be5e7e0c205c
https://doi.org/10.29007/nxv1
https://doi.org/10.29007/nxv1
Publikováno v:
Static Analysis ISBN: 9783030654733
SAS
SAS
We consider the termination problem for triangular weakly non-linear loops (twn-loops) over some ring \(\mathcal {S}\) like \(\mathbb {Z}\), \(\mathbb {Q}\), or \(\mathbb {R}\). Essentially, the guard of such a loop is an arbitrary Boolean formula ov
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b8e59299deb72ea3a44ee0ba421c18e6
https://doi.org/10.1007/978-3-030-65474-0_5
https://doi.org/10.1007/978-3-030-65474-0_5
Autor:
Florian Frohn, Jürgen Giesl
Publikováno v:
Information Processing Letters. 139:18-23
We prove that it is semi-decidable whether the runtime complexity of a term rewrite system is constant. Our semi-decision procedure exploits that constant runtime complexity is equivalent to termination of a restricted form of narrowing, which can be
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ebb1190dcddc904711c4b875f6fb1ed7
https://doi.org/10.1016/j.ipl.2018.06.012
https://doi.org/10.1016/j.ipl.2018.06.012
Publikováno v:
Journal of Logical and Algebraic Methods in Programming. 97:105-130
In earlier work, we developed an approach for automated termination analysis of C programs with explicit pointer arithmetic, which is based on symbolic execution. However, similar to many other termination techniques, this approach assumed the progra
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2e6f24dc3909736c564ff4a8ccf8992f
https://doi.org/10.1016/j.jlamp.2018.02.004
https://doi.org/10.1016/j.jlamp.2018.02.004
Autor:
Jürgen Giesl, Florian Frohn
Publikováno v:
Computer Aided Verification
Lecture Notes in Computer Science
Cham : Springer, Lecture Notes in Computer Science 11562, 426-444 (2019). doi:10.1007/978-3-030-25543-5_24
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran31. International Conference Computer Aided Verification, CAV 2019, New York City, NY, USA, 2019-07-15-2019-07-18
Computer Aided Verification ISBN: 9783030255428
CAV (2)
Lecture Notes in Computer Science
Cham : Springer, Lecture Notes in Computer Science 11562, 426-444 (2019). doi:10.1007/978-3-030-25543-5_24
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran31. International Conference Computer Aided Verification, CAV 2019, New York City, NY, USA, 2019-07-15-2019-07-18
Computer Aided Verification ISBN: 9783030255428
CAV (2)
Computer Aided Verification : 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II / edited by Isil Dillig, Serdar Tasiran 31st International Conference Computer Aided Verification, CAV 2019, New Yor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e2248c2d8952ac6f63bd5fa125a11c9b
http://arxiv.org/abs/1905.08664
http://arxiv.org/abs/1905.08664
Autor:
Florian Frohn, Jürgen Giesl
Publikováno v:
FMCAD
We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to accelerate it instead in order to find paths to other non-terminating l
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6ce3c8dccf39f67cc53afeeb429dfc11
Autor:
Jürgen Giesl, Florian Frohn
Publikováno v:
LPAR
There exist powerful techniques to infer upper bounds on the innermost runtime complexity of term rewrite systems (TRSs), i.e., on the lengths of rewrite sequences that follow an innermost evaluation strategy. However, the techniques to analyze the (
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cf5cd07df330f0e28438abaaa88a2d68
https://doi.org/10.29007/1nbh
https://doi.org/10.29007/1nbh