Zobrazeno 1 - 10
of 46
pro vyhledávání: '"Frohn, Florian"'
Autor:
Frohn, Florian, Giesl, Jürgen
SMT solvers use sophisticated techniques for polynomial (linear or non-linear) integer arithmetic. In contrast, non-polynomial integer arithmetic has mostly been neglected so far. However, in the context of program verification, polynomials are often
Externí odkaz:
http://arxiv.org/abs/2402.01501
Autor:
Frohn, Florian, Giesl, Jürgen
Bounded Model Checking (BMC) is a powerful technique for proving unsafety. However, finding deep counterexamples that require a large bound is challenging for BMC. On the other hand, acceleration techniques compute "shortcuts" that "compress" many ex
Externí odkaz:
http://arxiv.org/abs/2401.09973
There are many evaluation strategies for term rewrite systems, but proving termination automatically is usually easiest for innermost rewriting. Several syntactic criteria exist when innermost termination implies full termination. We adapt these crit
Externí odkaz:
http://arxiv.org/abs/2310.06121
Autor:
Frohn, Florian, Giesl, Jürgen
We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to disprove termination of transition systems, and we evaluate its implementation in o
Externí odkaz:
http://arxiv.org/abs/2307.09839
Autor:
Frohn, Florian, Giesl, Jürgen
We recently proposed Acceleration Driven Clause Learning (ADCL), a novel calculus to analyze satisfiability of Constrained Horn Clauses (CHCs). Here, we adapt ADCL to transition systems and introduce ADCL-NT, a variant for disproving termination. We
Externí odkaz:
http://arxiv.org/abs/2304.10166
Autor:
Frohn, Florian, Giesl, Jürgen
Constrained Horn Clauses (CHCs) are often used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On the other hand, acceleration techniques for computing formulas that ch
Externí odkaz:
http://arxiv.org/abs/2303.01827
Autor:
Frohn, Florian, Giesl, Jürgen
We present the new version of the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on a novel calculus for loop acceleration, i.e., transforming loo
Externí odkaz:
http://arxiv.org/abs/2202.04546
Autor:
Frohn, Florian, Fuhs, Carsten
Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques has been proposed. However, so far all of them have been monolithic, i.e., a single loop
Externí odkaz:
http://arxiv.org/abs/2111.13952
Autor:
Frohn, Florian
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:
http://arxiv.org/abs/2001.01516
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:
http://arxiv.org/abs/1911.01077