Abstract 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 for automated reasoning. Using the new notion of inductive lvalues , our technique can handle loops where previous techniques fail, and it unifies acceleration for arrays and scalar variables by regarding scalars as arrays of dimension 0. Moreover, our approach uses $$\lambda $$ λ s instead of quantifiers. Then the resulting SMT problems can be solved via lemmas on demand . An empirical evaluation of our implementation in the tool shows the power of our approach.

LoAT is a fully automated verification tool that can prove (un)satisfiability of linear Constrained Horn Clauses, as well as non-termination and lower bounds on the worst-case runtime complexity of transition systems. Recently, we introduced Accelerated Bounded Model Checking (ABMC), a novel model checking technique that combines acceleration techniques with Bounded Model Checking (BMC), and implemented it in LoAT . Acceleration techniques compute “shortcuts” that “compress” many execution steps into a single one, and thus ABMC is capable of finding deep counterexamples that are challenging for BMC, as finding them with BMC requires a large bound.

Abstract 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 constantly many steps suffice to cover all reachable states, irrespective of the initial state. Then we can prove safety by checking that no error state is reachable in D steps. To deduce transitive relations, we use recurrence analysis . While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with projections . An empirical evaluation of the implementation of our approach in our tool shows that it is highly competitive with the state of the art.

Abstract We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring $$\mathcal {S}$$ S like $$\mathbb {Z}$$ Z , $$\mathbb {Q}$$ Q , or $$\mathbb {R}$$ R . The guard of such a loop is an arbitrary quantifier-free Boolean formula over (possibly non-linear) polynomial inequations, and the body is a single assignment of the form $$\begin{bmatrix} x_1\\ \ldots \\ x_d \end{bmatrix} \leftarrow \begin{bmatrix} c_1 \cdot x_1 + p_1\\ \ldots \\ c_d \cdot x_d + p_d \end{bmatrix}$$ x 1 … x d ← c 1 · x 1 + p 1 … c d · x d + p d where each $$x_i$$ x i is a variable, $$c_i \in \mathcal {S}$$ c i ∈ S , and each $$p_i$$ p i is a (possibly non-linear) polynomial over $$\mathcal {S}$$ S and the variables $$x_{i+1},\ldots ,x_{d}$$ x i + 1 , … , x d . We show that the question of termination can be reduced to the existential fragment of the first-order theory of $$\mathcal {S}$$ S . For loops over $$\mathbb {R}$$ R , our reduction implies decidability of termination. For loops over $$\mathbb {Z}$$ Z and

Abstract 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 execution steps into a single one. In this paper, we tightly integrate acceleration techniques into SMT-based bounded model checking. By adding suitable “shortcuts” on the fly, our approach can quickly detect deep counterexamples. Moreover, using so-called blocking clauses , our approach can prove safety of examples where BMC diverges. An empirical comparison with other state-of-the-art techniques shows that our approach is highly competitive for proving unsafety, and orthogonal to existing techniques for proving safety.

Abstract 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 criteria to the probabilistic setting, e.g., we show when it suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to prove full AST of probabilistic term rewrite systems. These criteria also apply to other notions of termination like positive AST. We implemented and evaluated our new contributions in the tool .

Abstract 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 insufficient to capture the behavior of the analyzed system without resorting to approximations. In the last years, incremental linearization has been applied successfully to satisfiability modulo real arithmetic with transcendental functions. We adapt this approach to an extension of polynomial integer arithmetic with exponential functions. Here, the key challenge is to compute suitable lemmas that eliminate the current model from the search space if it violates the semantics of exponentiation. An empirical evaluation of our implementation shows that our approach is highly effective in practice.

Abstract 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 implemented ADCL-NT in our tool and evaluate it against the state of the art.

Abstract Loop acceleration can be used to prove safety, reachability, runtime bounds, and (non-)termination of programs. To this end, a variety of acceleration techniques have been proposed. However, so far all of them have been monolithic, i.e., a single loop could not be accelerated using a combination of several different acceleration techniques. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. Some of these acceleration techniques apply only to non-terminating loops. Thus, combining them with our novel calculus results in a new, modular approach for proving non-termination. An empirical evaluation demonstrates the applicability of our approach, both for loop acceleration and for proving non-termination.

In the last years, several works were concerned with identifying classes of programs where 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 algebraic numbers. Essentially, the body of such a loop is a single assignment (x_1, ..., x_d) ← (c_1 · x_1 + pol_1, ..., c_d · x_d + pol_d) where each x_i is a variable, c_i ∈ S, and each pol_i is a (possibly non-linear) polynomial over S and the variables x_{i+1}, ..., x_d. Recently, we showed that termination of such loops is decidable for S = R_A and non-termination is semi-decidable for S = Z and S = Q. In this paper, we show that the halting problem is decidable for twn-loops over any ring Z ≤ S ≤ R_A. In contrast to the termination problem, where termination on all inputs is considered, the halting problem is concerned with termination on a given input. This allows us to compute witnesses for non-termination. Moreover, we present the first computability results on the runtime complexity of such loops. More precisely, we show that for twn-loops over Z one can always compute a polynomial f such that the length of all terminating runs is bounded by f( || (x_1, ..., x_d) || ), where || · || denotes the 1-norm. As a corollary, we obtain that the runtime of a terminating triangular linear loop over Z is at most linear.

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 they accelerate a loop successfully or they fail completely. In contrast, we present a calculus that allows for combining acceleration techniques in a modular way and we show how to integrate many existing acceleration techniques into our calculus. Moreover, we propose two novel acceleration techniques that can be incorporated into our calculus seamlessly. An empirical evaluation demonstrates the applicability of our approach.

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 executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs using a special-purpose calculus and an SMT encoding. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large class of examples.

We consider the problem whether termination of affine integer loops is decidable. Since Tiwari conjectured decidability in 2004 [ 15 ], only special cases have been solved [ 3 , 4 , 14 ]. We complement this work by proving decidability for the case that the update matrix is triangular.

The following topics are dealt with: formal verification; program verification; computability; formal specification; program diagnostics; computational complexity; Boolean functions; protocols; theorem proving; inference mechanisms.

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 (full) runtime complexity of TRSs are substantially weaker. In this paper, we present a sufficient criterion to ensure that the runtime complexity of a TRS coincides with its innermost runtime complexity. This criterion can easily be checked automatically and it allows us to use all techniques and tools for innermost runtime complexity in order to analyze (full) runtime complexity. By extensive experiments with an implementation of our results in the tool AProVE, we show that this improves the state of the art of automated complexity analysis significantly.

We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term in the sequence. We implemented our approach in the tool AProVE and evaluated it by extensive experiments.