47 citations · 65 across the 16 of their papers we have counts for
22 papers · 1 filter
Accelerating Loops with Arrays
Florian Frohn, Jürgen Giesl
We propose a novel acceleration technique for loops operating on arrays. The goal of acceleration is to characterize the transitive closure of loops in a logic which is suitable fo…
Infinite State Model Checking by Learning Transitive Relations
Florian Frohn, Jürgen Giesl
We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until cons…
A Dependency Pair Framework for Relative Termination of Term Rewriting
Jan-Christoph Kassing, Grigory Vartanyan, Jürgen Giesl
Dependency pairs are one of the most powerful techniques for proving termination of term rewrite systems (TRSs), and they are used in almost all tools for termination analysis of T…
Satisfiability Modulo Exponential Integer Arithmetic
Florian Frohn, Jürgen Giesl
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.…
Integrating Loop Acceleration into Bounded Model Checking
Florian Frohn, Jürgen Giesl
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 han…
Automated Termination Proofs for C Programs with Lists (Short WST Version)
Jera Hensel, Jürgen Giesl
There are many techniques and tools for termination of C programs, but up to now they were not very powerful for termination proofs of programs whose termination depends on recursi…
Proving Non-Termination by Acceleration Driven Clause Learning (Short WST Version)
Florian Frohn, Jürgen Giesl
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 term…
Proving Termination of C Programs with Lists
Jera Hensel, Jürgen Giesl
There are many techniques and tools to prove termination of C programs, but up to now these tools were not very powerful for fully automated termination proofs of programs whose te…
Proving Non-Termination by Acceleration Driven Clause Learning
Florian Frohn, Jürgen Giesl
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 sy…
ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses
Florian Frohn, Jürgen Giesl
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…
AProVE: Modular Termination Analysis of Memory-Manipulating C Programs
Frank Emrich, Jera Hensel, Jürgen Giesl
Termination analysis of C programs is a challenging task. On the one hand, the analysis needs to be precise enough to draw meaningful conclusions. On the other hand, relevant progr…
Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)
Florian Frohn, Jürgen Giesl
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 b…
Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes
Fabian Meyer, Marcel Hark, Jürgen Giesl
We present a novel modular approach to infer upper bounds on the expected runtime of probabilistic integer programs automatically. To this end, it computes bounds on the runtime of…
Inferring Lower Runtime Bounds for Integer Programs
Florian Frohn, Matthias Naaf, Marc Brockschmidt +1
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-rec…
Termination of Triangular Polynomial Loops
Marcel Hark, Florian Frohn, Jürgen Giesl
We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring like , , or . The…
Termination of Triangular Integer Loops is Decidable
Florian Frohn, Jürgen Giesl
We consider the problem whether termination of affine integer loops is decidable. Since Tiwari conjectured decidability in 2004, only special cases have been solved. We complement…
Proving Non-Termination via Loop Acceleration
Florian Frohn, Jürgen Giesl
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 a…
Computing Expected Runtimes for Constant Probability Programs
Jürgen Giesl, Peter Giesl, Marcel Hark
We introduce the class of constant probability (CP) programs and show that classical results from probability theory directly yield a simple decision procedure for (positive) almos…
Aiming Low Is Harder -- Induction for Lower Bounds in Probabilistic Program Verification
Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl +1
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…
Loops under Strategies ... Continued
René Thiemann, Christian Sternagel, Jürgen Giesl +1
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…
Automated Termination Proofs for Logic Programs by Term Rewriting
P. Schneider-Kamp, J. Giesl, A. Serebrenik +1
There are two kinds of approaches for termination analysis of logic programs: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the…
SAT Solving for Argument Filterings
Michael Codish, Peter Schneider-Kamp, Vitaly Lagoon +2
This paper introduces a propositional encoding for lexicographic path orders in connection with dependency pairs. This facilitates the application of SAT solvers for termination an…