1 citations · 1 across the 1 of their papers we have counts for
8 papers
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…
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.…
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…
Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
Nils Lommen, Jürgen Giesl
We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, f…
Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops
Nils Lommen, Fabian Meyer, Jürgen Giesl
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 o…