Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Since Colón’s et al. seminal paper [1], the so-called constraint-based method has been applied with success to a wide range of problems in system verification, from invariant generation in Petri nets [2], hybrid systems [3] and programs with arrays [4, 5], to termination [6, 7] and non-termination proving [8]. In most of these applications, one is interested in generating linear properties, e.g., linear invariants or linear ranking functions. In these cases, Farkas’ Lemma is employed for producing the constraints over the template unknowns. As a result, a non-linear SMT formula is obtained, for which a model has to be found. Despite the great advances in non-linear SMT [9–11], the applicability of the approach is still strongly conditioned by current solving technology.

A way to circumvent the bottleneck of using non-linear constraint solvers is to exploit the fragment of logics in which the program under study is described. Although this has not been explored so far in the constraint-based method, other more mature approaches for program analysis such as abstract interpretation [12] have profited from this sort of refinements since the early days of their inception. Indeed, there is a wide variety of non-relational and weakly-relational numerical abstract domains which cover different subsets of linear arithmetic, but whose complexity is lower than that of the full language [13]: intervals [14], zones [15] and octagons [16], to name a few. Also in the model checking community, it is common to focus on particular subclasses of linear inequalities as a means to improve efficiency. In particular, potential constraints have been employed in the verification of several kinds of timed and concurrent systems [17–19].

In this paper we restrict our attention to difference logic over the integers, in which atoms are inequalities of the form \(u - v \le k\), where u and v are integer variables, and \(k \in \mathbb {Z}\). This fragment of linear arithmetic corresponds to the aforementioned zone abstract domain in abstract interpretation, and to the potential constraints in model checking. Our contributions in this work are:

  • we propose an encoding for satisfiability and unsatisfiability of sets of inequalities in difference logic including templates, which results in formulas of difference logic. This is noteworthy since current approaches to equivalent problems in general full linear arithmetic lead to non-linear formulas.

  • for the problem of, given a set of inequalities with free independent terms, choosing an invariant subset that proves an assertion, we present two encodings, one for full linear arithmetic and another specialized one for difference logic. While the former leads to non-linear formulas, again the latter falls into a more tractable fragment, in this case linear arithmetic.

  • we present an experimental evaluation with the constraint-based verification system VeryMax  [20]. We consider the problem of proving the absence of out-of-bounds array accesses in a benchmark suite of numerical programs, and our results show that the expressiveness of difference logic is sufficient to succeed in the majority of the cases, while a remarkable boost in performance is obtained thanks to the proposed techniques.

Two closely related works are [21, 22], in which invariants of slightly more general classes than difference logic are generated following the constraint-based method, but with different strategies for producing the constraints over template unknowns. In [21], the authors discover octagonal invariants, i.e., of the form \(\pm x_1 \pm x_2 \le k\), as well as max-plus invariants \(\max _{1 \le i \le n}(a_0, x_i + a_i) \le \max _{1 \le i \le n}(b_0, x_i + b_i)\). While our approach cannot currently produce max-plus invariants, the standard technique of adding for each variable x a copy standing for \(-x\) [16, 23] allows generating octagonal invariants too. However, the quantifier elimination method in [21] is incomplete and, as a result, invariants may be missed. Moreover, program assignments must be of the form \(x := \pm x + K\) or \(x := K\), where K is a constant, and so unlike with our techniques the common case of assignments like \(x := y\), where x, y are different variables, is not allowed. As regards [22], in that paper template domains are considered, where templates are linear inequalities with free independent term but fixed dependent term. There the quantifier elimination procedure [24] is precise, but is not specialized for difference logic. Unfortunately, the available implementation cannot produce difference logic invariants and so cannot be used for an experimental comparison.

2 Background

Programs, Invariants and Safety. Let us fix a set of (integer) program variables \(\mathcal{X}= \{ x_1,\ldots ,x_n \}\), and denote by \(\mathcal {F}(\mathcal{X})\) the formulas consisting of conjunctions of linear inequalitiesFootnote 1 over the variables \(\mathcal{X}\). Let \(\mathcal{L}\) be the set of program locations, which contains a set \(\mathcal{L}_0\) of initial locations. Program transitions \(\mathcal{T}\) are tuples \((\ell _S, \tau , \ell _T)\), where \(\ell _S\) and \(\ell _T \in \mathcal{L}\) represent the source and target locations respectively, and \(\tau \in \mathcal {F}(\mathcal{X}\cup \mathcal{X}')\) describes the transition relation. Here \(\mathcal{X}' = \{ x_1', \ldots , x_n'\}\) represent the values of the variables after the transition.Footnote 2 A transition is initial if its source location is initial. The set of initial transitions is denoted by \(\mathcal{T}_0\). A program is a pair \(\mathcal{P}= (\mathcal{L}, \mathcal{T})\), which can be viewed as a directed graph where the locations \(\mathcal{L}\) are the nodes, and each transition \((\ell _S, \tau , \ell _T)\) from \(\mathcal{T}\) leads to an edge in the graph from \(\ell _S\) to \(\ell _T\) labelled by \(\tau \).

A state \(s = (\ell , {\varvec{x}})\) consists of a location \(\ell \in \mathcal{L}\) and a valuation \({\varvec{x}}: \mathcal{X}\rightarrow \mathbb {Z}\). A state is initial if its location is initial. We denote a computation step with transition \(t = (\ell _{S}, \tau , \ell _T)\) by \((\ell _S, {\varvec{x}}) \rightarrow _t (\ell _T, {\varvec{x}'})\) when the valuations \({\varvec{x}}\), \({\varvec{x}'}\) satisfy the transition relation \(\tau \) of t. We use \(\rightarrow _{\mathcal{P}}\) if we do not care about the executed transition, and \(\rightarrow ^*_{\mathcal{P}}\) to denote the transitive-reflexive closure of \(\rightarrow _{\mathcal{P}}\). We say that a state s is reachable if there exists an initial state \(s_0\) such that \(s_0 \rightarrow ^*_{\mathcal{P}} s\).

An assertion \((\ell , \varphi )\) is a pair of a location \(\ell \in \mathcal{L}\) and a formula \(\varphi \) with free variables \(\mathcal{X}\). A program is safe with respect to the assertion \((\ell , \varphi )\) if for every reachable state \((\ell , {\varvec{x}})\), we have that \({\varvec{x}}\, \models \, \varphi \) holds.

A map \(\mathcal{I}: \mathcal{L}\rightarrow \mathcal {F}(\mathcal{X})\) is an invariant if for every \(\ell \in \mathcal{L}\), the program is safe with respect to \((\ell , \mathcal{I}(\ell ))\). An important class of invariants are inductive invariants. A map \(\mathcal{I}\) is an inductive invariant if the following two conditions hold:

figure a

If only the condition Consecution is fulfilled, the map \(\mathcal{I}\) is called a conditional inductive invariant.

One of the key problems in program analysis is to determine whether a program is safe with respect to a given assertion \((\ell , \varphi )\). This is typically proved by computing an (inductive) invariant \(\mathcal{I}\) such that the following condition holds:

figure b

In this case we say that the invariant \(\mathcal{I}\) proves the assertion \((\ell , \varphi )\).

Finally, we say a transition \(t = (\ell _S, \tau , \ell _T)\) is disabled if it can never be executed, i.e., if for any reachable state \((\ell _S, {\varvec{x}})\), there does not exist any \({\varvec{x}'}\) such that \(({\varvec{x}}, {\varvec{x}'})\) satisfies \(\tau \). One can prove this by computing an invariant \(\mathcal{I}\) such that \(\mathcal{I}(\ell _S) \, \models \, \lnot \tau \). Disabled transitions allow one to simplify the program under analysis, since they can be soundly removed from the program. In general, if \(\mathcal{I}\) is an invariant map, then any transition \(t=(\ell _S, \tau , \ell _T)\) can be soundly strengthened by replacing the transition relation \(\tau \) by \(\mathcal{I}(\ell _S) \wedge \tau \).

Constraint-Based Invariant Generation. Invariants can be generated using the constraint-based (also called template-based) method [1]. The idea is to consider templates for candidate invariant properties. These templates involve both the program variables as well as fresh template variables whose values have to be determined to ensure invariance. To this end, conditions Initiation and Consecution are enforced by means of constraints. Any solution to these constraints yields an invariant. If templates represent linear inequalities, Farkas’ Lemma [25] is used to express the constraints in terms of the template variables:

Theorem 1

(Farkas’ Lemma). Let S be a system of linear inequalities \({\varvec{A}}{\varvec{x}} \le {\varvec{b}}\) (\({\varvec{A}} \in \mathbb {R}^{m \times n}, {\varvec{b}} \in \mathbb {R}^m\)) over real variables \({\varvec{x}}\). Then S has no solution iff there is \({\varvec{\lambda }}\in \mathbb {R}^m\) (called the multipliers) such that \({\varvec{\lambda }}\ge {\varvec{0}}\), \({\varvec{\lambda }}^T {\varvec{A}} = {\varvec{0}}\) and \({\varvec{\lambda }}^T {\varvec{b}} \le -1\).

In general, an SMT formula over non-linear arithmetic is obtained. By assigning weights to the different conditions, invariant generation can be cast as an optimization problem in the Max-SMT framework [7, 8, 20].

Example 1

Consider the program in Fig. 1, with the state variables n, \(x_0\), i:

Fig. 1.
figure 1

Program with a single initial location \(\ell _0\).

Full size image

Let us take the following 3 templates expressing general linear inequalities, one for each non-initial location:

$$T_j:= c_{0j} \, x_0 \,+\, c_{1j}\, n \,+\, c_{2j}\, i \le d_j \qquad \text { for all } j = 1\ldots 3\, .$$

By imposing that these templates yield an invariant, we obtain the conditions (for simplicity, no assertion and thus no Safety condition is considered here):

By fleshing out the transition relations, expanding the templates and simplifying, these four formulas are equivalent to

$$ \begin{array}{lllllllllllllllllllllllllllllllllllllllllll} (1)\ x_0 - n \le -1 \wedge -(c_{01} \,+\, c_{21})\, x_0 \,-\, c_{11}\, n \le -d_1-1 \\ (2)\ c_{01} \, x_0 \,+\, c_{11}\, n \,+\, c_{21}\, i \le d_1 \wedge i-n \le -2 \wedge -c_{02} \, x_0 \,-\, c_{12}\, n \,-\, c_{22}\, i \le -d_2-1 \\ (3)\ c_{02} \, x_0 \,+\, c_{12}\, n \,+\, c_{22}\, i \le d_2 \wedge \wedge -c_{01} \, x_0 \,-\, c_{11}\, n \,-\, c_{21}\, i \le -d_1-1+c_{21} \\ (4)\ c_{01} \, x_0 \,+\, c_{11}\, n \,+\, c_{21}\, i \le d_1 \wedge n-i \le 1 \wedge -c_{03} \, x_0 \,-\, c_{13}\, n \,-\, c_{23}\, i \le -d_3-1\\ \end{array} $$

respectively. Now Farkas’ Lemma is applied to express unsatisfiability. Namely, for (1) we consider non-negative multipliers \(\lambda _{11},\lambda _{12}\) such that the linear combination that consists in multiplying the first inequality by \(\lambda _{11}\) and the second inequality by \(\lambda _{12}\) results in a trivially false inequality. For that, we need the coefficients of \(x_0\) to cancel out, i.e., \(\lambda _{11} - \lambda _{12}(c_{01}+c_{21}) = 0\), and the same for n, i.e., \(-\lambda _{11} - \lambda _{12} c_{11} = 0\). With respect to the independent term, we force that it is smaller than or equal to \(-1\), i.e., \(-\lambda _{11} + \lambda _{12} (-d_1-1) \le -1\), which will create a trivially false inequality. All in all, we get the non-linear formula

$$\begin{aligned} \begin{array}{llll} \exists \lambda _{11} \lambda _{12} &{} \big ( \lambda _{11}, \lambda _{12} \ge 0 \;\wedge \; \\ &{} \lambda _{11} - \lambda _{12}(c_{01}+c_{21}) = -\lambda _{11} - \lambda _{12} c_{11} = 0 \;\wedge \; \\ &{} -\lambda _{11} + \lambda _{12} (-d_1-1) \le -1\big ) \end{array} \end{aligned}$$
(1)

Similar constraints are obtained for (2)-(4).   \(\square \)

Difference Logic and Graph Theory. Given variables u and v and a numeric constant k, henceforth we will refer to an inequality of the form \(u - v \le k\) as a difference inequality. The fragment of (quantifier-free) first-order logic where atoms are difference inequalities is called difference logic.

Sets (conjunctions) of difference inequalities, also called difference systems, have long been studied in the literature (e.g., in [26], where they are referred to as simple temporal problems, STP’s). For instance, they can be represented as graphs as follows. Given a difference system S defined over variables \(v_1,v_2,\ldots ,v_n\), we consider the weighted graph G with vertices \(\left( v_1,v_2,\ldots ,v_n \right) \) and an edge \(v_i \mathop {\rightarrow }\limits ^{k} v_j\) for each inequality \(v_i - v_j \le k \in S\). This graph is called the constraint graph of S.

It is well-known that a constraint graph has interesting properties as regards to the solutions of the corresponding difference system [27]:

Theorem 2

Let S be a difference system, and G its constraint graph. Then S has no solution iff G has a negative cycle.

This result is a particular case of Farkas’ Lemma. It essentially ensures that, for difference systems, the multipliers of Farkas’ Lemma are either 1 or 0 (the difference inequality belongs to the negative cycle or it does not, respectively).

One of the most important practical consequences of Theorem 2 is that any algorithm that is able to detect negative cycles in weighted graphs (such as, for instance, Bellman-Ford, or Floyd-Warshall [27]) can be used to determine the existence of solutions to a difference system.

Theorem 2 can be extended to allow also bound inequalities, i.e., inequalities of the form \(v \le k\) or \(v \ge k\), where v is a variable and k is a numeric constant: Given a system S that includes difference inequalities as well as bound inequalities, a fresh variable \(v_0\) is introduced. Then a new system \(S^*\) is defined, which is like S but where each inequality of the form \(v_i \le k\) in S is replaced by \(v_i - v_0\le k\), and each \(v_i \ge k\), or equivalently \(-v_i \le -k\), is replaced by \(v_0 - v_i \le -k\). It is not difficult to prove that S has a solution iff \(S^*\) has one.

3 Proving Safety of Difference Programs

In this paper we will focus on difference programs, that is, programs whose transition relations are conjunctions of difference inequalities.

Although this may seem rather restrictive, in fact more general programs can be cast into this form: for any program with difference as well as bound inequalities in the transition relations, there exists an equivalent difference program, as it is well-known in the literature [15]. The trick consists in introducing an artificial variable \(x_0\), which intuitively is always zero, and then transform bound inequalities into difference inequalities by adding \(x_0\) with the appropriate sign. Thus, e.g., \(n \ge 1\) is transformed into \(n - x_0 \ge 1\). Moreover, the equation \(x_0' = x_0\) has to be added to all transitions. For example, after this transformation the program in Fig. 2 leads to that in Fig. 1.

Fig. 2.
figure 2

Program with difference and bound inequalities in the transition relations.

Full size image

The problem we consider in this section is, given a location \(\ell \) and a difference inequality \(\varphi \), to prove that the program under consideration is safe with respect to the assertion \((\ell , \varphi )\). As the following theorem states, proving safety of a difference program is in general undecidable, and therefore we cannot hope for a sound and complete terminating algorithm that solves the problem:

Theorem 3

Given a difference program \(\mathcal{P}\), a location \(\ell \in \mathcal{L}\) and a difference inequality \(\varphi \), the problem of deciding whether \(\mathcal{P}\) is safe with respect to the assertion \((\ell , \varphi )\) is undecidable.

3.1 Specialization of the Constraint-Based Method

Here we attempt to prove difference programs safe by finding invariants consisting of difference inequalities with a specialization of the constraint-based method.Footnote 3 Let us first illustrate the gist of our technique with an example.

Example 2

Again let us consider the program in Fig. 1 and assign a template to each non-initial location: \(T_j:= c_{0j} \, x_0 \,+\, c_{1j}\, n \,+\, c_{2j}\, i \le d_j\) for all \(j = 1\ldots 3\, .\) This program is a difference program. Let us also consider the assignment \(c_{0,j} = 0, c_{1,j} = -1, c_{2,j} = 1\) for all \(j = 1 \ldots 3\), \(d_1 = d_3 = -1\), \(d_2 = -2\), which instantiates the templates as follows:

$$\begin{aligned} T_1 \equiv i - n \le -1 \qquad T_2 \equiv i - n \le -2 \qquad T_3 \equiv i - n \le -1, \qquad \end{aligned}$$

and check that they are invariant. Since the above inequalities belong to difference logic, we can use Theorem 2 to check that indeed the formulas \({\tau _0} \wedge \lnot T'_1\), \(T_1 \wedge {\tau _1} \wedge \lnot T'_2\), \(T_2 \wedge {\tau _2} \wedge \lnot T'_1\) and \(T_1 \wedge {\tau _3} \wedge \lnot T'_3\) are unsatisfiable, as required by the Initiation and Consecution conditions. By the theorem, the unsatisfiability of each of these formulas is equivalent to the existence of a negative cycle in the corresponding graph. In Fig. 3 some of these graphs are shown for the particular solution considered here, and the respective negative cycles are highlighted. Solving the Initiation and Consecution constraints over the template coefficients can thus be seen as adding new weighted edges to the graphs of the transition relations so that, in the end, all graphs have a negative cycle. Note this must be done consistently for all Initiation and Consecution constraints, so that, e.g., the edge of \(\lnot T'_1\) is the same in \({\tau _0} \wedge \lnot T'_1\) and in \(T_2 \wedge {\tau _2} \wedge \lnot T'_1\).

Fig. 3.
figure 3

Graphs for the formulas \({\tau _0} \wedge \lnot T'_1\) (a) and \(T_2 \wedge {\tau _2} \wedge \lnot T'_1\) (b). The edges corresponding to the templates (or their negation) are dashed. The edges forming the negative cycles are highlighted with thicker lines.

Full size image

In what follows, we assume we have associated to each non-initial location \(\ell \) a template invariant \(T_{\ell }\) of the form

$$ c_{0,\ell } \, x_0 \,+\, c_{1,\ell }\, x_1 \,+\, \ldots \,+\, c_{n,\ell }\, x_n \le d_\ell $$

where the \(c_{i,\ell }\) and the \(d_{\ell }\) are template unknowns.Footnote 4 For obvious reasons we will refer to the \(c_{i,\ell }\) as left-hand side variables, whereas the \(d_{\ell }\) are called right-hand side variables (LHS and RHS variables, respectively). Here we focus on difference inequalities, and therefore the domain of LHS variables is \(\{+1,0,-1\}\), while the domain of RHS variables is \(\mathbb {Z}\).

We propose to find appropriate values for the RHS and LHS variables following an eager approach: we encode all required constraints obtained from the Initiation, Consecution and Safety conditions into a single SMT formula, and then use an off-the-shelf SMT solver to solve the resulting problem. As will be seen next, in our particular case the atoms in the SMT formula will be either Boolean variables or bound inequalities or difference inequalities. By virtue of the results reviewed in Sect. 2, the generated formula can be handled with an SMT solver of difference logic, for which efficient implementations are available.

The formula that expresses the constraints over template variables (LHS and RHS variables) is a conjunction of the following ingredients.

Membership to Difference Logic. First of all, we have to express that all templates are difference inequalities. To that end, for each LHS variable \(c_{i}\) we introduce two auxiliary Boolean variables: \(c^{+}_{i}\) and \(c^{-}_{i}\). Intuitively, \(c^{+}_{i}\) will be true iff \(c_i\) is assigned to \(+1\), and \(c^{-}_{i}\) will be true iff \(c_{i}\) is assigned to \(-1\). If both \(c^{+}_{i}\) and \(c^{-}_{i}\) are false, then \(c_{i}\) is 0. We need to enforce: (i) that the \(c^{+}_{i}\) and \(c^{-}_{i}\) cannot be true at the same time, (ii) that exactly one of the \(c_i\) in each template is \(+1\) (i.e., exactly one of the \(c^{+}_{i}\) is true), and (iii) exactly one is \(-1\) (i.e., exactly one of the \(c^{-}_{i}\) is true). The constraints resulting from (ii) and (iii), which are of the form \(\sum _{j=1}^m b_j = 1\), are encoded with a clause \(\bigvee _{j=1}^m b_j\) that imposes \(\sum _{j=1}^m b_j \ge 1\), together with additional clauses that express \(\sum _{j=1}^m b_j \le 1\) using one of the available encodings in the literature (e.g., quadratic, logarithmic [28] or ladder [29]).

Unsatisfiability of Difference Systems. When encoding the Initiation, Consecution and Safety conditions, essentially one has to impose the unsatisfiability of a set of difference inequalities, some of which may be templates. Namely, in Initiation and Safety one has a single template, but while in the former the template appears negatively, in the latter it appears positively. On the other hand, in Consecution two templates appear, one negatively and the other positively. Here we will elaborate on this latter case, being the others simpler.

Thus, let \(\mathcal{S}\) be a difference system over program variables \(\mathcal{X}\), \(\mathcal{X}'\) such that

$$c_0\,x_0 + \ldots + c_n\,x_n \le d \;\wedge \; \mathcal{S}\;\;\wedge \;\; \lnot (\tilde{c_0}\,x'_0 + \ldots + \tilde{c_n}\,x'_n \le \tilde{d})$$

must be unsatisfiable. Our goal is to instantiate the templates so that this is the case. Note \(\lnot (\tilde{c_0}\,x'_0 + \ldots + \tilde{c_n}\,x'_n \le \tilde{d})\) is equivalent to \(-\tilde{c_0}\,x'_0 - \ldots - \tilde{c_n}\,x'_n \le -\tilde{d}-1\). To ensure unsatisfiability, i.e., that a negative cycle exists, we first construct \(\mathcal {G}\), the constraint graph induced by \(\mathcal S\). We then apply Floyd-Warshall algorithm in order to compute the distances dist(y, z) for each pair of vertices y and z in \(\mathcal {G}\).

If for some vertex y we have \(dist(y,y) < 0\), then \(\mathcal{S}\) has a negative cycle and hence the unsatisfiability requirement is fulfilled independently from the templates. In this case, no clause needs to be added.

Otherwise \(\mathcal{S}\) has no negative cycles, and the only possibility to construct one is to go through the edges induced by the templates. Let us consider an assignment such that \(c_u = +1\), \(c_v = -1\), \(\tilde{c}_{\tilde{u}} = +1\) and \(\tilde{c}_{\tilde{v}} = -1\) (i.e. \(c^{+}_{u}\), \(c^{-}_{v}\), \(c^{+}_{\tilde{u}}\) and \(c^{-}_{\tilde{v}}\) are true). In this case the instantiation of the positive template is \(x_u -x_v \le d\), and the instantiation of the negation of the other template is \(x^\prime _{\tilde{v}} -x^\prime _{\tilde{u}} \le -\tilde{d}-1\). Hence, the former induces an edge from \(x_{u}\) to \(x_{v}\) with weight d, while the latter induces an edge from \(x'_{\tilde{v}}\) to \(x'_{\tilde{u}}\) with weight \(-\tilde{d}-1\).

To form a negative cycle, either (i) the cycle contains only the positive template, or (ii) contains only the negative template, or (iii) contains both. The first situation can be seen in Fig. 4(a), where it is needed that \(dist(x_v,x_u) + d < 0\). The second situation is depicted in Fig. 4(b), where we need \(dist(x'_{\tilde{u}},x'_{\tilde{v}}) - \tilde{d} -1 < 0\). Finally the third situation can be seen in Fig. 4(c), where we need \(d + dist(x_v,x'_{\tilde{v}}) - \tilde{d} -1 + dist(x'_{\tilde{u}},x_u) < 0\). Hence, we add the following clause:

(2)
Fig. 4.
figure 4

The only three ways of creating a negative cycle.

Full size image

Note that it might be the case that some of the paths represented in Fig. 4 do not actually exist. For example, if \(x_u\) is unreachable from \(x_v\), i.e., \(dist(x_{v},x_{u}) = \infty \), then there cannot be a negative cycle that only uses the positive template, independently of the value we give to its RHS variable. Hence the first inequality in the clause of Eq. 2 can be dropped.

This reasoning is applied to all vertices, namely, to all \(u,v,\tilde{u},\tilde{v}\) with \(u\ne v\), \(\tilde{u}\ne \tilde{v}\), and \(u,v,\tilde{u},\tilde{v} \in \{0,1,\ldots , n\}\), adding in each case the respective clause.

Satisfiability of Difference Systems. The opposite problem to the previous one, that is, to enforce that a difference system is satisfiable, also arises in the constraint-based method. This is the case when, for example, one performs several rounds of invariant generation as described above, and requires that the newly generated invariants are not redundant with respect to the already computed ones: then there must exist a witness that certifies the non-redundancy.

Hence, let \(\mathcal{S}\) be a difference system over program variables \(\mathcal{X}\) such that

\(\mathcal{S}\wedge \lnot ( c_0\,x_0 + \ldots + c_n\,x_n \le d) \;\;\equiv \;\; \mathcal{S}\wedge -{c_0}\,x_0 - \ldots - {c_n}\,x_n \le -{d}-1\)

must be satisfiableFootnote 5. By Theorem 2, this amounts to proving that no negative cycle exists in the corresponding constraint graph. Again, we will start by constructing \(\mathcal{G}\), the constraint graph induced by \(\mathcal{S}\), and applying Floyd-Warshall.

If a negative cycle is already detected, the satisfiability requirement cannot be met. Otherwise \(\mathcal{S}\) has no negative cycles, and the only possibility to achieve one is to go through the edge induced by the template. If \(c_u=1\) and \(c_v=-1\), then the negation of the template is \(x_v - x_u \le -d-1\), which induces an edge from \(x_v\) to \(x_u\) with weight \(-d-1\). This edge is part of a negative cycle iff \(dist(x_u,x_v) - d - 1 < 0\). Since we want to avoid negative cycles, we should enforce that \(d \le dist(x_u,x_v) - 1\). Hence, we should add the clause:

$$c^{+}_{u} \wedge c^{-}_{v} \implies d \le dist(x_u, x_v ) - 1 \, .$$

Note that if \(dist(x_u, x_v) = \infty \) the clause is trivially satisfied and can be dropped.

3.2 Experiments

To experimentally evaluate our techniques, we executed an implementation of the encoding presented in Sect. 3.1 on a benchmark suite obtained as followsFootnote 6: we first ran our verification system VeryMax  [20] on numerical (possibly non-difference) programs from [30], checking whether all array accesses are within bounds. For each such check, VeryMax needs to process several safety subqueries, which consist of a small program with an assertion to be proved. Among them, we chose those where the program and the assertion can be expressed in difference logic. For these queries, VeryMax requires one of the next five possible outputs:

  1. I.

    An invariant at each location proving the assertion

  2. II.

    An invariant at each location disabling a transition

  3. III.

    A conditional invariant at each location proving the assertion

  4. IV.

    An invariant at each location

  5. V.

    None of the previous ones

Solving one such query using the constraint-based method generates an SMT formula with multiple Initiation, Consecution, Safety and other conditions (e.g. no redundant invariants are generated, conditional invariants are compatible with initial transitions) that can be encoded via Farkas’ Lemma or via our novel difference logic encoding presented in the previous section. By making some of these conditions soft with the use of appropriate weights as in [31], we can order the five possible outputs from most desirable (I) to least desirable (V). For example, the optimal solution gives output (III) only if no solution exists that gives results (II) or (I).

The resulting Max-SMT formula can be processed with an off-the-shelf Max-SMT solver, such as Opti-Mathsat [32], Z3Opt [33] or Barcelogic [34]. Unfortunately, we had to discard Opti-Mathsat because it cannot deal with non-linearities. Between the remaining two, it was Barcelogic the one that showed a better performance, probably due to its novel method to deal with non-linearities [11]. Regarding the optimization part, Barcelogic implements a very simple branch-and-bound approach as explained in [35]. Due to its better performance, in what follows only experiments with Barcelogic will be reported.

Experiments were performed on an Intel i5 2.8 GHz CPU with 8 Gb of memory. For each of the 3270 generated queries and each encoding, we consider the best solution obtained within a time limit of 5 sFootnote 7. In Table 1 we can see the output and the running time of four different encodings: Farkas (the standard encoding based on Farkas’ Lemma), FarkasDL (the previous one additionally restricting the templates to be difference logic), FarkasDL- \(\varvec{\lambda }\) (the previous one additionally imposing that the \(\lambda \) multipliers are 0 or 1), and Diff Logic (our novel encoding introduced in the previous section).

Table 1. Results on the 3270 generated queries with a time limit of 5 s.
Full size table

The experiments confirm our intuition that our specialized difference logic encoding outperforms Farkas both in runtime and in quality of solutions. Even if we try to improve Farkas with additional constraints that limit the search space, as in FarkasDL and FarkasDL- \(\varvec{\lambda }\), the differences are still dramatic. We want to remark that in no query Farkas gave a better-quality result than Diff Logic.

More detailed results can be seen in Fig. 5, where in the scatter plots we display the timings (in seconds, logarithmic scale) over queries whose optimal solution finds invariants proving the assertion (a) or disabling a transition (b). One can see that even the best Farkas-based encoding is systematically slower than Diff Logic. We can also observe that in lots of queries Farkas times out, which means that the Max-SMT solver could not prove the solution to be optimal. One could think this is because proving optimality is equivalent to proving unsatisfiability, something at which Barcelogic non-linear techniques are particularly bad. However, a careful inspection of the results reveals the situation is worse, as in more than 80 % of the queries the found solution was not optimal.

Fig. 5.
figure 5

Comparison of Diff Logic and FarkasDL- \(\varvec{\lambda }\) runtimes over queries whose optimal solution gives invariants proving the assertion (a) or disabling a transition (b).

Full size image

4 Finding Invariant Subsets

Another important problem that we need to solve inside VeryMax is the Invariant Subset Selection Problem. Formally, we are given a program, an assertion \((\ell _{ass},\varphi )\) and, for each location \(\ell \in \mathcal{L}\), a set \( Cand (\ell )\) of \(m_{\ell }\) candidate invariants

$$\begin{array}{rrrcl} c_1^{\ell ,1} x_1 + &{} \cdots + &{} c_n^{\ell ,1} x_n &{} \le &{} d^{\ell ,1} \\ \ldots \\ c_1^{\ell ,m_{\ell }} x_1 + &{} \cdots + &{} c_n^{\ell ,m_{\ell }} x_n &{} \le &{} d^{\ell ,m_{\ell }} \end{array} $$

where the \(c_i^{\ell ,j}\) are fixed integer numbers and the \(d^{\ell ,j}\) are integer variables. The goal is to select, if it exists, a subset of \( Cand (\ell )\) for each \(\ell \in \mathcal{L}\), and find an assignment to the \(d^{\ell ,j}\)’s such that (i) the chosen subsets are invariant and (ii) the invariants chosen at \(\ell _{ass}\) imply \(\varphi \).

As in Sects. 2 and 3 we will show that, in the general case, if we use Farkas’ Lemma we obtain a non-linear formula, whereas non-linearities can be avoided when the program, the assertion and the candidate invariants are difference logic. In this case, the resulting formula belongs to linear arithmetic.

4.1 General Case

We can imagine the process of finding a solution as working in two stages. First of all, we have to select a subset of the candidate invariants at each location, together with their corresponding right-hand sides \(d^{\ell ,j}\). After that, we need to ensure that Initiation, Consecution and Assertion conditions are satisfied. To prove these conditions, we only need to find the right Farkas’ multipliers.

More precisely, for each location \(\ell \in \mathcal{L}\) and \(1\le j \le m_{\ell }\), let us consider a Boolean variable \(chosen_{\ell ,j}\) that indicates whether the j-th invariant in \( Cand (\ell )\) is chosen. Additionally, to each coefficient \(c_i^{\ell ,j}\) we will associate a fresh integer variable \(\widehat{c}_i^{\ell ,j}\), and to each \(d^{\ell ,j}\) a fresh integer variable \(\widehat{d}^{\ell ,j}\). The following formulas

$$ \begin{array}{rclcl} chosen_{\ell ,j} &{} \implies &{} \bigwedge \limits _{i=1}^n \widehat{c}_i^{\ell ,j} = c_i^{\ell ,j} &{} \;\;\wedge \;\; &{} \widehat{d}^{\ell ,j} = d^{\ell ,j} \qquad \qquad (3)\\ \lnot chosen_{\ell ,j}&{} \implies &{} \bigwedge \limits _{i=1}^n \widehat{c}_i^{\ell ,j} = 0 &{} \wedge &{} \widehat{d}^{\ell ,j} = 0 \qquad \qquad \quad (4) \end{array} $$

constraint the shape of the invariants depending on whether they are chosen or not. In the following, we will consider that \(\widehat{ Cand }(\ell )\) consists of all elements of \( Cand (\ell )\) where all c’s and d’s have been replaced by their respective \(\widehat{c}\)’s and \(\widehat{d}\)’s.

Let us explain how a Consecution condition will be enforced (for Initiation and Assertion an analogous idea applies). Let \((\ell _S,\tau ,\ell _T)\) be the transition to which consecution refers. We want to enforce that \(\widehat{ Cand }(\ell _S) \wedge \tau \, \models \, \widehat{ Cand }(\ell _T)'\), which amounts to checking, for each \(\widehat{ inv '}\in \widehat{ Cand }(\ell _T)'\), that \(\widehat{ Cand }(\ell _S) \wedge \tau \, \models \, \widehat{ inv '}\), or equivalently, that \(\widehat{ Cand }(\ell _S) \wedge \tau \wedge \lnot \widehat{ inv '}\) is unsatisfiable. The latter can be easily encoded into a non-linear formula by using Farkas’ Lemma.

4.2 Difference Logic Case

Let us now assume that all candidate invariants, the formula in the assertion and the input program are expressed in difference logic. The idea of the encoding is similar. However, in Sect. 4.1 new inequalities were globally introduced standing for the original inequalities or the trivial inequality \(0 \le 0\), depending on whether they had been chosen or not. Instead, here we exploit the fact that in Farkas’ proofs of unsatisfiability of difference sets, multipliers are 0 or 1: for each unsatisfiability proof that must hold, new inequalities are locally introduced, standing for the product of the Farkas’ multiplier with the original inequality.

As an example, let us explain how to encode a Consecution condition referring to a transition \((\ell _S,\tau ,\ell _T)\). The \(chosen_{\ell ,j}\) variables will be as before, common to the overall encoding. However, for each \( inv \in Cand (\ell _T)\), in order to enforce that \( Cand (\ell _S) \wedge \tau \, \models \, inv '\), we will now introduce fresh \(\widehat{c}\)’s and \(\widehat{d}\)’s and add, for \(1\le j \le m_{\ell _S}\), the previous formula (4) and:

$$ ( \bigwedge \limits _{i=1}^n \widehat{c}_i^{\ell _S,j} = 0 \;\wedge \; \widehat{d}^{\ell _S,j} = 0) \;\;\;\;\vee \;\;\;\; ( \bigwedge \limits _{i=1}^n \widehat{c}_i^{\ell _S,j} = c_i^{\ell _S,j} \;\wedge \; \widehat{d}^{\ell _S,j} = d^{\ell _S,j}) $$

The intuition is that \(\widehat{c_1}^{\ell _S,j} x_1 + \cdots + \widehat{c_n}^{\ell _S,j} x_n \le \widehat{d}^{\ell _S,j}\) is the inequality resulting from multiplying \(c_1^{\ell _S,j} x_1 + \cdots + c_n^{\ell _S,j} x_n \le d^{\ell _S,j}\) by the corresponding multiplier in Farkas’ proof of unsatisfiability of \( Cand (\ell _S) \wedge \tau \wedge \lnot inv '\). Similarly, let us assume that \( inv \) is \(c_1 x_1 + \cdots + c_n x_n \le d\), with chosen being the variable that indicates whether we pick it or not. Then we will add the formula

$$ ( \bigwedge \limits _{i=1}^n c_i^{\star } = 0 \;\wedge \; d^{\star } = 0) \;\;\;\;\vee \;\;\;\; ( \bigwedge \limits _{i=1}^n c_i^{\star } = -c_i \;\wedge \; d^{\star } = -1-d), $$

which intuitively means that \(c_1^{\star } x_1 + \cdots + c_n^{\star } x_n \le d\) is the inequality resulting from multiplying \(\lnot (c_1 x_1 + \cdots + c_n x_n \le d) \equiv -c_1 x_1 - \cdots - c_n x_n \le -1-d\) by the corresponding multiplier in the proof of unsatisfiability of \( Cand (\ell _S) \wedge \tau \wedge \lnot inv '\).

The encoding finishes by: (i) applying Farkas’ Lemma to enforce unsatisfiability of \(\widehat{ Cand (\ell _S)} \wedge \tau \wedge c_1^{\star } x'_1 + \cdots + c_n^{\star } x'_n \le d'\) as in the general case, but now assuming that multipliers are 1, which gives a linear formula F; and (ii) adding the implication \(chosen \Rightarrow F\) to the encoding. Detailed experiments comparing the general and the particular encoding for difference logic give similar results to Sect. 3.2, and we omit them here due to lack of space.

A final remark is that the previous encoding can be applied to solve the problem in Sect. 3 by exhaustively considering in \( Cand (\ell )\) all differences of variables. This allows finding simultaneously more than one invariant inequality per location, in particular coinductive invariants. So the price to pay for a complete method is moving from a difference logic to a linear arithmetic formula.

5 Experiments

The goal here is to assess to which extent a constraint-based verifier like VeryMax can be globally improved by incorporating the novel encodings introduced in Sects. 3.1 and 4.2 (for handling safety subqueries and invariant subset selection problems, respectively). Note it is not uncommon that huge enhancements on the runtime of a theorem prover (SAT or SMT solver or first-order theorem prover) get diluted into insignificant improvements on the verifier that uses it.

We compared the original VeryMax safety prover, which uses Farkas as the encoding methodology to find linear invariants, with a new version VeryMaxDL where the problems described in Sects. 3 and 4 are solved using the novel encodings. A time limit of 900 s was given to each problem. Table 2 summarizes the experiments, where for each system we report the number of problems found to be safe (Yes), not found to be safeFootnote 8 (No), proved safe only by this version of the system (Only-yes) and the total runtime (including timeouts).

The results are extremely positive since the runtime is reduced to one third, and the loss of verification power due to generating only difference logic invariants, as opposed to linear invariants, is very limited. We analyzed all problems that VeryMax could prove safe whereas VeryMaxDL could not and they all need linear invariants outside difference logic, which means that they cannot be proved using the techniques on which VeryMaxDL is based.

Table 2. Results comparing VeryMax and VeryMaxDL.
Full size table

Figure 6 contains scatter plots comparing VeryMax and VeryMaxDL on all problems, problems proved safe by VeryMaxDL, and problems not found to be safe by VeryMaxDL. At first glance, although the difference logic version is faster, we observe that the plots are not as clean as the ones of Sect. 3.2. This is not surprising: if the subproblems solved via Farkas or difference logic give different results (e.g. they disable different transitions), the overall behavior of the verification system changes and this has an impact on the overall runtime. The second observation is that VeryMaxDL is faster, independently of whether the problem can be found to be safe or not. This opens the way to run both versions in parallel, or even first run VeryMaxDL and if the program cannot be proved safe, run VeryMax in a second attempt.

Fig. 6.
figure 6

Scatter plots comparing VeryMax and VeryMaxDL.

Full size image

6 Conclusions and Future Work

It is well acknowledged that the current bottleneck in the effectiveness of the constraint-based method compared to other approaches for verification is the technology for solving non-linear constraints. In this paper we have introduced novel encodings that, if we restrict ourselves to programs and invariants in difference logic, allow one to replace non-linear solvers by cheaper ones. Experiments show that this yields a remarkable gain in terms of runtime at the expense of restricting the class of programs under consideration and a certain but acceptable loss of verification power.

As future work, we plan to extend the use of similar encodings in our verification system VeryMax. E.g., finding simple ranking functions in (non)-termination problems is a particularly interesting area where related ideas could be applied.