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

This paper addresses a fundamental problem in automatic program verification: how to prove that a piece of code preserves a given invariant. In Floyd-Hoare style verification this means that we want to automatically prove the validity of the Hoare triple \(\{P\} C \{P\}\) where P is an assertion and C is a command. Alternatively, this can be shown by proving the unsatisfiability of the formula \(P(V) \wedge \delta (V, V') \wedge \lnot P(V')\) (the verification condition) where P(V) denotes the assertion P before the command, \(P(V')\) denotes the assertion P after the command, and \(\delta (V, V')\) is a formula expressing the meaning of the command C as a transition relation between pre- and post-states. When C is a loop body, such a P is an inductive invariant and can be used to prove safety properties of the loop (if it also holds initially and implies the desired property).

For programs with infinite state space, proving the validity of \(\{P\} C \{P\}\) is generally undecidable even when C does not include loops. Indeed, existing SMT solvers can diverge even for simple assertions and simple commands. Recent attempts to apply program verification to prove the correctness of critical system’s design and code [16] identify this as the main hurdle for using program verification.

The difficulty is rooted in powerful constructs used in SMT-based verification of interesting programs. Prominent among these constructs are arithmetic and other program operations modeled using background theories, and logical quantifiers. In this paper we target the verification of applications in which the problem can be modeled without interpreted theories. This is in line with recent works that show that although reasoning about arithmetic is crucial for low-level code, in many cases the verification of high-level programs and designs can be performed by reasoning about quantification in uninterpreted theories. Specifically, the decidable Effectively Propositional logic (EPR) has been successfully applied to domains such as linked-list manipulation [21], Software-Defined Networks [6] and some distributed protocols [29]. Without interpreted theories it remains to address the complications induced by the use of quantifier alternation.

In the presence of quantifier alternation, the solver’s ability to check assertions is hindered by the following issues: (1) an infinite search space of proofs that needs to be explored for correct assertions, a problem which is sometimes manifested in matching loops [12], and (2) a difficulty of finding counterexamples for invalid assertions, notably when counterexamples may be of infinite size. Current SMT techniques often fail to produce models of satisfiable quantified formulas [15, 34], which is somewhat unfortunate since one of the main values of program verification is early detection of flaws in designs and programs. The existence of infinite counterexamples is a major complication as they are difficult to find. In uninterpreted domains, infinite counterexamples usually do not indicate a real violation of the verification conditions and are counterintuitive to programmers, yet render assertions invalid in the context of general first-order logic (on which SMT proof techniques are based). Hence infinite counter-models pose a real problem in the verification process.

Previous work on EPR [6, 21, 29] used universally quantified invariants with programs expressed by \(\exists ^*\forall ^*\) formulasFootnote 1, in which case checking inductive invariants is decidable, hence problems (1) and (2) do not occur. In particular, EPR enjoys the finite-model property and so counterexamples are of finite size. EPR programs are in fact Turing-complete [29], but universal invariants are not always sufficient to express the required program properties.

For example, [16] describes a client server scenario where the invariant is “For every reply message sent by the server, there exists a corresponding request message sent by a client”. (See Example 1 for further details.) This invariant is \({\forall ^*\exists ^*}\) and thus leads to verification conditions with quantifier alternation. This kind of quantifier alternation may lead to divergence of the solver as problems (1) and (2) re-emerge.

The current work aims to expand the applicability of the EPR-based verification approach to invariants of more complex quantification. We focus on the class \(\forall ^*\exists ^*\) invariants, which arise in interesting programs. As we show, checking inductiveness of invariants in this class is undecidable. We thus study problems (1),(2) above for this setting using the notion of bounded quantifier instantiations, which we term Bounded-Horizon.

Main Results. This paper explores the utility of limited quantifier instantiations for checking \(\forall ^*\exists ^*\)invariants, and for dealing with the problems that arise from quantifier alternation: divergence of the proof search and infinite counter-models.

We consider instantiations that are bounded in depth of terms. Bounded instantiations trivially prevent divergence while maintaining soundness. Although for a given bound the technique is not complete, i.e. unable to prove every correct invariant, we provide completeness guarantees by comparing bounded instantiations to the method of instrumentation, a powerful technique implicitly employed in previous works [21, 23, 29]. Instrumentation tackles a \(\forall ^*\exists ^*\)invariant by transforming the program in a way that allows the invariant to be expressed in a universal form, and, accordingly, makes the verification conditions fall in EPR. We show that for invariants that can be proven using a typical form of instrumentation, bounded instantiations of a small bound are also complete. Namely, they are sufficiently powerful to prove the original program without modifications and in a fully automatic way. This is encouraging since instrumentation is labor-intensive and error-prone while bounded instantiations are completely automatic.

This result suggests that in many cases correct \(\forall ^*\exists ^*\)invariants of EPR programs can be proven using a simple proof technique. Typically in such cases tools such as Z3 will also manage to automatically prove the verification conditions. However, bounded instantiations guarantee termination a-priori even when the invariant is not correct. When it terminates, the procedure returns a logical structure which is not necessarily a true counterexample but “approximates” it, as it satisfies all the bounded instantiations. Interestingly, this suggests a way to overcome the problem of infinite models. This problem arises when the user provides an invariant that is correct for finite models but is incorrect in general first-order logic. In such cases, state-of-the-art SMT solvers typically produce “unknown” or timeout since they fail to find infinite models. Thus the user is left with very little aid from the solver when attempting to make progress and successfully verify the program. In contrast, bounded quantifier instantiation can be used to find finite models with increasing sizes, potentially indicating the existence of an infinite model, and provide hints as to the source of the error. This information allows the user to modify the program or the invariant to exclude the problematic models. We demonstrate this approach on a real example in which such a scenario occurred in one of our verification attempts. We show that the provided models assist in identifying and fixing the error, allowing the user to successfully verify the program.

We also implemented a prototype tool that performs bounded instantiations of bound 1, and used it to verify several distributed protocols and heap manipulating programs. The implementation efficiently reduces the problem of checking inductiveness with bound 1 to a Z3 satisfiability check on which the solver always terminates, thereby taking advantage of Z3’s instantiation techniques while guaranteeing termination.

2 Preliminaries

In this section we provide background and explain our notation. \(\varSigma \) will always denote a relational first-order vocabulary, which may contain constant symbols, \(c_i\), and relation symbols, \(r_j\), but no function symbols. For a formula \(\varphi \) we denote by \(\mathop {\text {const}}[\varphi ]\) the set of constants that appear in \(\varphi \). We write that \(\varphi \in \exists ^*(\varSigma )\) to mean that \(\varphi \) is an existential formula defined over vocabulary \(\varSigma \). Similarly, the class of universal formulas is denoted by \(\forall ^*(\varSigma )\). We say that \(\varphi \) is quantifier-free, denoted \(\varphi \in \text{ QF }(\varSigma )\) if it contains no quantifiers, and that it is alternation free, denoted \(\varphi \in \text{ AF }(\varSigma )\), if it can be written as a Boolean combination of formulas in \(\exists ^* (\varSigma )\). \(\text{ FOL }(\varSigma )\) stands for arbitrary first-order formulas over \(\varSigma \). A sentence is a closed formula.

EPR. The effectively-propositional (EPR) fragment of first-order logic, also known as the Bernays-Schönfinkel-Ramsey class, consists of \(\exists ^* \forall ^*(\varSigma )\) sentences. Such sentences enjoy the small model property. Thus satisfiability of EPR sentences is decidable [31].

EPR Transition Relation. We specify a transition relation via an EPR sentence, \(\delta \), over a vocabulary \(\varSigma \uplus \varSigma '\) where \(\varSigma \) is a relational vocabulary used to describe the source state of a transition and \(\varSigma ' = \{a' \mid a \in \varSigma \}\) is used to describe the target state.

Inductive Invariants. A first-order sentence I over \(\varSigma \) is an inductive invariant for \(\delta \) if \(I \wedge \delta \rightarrow I'\) is valid, or, equivalently, if \(I \wedge \delta \wedge \lnot I'\) is unsatisfiableFootnote 2, where \(I'\) results from substituting every constant and relation symbol in I by its primed version.

Skolemization. Let \(\varphi (z_1,\ldots ,z_n) \in \text{ FOL }(\varSigma )\). The Skolemization of \(\varphi \), denoted \({\varphi }_{S}\), is a universal formula over \(\varSigma \uplus {\varSigma }_{S}\), where \({\varSigma }_{S}\) consists of fresh constant symbols and function symbols, obtained as follows. We first convert \(\varphi \) to negation normal form (NNF) using the standard rules. For every existential quantifier \(\exists y\) that appears under the scope of the universal quantifiers \(\forall x_1, \ldots , \forall x_m\), we introduce a fresh function symbol \(f_y \in {\varSigma }_{S}\) of arity \(n+m\). We replace each bound occurrence of y by \(f_y(z_1,\ldots ,z_n,x_1, \ldots , x_m)\), and remove the existential quantifier. If \(n+m = 0\) (i.e., \(\varphi \) has no free variables and \(\exists y\) does not appear in the scope of a universal quantifier) a fresh constant symbol is used to replace y. It is well known that \({\varphi }_{S}\rightarrow \varphi \) is valid and \({\varphi }_{S}\) and \(\varphi \) are equi-satisfiable.

3 Bounded-Horizon

In this section, we define a systematic method of quantifier instantiation called Bounded-Horizon as a way of checking the inductiveness of first-order logic formulas, and explore some of its basic properties. We start with the undecidability of the problem.

Undecidability of Inductiveness. For a universal formula \(I \in \forall ^*(\varSigma )\), checking inductiveness amounts to checking unsatisfiability of an EPR formula, and is therefore decidable. The same holds for \(I \in AF(\varSigma )\). However, this is no longer true when quantifier alternation is introduced. For example, checking inductiveness of \(I \in \forall ^* \exists ^* (\varSigma )\) amounts to checking unsatisfiability of a formula in a fragment for which satisfiability is undecidable. In fact we prove that:

Theorem 1

The problem of determining on input \(I \in \forall ^* \exists ^*(\varSigma )\) and \(\delta \in \exists ^*\forall ^*(\varSigma ,\varSigma ')\), whether I is an inductive invariant for \(\delta \), is undecidable.

Proof Sketch

The proof is by reduction from the halting problem, which can be encoded using a \({\forall ^*\exists ^*}\) formula via tiling (see e.g. [20]). For the setting of checking invariants, we start with a Turing machine M, and construct \(\delta \in \exists ^*\forall ^*(\varSigma ,\varSigma ')\), and \(I \in \forall ^* \exists ^*(\varSigma )\) s.t. I is an inductive invariant for \(\delta \) iff M halts on the empty tape. In case M does not halt, the counter-model that shows that I is not inductive is an infinite structure which encodes an infinite run of M.    \(\square \)

Bounded-Horizon Instantiations. Let \(\delta \in \exists ^{*}\forall ^{*}(\varSigma , \varSigma ')\) be an EPR transition relation and \(I \in \text{ FOL }(\varSigma )\) a candidate invariant. We would like to check the satisfiability of \(I \wedge \delta \wedge \lnot I'\), and equivalently of \(\textit{Ind}= {I}_{S} \wedge {\delta }_{S} \wedge {(\lnot I')}_{S}\). Recall that \({\varphi }_{S}\) denotes the Skolemization of \(\varphi \), and note that \({I}_{S}\) and \({(\lnot I')}_{S}\) possibly add Skolem functions to the vocabulary. Roughly speaking, for a given \(k \in {\mathbb {N}}\), Bounded-Horizon instantiates the universal quantifiers in \(\textit{Ind}\), while restricting the instantiations to produce ground-terms of function nesting at most k.

Below we provide the formal definitions and discuss soundness and (in)completeness. We start with the notion of instantiations, and recall Herbrand’s theorem which establishes completeness of proof by (unrestricted) instantiations. Suppose that some vocabulary \(\tilde{\varSigma }\) including constants and function symbols is understood (e.g., \(\tilde{\varSigma } = \varSigma \uplus {\varSigma }_{S}\), where \({\varSigma }_{S}\) includes Skolem constants and function symbols).

Definition 1

(Instantiation). Let \(\varphi (\overline{x}) \in \forall ^{*}(\tilde{\varSigma })\) be a universal formula with n free variables and m universal quantifiers. An instantiation of \(\varphi \) by a tuple \(\overline{t}\) of \(n+m\) ground terms, denoted by \({\varphi }[\,\overline{t}\,]\), is obtained by substituting \(\overline{t}\) for the free variables and the universally quantified variables, and then removing the universal quantifiers.

Note that an instantiation is a quantifier-free sentence.

Theorem 2

(Herbrand’s Theorem). Let \(\varphi \in \forall ^{*} (\tilde{\varSigma })\). Then \(\varphi \) is satisfiable iff the (potentially infinite) set \(\left\{ {\varphi }[\,\overline{t}\,] \mid \overline{t} \text{ is } \text{ a } \text{ tuple } \text{ of } \text{ ground } \text{ terms } \text{ over } \tilde{\varSigma }\right\} \) is satisfiable.

We now turn to restrict the depth of terms used in instantiations.

Definition 2

(Bounded-Depth Terms). For every \(k \in {\mathbb {N}}\), we define \( BHT _{k}\) to be the set of ground terms over \(\tilde{\varSigma }\) with function symbols nested to depth at most k. \( BHT _{k}\) is defined by induction over k. Let C be the set of constants in \(\tilde{\varSigma }\), F the set of functions, and for every \(f \in F\) let \(\text {Arity}_{f}\) be the arity of f. Then \( BHT _{0} = C\) and for \(k>0\):

$$\begin{aligned} BHT _{k}&= BHT _{k - 1} \cup \{f(t_1, \ldots t_m) \mid f \in F, \ m = \text {Arity}_{f}, \ t_1, \ldots , t_m \in BHT _{k-1} \}. \end{aligned}$$

We will also write \(\overline{t}\in BHT _{k}\) for a tuple of terms \(\overline{t}\), to mean that every entry of \(\overline{t}\) is in \( BHT _{k}\) (the number of elements in \(\overline{t}\) should be clear from the context). Note that the set of ground terms is \( BHT _{\infty }= \bigcup _{k \in {\mathbb {N}}}{ BHT _{k}}\).

Definition 3

(Depth of Instantiation). Let \(\varphi \in \forall ^{*}(\tilde{\varSigma })\) and \(\overline{t} \in BHT _{\infty }\). The depth of instantiation, denoted \(\mathop {\text {depth}}({\varphi }[\,\overline{t}\,])\), is the smallest k such that all ground terms that appear in \({\varphi }[\,\overline{t}\,]\) are included in \( BHT _{k}\).

Bounded-Horizon Algorithm. Given a candidate invariant \(I \in \text{ FOL }(\varSigma )\), a transition relation \(\delta \) over \(\varSigma \uplus \varSigma '\), and \(k \in {\mathbb {N}}\), the Bounded-Horizon algorithm constructs the formula \(\textit{Ind}= {I}_{S} \;\wedge \;{\delta }_{S} \;\wedge \;{(\lnot I')}_{S}\), and checks if the set

$$\begin{aligned} \left\{ {\textit{Ind}}[\,\overline{t}\,] \ | \ \overline{t} \in BHT _{k}, \ \mathop {\text {depth}}({\textit{Ind}}[\,\overline{t}\,]) \le k \right\} \end{aligned}$$
(1)

is unsatisfiable. If it is, then I is provably inductive w.r.t. \(\delta \) with Bounded-Horizon of bound k. Otherwise we report that I is not known to be inductive.

Note that the satisfiability check performed by Bounded-Horizon is decidable since the set of instantiations is finite, and each of them is a ground formula.

Bounded-Horizon for \(\forall ^{*}\exists ^{*}\) Invariants. We illustrate the definition of Bounded-Horizon in the case that \(I \in \forall ^{*}\exists ^{*}(\varSigma )\). Assume that \(I = \forall \overline{x}. \ \exists \overline{y}. \ \alpha (\overline{x}, \overline{y})\) where \(\alpha \in \text{ QF }\). Then \({I}_{S} = \forall \overline{x}. \ \alpha (\overline{x}, \overline{f}(\overline{x}))\) where \(\overline{f}\) are new Skolem function symbols. \({\delta }_{S}\) introduces Skolem constants but no function symbols, and in this case so does \({(\lnot I')}_{S}\). Bounded-Horizon check of bound k can be approximately understood as checking the satisfiability of

$$\begin{aligned} \bigl (\bigwedge _{\overline{t} \in BHT _{k-1}}{{{I}_{S}}[\,\overline{t}\,]}\bigr ) \;\wedge \;\bigl (\bigwedge _{\overline{t} \in BHT _{k}}{{{\delta }_{S}}[\,\overline{t}\,]}\bigr ) \;\wedge \;\bigl (\bigwedge _{\overline{t} \in BHT _{k}}{{{\bigl (\lnot I'\bigr )}_{S}}[\,\overline{t}\,]}\bigr ). \end{aligned}$$
(2)

(In fact, it is possible that \({I}_{S}\) contains sub-formulas for which instantiations of depth k do not increase the total depth of instantiations beyond k, and are thus also included.)

Lemma 1

(Soundness). For every \(k \in {\mathbb {N}}\), Bounded-Horizon with bound k is sound, i.e., if it reports that \(I \in \text{ FOL }(\varSigma )\) is inductive w.r.t. \(\delta \), then I is indeed inductive.

Proof

Assume that I is not inductive w.r.t. \(\delta \), so there is a structure \(\mathcal{A}\) such that \(\mathcal{A}\models {I}_{S} \;\wedge \;{\delta }_{S} \;\wedge \;{(\lnot I')}_{S}\). In particular \(\mathcal{A}\models {\textit{Ind}}[\,\overline{t}\,]\) for every \(\overline{t} \in BHT _{\infty }\) and in particular for every \(\overline{t} \in BHT _{k}\) such that \(\mathop {\text {depth}}({\textit{Ind}}[\,\overline{t}\,]) \le k\). Hence, Bounded-Horizon of bound k will not report that I is inductive.    \(\square \)

Fig. 1.
figure 1

Example demonstrating a \(\forall ^*\exists ^*\) invariant that is provable with bound 1. The reader should first ignore the instrumentation code denoted by \(/@\) (see Example 2). This example is inspired by [16]. The complete program is provided in [2] (files client_server_ae.ivy, client_server_instr.ivy).

Full size image

Example 1

Figure 1 presents a simple model of the client server scenario described in [16]. The program induces an EPR transition relation, and its invariant is provable by Bounded-Horizon of bound 1.

We first explain this example ignoring the annotations denoted by “\(/@\)”. The system state is modeled using three binary relations. The \({\textit{req}}\) relation stores pairs of users and requests, representing requests sent by users. The \({\textit{resp}}\) relation similarly stores pairs of users and replies, representing replies sent back from the server. The \({\textit{match}}\) relation maintains the correspondence between a request and its reply.

The action new_request models an event where a user \( u \) sends a new request to the server. The action respond models an event where the server responds to a pending request by sending a reply to the user. The request and response are related by the \({\textit{match}}\) relation. The action check is used to verify the safety property that every response sent by the server has a matching request, by aborting the system if this does not hold.

A natural inductive invariant for this system is

$$I = \forall u , p . \; {\textit{resp}}( u , p ) \rightarrow \exists q . \; {\textit{req}}( u , q ) \wedge {\textit{match}}( q , p ).$$

The invariant proves that the then branch in action check will never happen and thus the system will never abort. This invariant is preserved under execution of all actions, and is provable by Bounded Horizon of bound 1.

Lemma 2

(Completeness for some k ). If \(I \in \text{ FOL }(\varSigma )\) is inductive w.r.t. \(\delta \) then there exists \(k \in {\mathbb {N}}\) s.t. I is provably inductive w.r.t. \(\delta \) with Bounded-Horizon of bound k.

Proof

From Theorem 2 and compactness there is a finite set S of instantiations that is unsatisfiable. Take k to be the maximal depth of instantiations in S.    \(\square \)

For example, if \(I \in \forall ^{*}\) then Bounded-Horizon of bound 0 is complete. However, as expected due to the undecidability of checking inductiveness, for arbitrary invariants Bounded-Horizon is not necessarily complete for a given k: An example for which a bound of 1 is insufficient appears in the extended version [1].

Small Bounded-Horizon for \(\forall ^{*}\exists ^{*}\) Invariants. Despite the incompleteness, we conjecture that a small depth of instantiations typically suffices to prove inductiveness. The intuition is that an EPR transition relation has a very limited “horizon” of the domain: it interacts only with a small fraction of the domain, namely elements pointed to by program variables (that correspond to logical constants in the vocabulary).

When performing the Bounded-Horizon check with bound 1 on a \(\forall ^* \exists ^*\) invariant \(I = \forall \overline{x}. \ \exists \overline{y}. \ \alpha (\overline{x}, \overline{y})\), we essentially assume that the existential part of the invariant \(\psi (\overline{x}) = \ \exists \overline{y}. \ \alpha (\overline{x}, \overline{y})\) holds on all program variables—but not necessarily on all elements of the domain — and try to prove that it holds on all elements of the domain after the transition. We expect that for most elements of the domain, the correctness of \(\psi \) is maintained simply because they were not modified at all by the transition. For elements that are modified by the transition, we expect the correctness after modifications to result from the fact that \(\psi \) holds for the elements of the domain that the transition directly interacts with. If this is indeed the reason that \(\psi \) is maintained, a bound of 1 sufficiently uses \(\psi \) in the pre-state to prove the invariant in the post-state, i.e. it is inductive.

This is the case in Example 1. Additional examples are listed in Sect. 6.

4 Power of Bounded-Horizon for Proving Inductiveness

We now turn to investigate the ability of Bounded-Horizon to verify inductiveness. In this section we provide sufficient conditions for its success by relating it to the notion of instrumentation (which we explain below). We show that Bounded-Horizon with a low bound of 1 or 2 is as powerful as a natural class of sound program instrumentations, those that do not add existential quantifiers. Section 6 demonstrates the method’s power on several interesting programs we verified using Bounded-Horizon of bound 1.

4.1 Instrumentation

We present our view of the instrumentation procedure used in previous works [21, 23, 29] to eliminate the need for quantifier-alternation, thus reducing the verification task to a decidable fragment. The procedure begins with a program that induces a transition relation \(\delta \in {\exists ^*\forall ^*}(\varSigma \cup \varSigma ')\). The purpose of instrumentation is to modify \(\delta \) into another transition relation \(\widehat{\delta }\) that admits an inductive invariant with simpler quantification (e.g., universal, in which case it is decidable to check). We note that instrumentation is generally a manual procedure. For simplicity, we describe the instrumentation process informally, but provide the semantic soundness requirement in Definition 4. The instrumentation procedure consists of the following three steps:

  1. 1.

    Identify a formula \(\psi ({\overline{x}}) \in \text{ FOL }(\varSigma )\) (usually \(\psi \) will be existential) that captures information that is needed in the inductive invariant. Extend the vocabulary with an instrumentation relation \(r({\overline{x}})\) that intentionally should capture the derived relation defined by \(\psi ({\overline{x}})\). Let \(\widehat{\varSigma }= \varSigma \cup \{r\}\) denote the extended vocabularyFootnote 3.

  2. 2.

    Add update code that updates r when the original (“core”) relations are modified, and maintains the meaning of r as encoding \(\psi \). The update code must not block executions of real code, and can possibly be a sound approximation. Sometimes it can be generated automatically via finite differencing [32].

  3. 3.

    Modify the program to use r. Often this is performed by rewriting some program conditions, keeping in mind that r encodes \(\psi \). This means replacing some quantified expressions by uses of r.

Example 2

In the example of Fig. 1, to achieve a universal invariant we add an instrumentation relation \({\textit{r}}\) defined by \({\textit{r}}(x,y) \equiv \exists z. \ {\textit{req}}(x,z) \wedge {\textit{match}}(z,y)\) (step 1). The simple form of \(\psi \) allows us to obtain precise update code, which appears as annotations marked with \(/@\) in lines that mutate \({\textit{req}}\) and \({\textit{match}}\) (step 2). We also replace the \(\texttt {if}\) condition in the action check by an equivalent condition that uses \({\textit{r}}\) (step 3). The line marked with \(/@\hookrightarrow \) in the check action replaces the line above it. The resulting program has the invariant \(\widehat{I}= \forall u , p . \; {\textit{resp}}( u , p ) \rightarrow {\textit{r}}( u , p )\), which is universal.

Let \(\widehat{\delta }\in {\exists ^*\forall ^*}(\widehat{\varSigma }\cup \widehat{\varSigma }')\) denote the transition relation induced by the modified program (modifications occur in steps 2, 3). The soundness of the instrumentation procedure is formalized in the following connection between \(\psi \), \(\delta \), and \(\widehat{\delta }\):

Definition 4

(Sound Instrumentation). \(\widehat{\delta }\in {\exists ^*\forall ^*}(\widehat{\varSigma }\cup \widehat{\varSigma }')\) is a sound instrumentation for \(\delta \in {\exists ^*\forall ^*}(\varSigma \cup \varSigma ')\) and \(\psi \in \text{ FOL }(\varSigma )\) if \(\bigl (\forall {\overline{x}}. \; r({\overline{x}}) \leftrightarrow \psi ({\overline{x}}) \;\wedge \;\delta \;\wedge \;\forall {\overline{x}}. \; r'({\overline{x}}) \leftrightarrow \psi '({\overline{x}})\bigr ) \rightarrow \widehat{\delta }\) is valid, or equivalently, \(\delta \rightarrow \widehat{\delta }[\psi / r, \psi ' / r']\) is valid.

Definition 4 ensures that the instrumented program includes at least all the behaviors of the original program, when r is interpreted according to \(\psi \). Thus, if the instrumented program is safe, then it is sound to infer that the original program is safe.

The instrumentation procedure does not require the user to know an inductive invariant for the original program. However, if a sound instrumentation which leads to an invariant exists, then an inductive invariant for the original \(\delta \) can be produced by substituting back the “meaning” of r as \(\psi \) (thus, safety of the original program is implied):

Lemma 3

Let \(\widehat{\delta }\) be a sound instrumentation for \(\delta \) and \(\psi \), and \(\widehat{I}\in \text{ FOL }(\widehat{\varSigma })\) be an inductive invariant for \(\widehat{\delta }\). Then \(I = \widehat{I}[\psi / r]\) is inductive w.r.t. \(\delta \).

Proof

\(\widehat{I}\wedge \widehat{\delta }\rightarrow \widehat{I}'\) is valid, thus, so is \((\widehat{I}\wedge \widehat{\delta }\rightarrow \widehat{I}')[\psi /r,\psi '/r']\). \(\widehat{\delta }\) is a sound instrumentation for \(\delta \), so (using Definition 4) \({I} \wedge {\delta } \rightarrow {I}'\) is valid.    \(\square \)

Note that typically the quantification structure of I is more complex than that of \(\widehat{I}\).

Instrumentation Without Additional Existential Quantifiers. In order to relate instrumentation to Bounded-Horizon instantiations, we consider the typical case where the instrumentation process of \(\delta \) does not add new existential quantifiers to \(\widehat{\delta }\). This happens when the update code does not introduce additional existential quantifiers. Formally:

Definition 5

(Existential Naming). Let \(\widehat{\delta }= \exists z_1, \ldots z_m. \ \varphi (z_1, \ldots , z_m)\) where \(\varphi \in \forall ^{*}(\widehat{\varSigma },\widehat{\varSigma }')\). An existential naming \(\eta \) for \((\widehat{\delta },\delta )\) is a mapping \(\eta : \{z_1, \ldots , z_m\} \rightarrow \mathop {\text {const}}[{\delta }_{S}] \cup \mathop {\text {const}}[{\widehat{\delta }}_{S}]\). We define \(\eta (\widehat{\delta })\) to be \(\varphi [\eta (z_1) / z_1, \ldots , \eta (z_m) / z_m]\).

An existential naming provides a Skolemization procedure which uses existing constants rather than fresh ones. If such \(\eta \) exists, it maps the (Skolemized) existential quantifiers in \(\widehat{\delta }\) to their counterparts in \(\delta \). For example, the instrumentation in Fig. 1 results in \(\widehat{\delta }\) that has an existential naming w.r.t. the original \(\delta \). Note that it is possible that \(\widehat{\delta }\) has in fact fewer existential quantifiers than \(\delta \), for example due to the rewriting of conditions (as happens in the example of Fig. 1—see the if statement in action check).

Definition 6

(Instrumentation Without Additional Existenials). \(\widehat{\delta }\) is a sound instrumentation without additional existentials for \(\delta \) if there exists an existential naming \(\eta \) such that \({\delta }_{S} \rightarrow \eta (\widehat{\delta })[\psi / r,\psi ' / r']\) is valid.

4.2 From Instrumentation to Bounded-Horizon

The results described in this section show that if there is an instrumentation without additional existentials, then Bounded-Horizon with a low bound is able to prove the original invariant, without specific knowledge of the instrumentation and without manual assistance from the programmer. This is the case in the example of Fig. 1, which admits an instrumentation that transforms the invariant to a universal invariant (see Example 2) in a form that matches Theorem 3, and indeed the original invariant is provable by Bounded-Horizon of bound 1.

Interestingly, in case Bounded-Horizon with a small bound does not prove inductiveness (see the example in the extended version [1]), the results imply that either the invariant is not inductive or no instrumentation that does not add existential quantifiers can be used to show that it is inductive (even with the programmer’s manual assistance).

In the remainder of this section we will assume that \(\widehat{\delta }\) is a sound instrumentation without additional existentials for \(\delta \), and \(\eta \) is the corresponding naming of existentials. Further, we assume that \(\widehat{I}\) is an inductive invariant for \(\widehat{\delta }\) and denote \(I = \widehat{I}[\psi / r]\).

The following theorems state our results for \(I \in {\forall ^*\exists ^*}\).

Theorem 3

Let \(\widehat{I}\in \forall ^{*}\). Assume \(\psi \in \exists ^{*}\) and r appears only positively in \(\widehat{I}\), or \(\psi \in \forall ^{*}\) and r appears only negatively in \(\widehat{I}\). Then \(I = \widehat{I}[\psi / r]\) is inductive for \(\delta \) with Bounded-Horizon of bound 1. (Note that \(I \in \forall ^* \exists ^*\).)

Proof Sketch

Let \(I = \forall \overline{x}. \ \alpha (\overline{x})\) where \(\alpha \in \exists ^*\). Assume for the sake of contradiction that I is not inductive for \(\delta \) with Bounded-Horizon of bound 1. By the assumptions on \(\psi \) and \(\widehat{I}\), this means that there is a structure \(\mathcal{A}\) such that

$$ \textstyle \mathcal{A}\models \bigl (\bigwedge _{\overline{c}}{\alpha (\overline{c})}\bigr ) \;\wedge \;{\delta }_{S} \;\wedge \;{(\lnot I')}_{S}. $$

From the assumption (Definition 6) and properties of Skolemization, it follows that

$$ \textstyle \mathcal{A}\models \bigl (\bigwedge _{\overline{c}}{\alpha (\overline{c})}\bigr ) \;\wedge \;\bigl (\eta (\widehat{\delta })\bigr )[\psi / r,\psi ' / r'] \;\wedge \;\bigl ({(\lnot \widehat{I}')}_{S}\bigr )[\psi /r, \psi '/r']. $$

From the assumptions on the way \(\psi \) appears in \(\widehat{I}\), when we write \(\widehat{I} = \forall \overline{x}. \ \widehat{\alpha } (\overline{x})\) where \(\widehat{\alpha } \in \text{ QF }\) we have \(\alpha = \widehat{\alpha }[\psi /r]\). Thus, from properties of substitution (interpreting \(r, r'\) according to \(\psi ,\psi '\) in \(\mathcal{A}\)) it follows that there is a structure \(\widehat{A}\) such that

$$ \textstyle \widehat{{\mathcal{A}}} \models \bigl (\bigwedge _{\overline{c}}{\widehat{\alpha }(\overline{c})}\bigr ) \;\wedge \;\eta (\widehat{\delta }) \;\wedge \;{(\lnot \widehat{I}')}_{S}. $$

By reducing \(\widehat{\mathcal{A}}\)’s domain to the constants we have that \( \bigl (\forall \overline{x}. \ \widehat{\alpha }(\overline{x})\bigr ) \wedge \eta (\widehat{\delta }) \wedge {(\lnot \widehat{I}')}_{S} \) is satisfiable. (This is a use of complete instantiation for universal formulas.)

This in turn implies (by properties of Skolemization) that \(\widehat{I} \wedge \widehat{\delta }\wedge \lnot \widehat{I}'\) is satisfiable, which is a contradiction to the assumption that \(\widehat{I}\) is inductive for \(\widehat{\delta }\).    \(\square \)

Theorem 4

Let \(\widehat{I}\in \forall ^{*}\). If \(\psi \in \text{ AF }\) then \(I = \widehat{I}[\psi / r]\) is inductive for \(\delta \) with Bounded-Horizon of bound 2. (Note that \(I \in \forall ^* \exists ^*\).)

The following theorem generalizes the above result to 1-alternation invariants. A formula is 1-alternation if it can be written as a Boolean combination of \(\forall ^* \exists ^*\) formulas.

Theorem 5

Let \(\widehat{I}\in \text{ AF }\). If \(\psi \in \text{ AF }\) then \(I = \widehat{I}[\psi / r]\) is inductive for \(\delta \) with Bounded-Horizon of bound 2. (Note that \(I \in \text{1-alternation }\).)

The full proofs appear in the extended version [1]. The results of this section also apply when multiple instrumentation relations \(\psi _1, \ldots , \psi _t \in \text{ FOL }(\varSigma )\) are simultaneously substituted instead of the relation symbols \(r_1, \ldots , r_t\) in \(\widehat{\delta }\) and \(\widehat{I}\).

Instrumentations for Higher Bounds. While instrumentation that does not add existentials is at most as powerful as Bounded-Horizon with a low bound, sound instrumentations that do add existentials to the program (thereby not satisfying Definition 6) can be used to simulate quantifier instantiation of an arbitrary depth. A simple way is to add r as an instrumentation that tracks the existential part of a \({\forall ^*\exists ^*}\) invariant. Instantiations are performed by introducing existentially quantified variables to the program and using \(\texttt {assume}\) statements to make these variables function as witnesses for a tuple of variables that instantiate the universal quantifiers. Doing this recursively generates instantiations of an arbitrary depth. See the extended version [1] for further details.

5 Partial Models for Understanding Non-Inductiveness

When conducting SMT-based deductive verification (e.g., using Dafny [26]), the user constructs both the formal representation of the system and its invariants. In many cases, the invariant I is initially not inductive w.r.t. the given program, due to a bug in the program or in the invariant. Therefore, deductive verification is typically an iterative process in which the user attempts to prove inductiveness, and, when this fails, adapts the program, the invariant, or both.

In such scenarios, it is extremely desirable to present the user with a counterexample to induction in the form of a state that satisfies I but makes a transition to a state that violates it. Such a state can be obtained from a model of the formula \(\textit{Ind}= I \wedge \delta \wedge \lnot I'\) which is used to check inductiveness. It explains the error, and guides the user towards fixing the program and/or the invariant [13, 26]. However, in many cases where the check involves quantifier alternation, current SMT solvers are unable to produce counterexamples. Instead, SMT solvers usually diverge or report “unknown” [15, 33]. In such cases, Bounded-Horizon instantiations can be used to present a concrete logical structure which is comprehensible to the user, and is obtained as a model of the (finite) instantiations of the formula \(\textit{Ind}\). While this structure is not a true counterexample (as it is only a model of a subset of the instantiations of the formula), it can still guide the user in the right direction towards fixing the program and/or the invariant.

Fig. 2.
figure 2

Leader-election in a ring protocol as an illustration of the use of partial models for incorrect programs and invariants. (a) sketches the protocol (the complete program appears in [2], file ring_leader_termination.ivy). (b), (c) show partial models of bound 1 and 2, respectively, and (d) illustrates an infinite structure that explains the root cause of the non-inductiveness.

Full size image

We illustrate this using a simple leader-election protocol in a ring [10], whose model is presented in Fig. 2(a). The protocol assumes that nodes are organized in a directional ring topology with unique IDs, and elects the node with the highest ID as the leader. Each node sends its own ID to its successor, and forwards messages when they contain an ID higher than its own ID. A node that receives its own ID is elected as leader. We wish to prove a termination property which states that once all nodes have sent their ID, and there are no pending messages in the network, then there is an elected leader. To verify this we use a relational model of the protocol similar to [29], and specify the property via the following formula:

$$\begin{aligned} \left( \exists n. \ {\textit{leader}}(n)\right) \vee \left( \exists n_1,n_2. \ \lnot {\textit{sent}}(n_1) \vee {\textit{pending}}(n_1,n_2)\right) \end{aligned}$$
(3)

A natural attempt of proving this using an inductive invariant is by conjoining Eq. (3) (which is not inductive by itself) with the following property (this was the authors’ actual next step in proving this termination property):

$$\begin{aligned} \forall n_1. \ {\textit{sent}}(n_1) \wedge \lnot {\textit{leader}}(n_1) \rightarrow \left( \left( \exists n_2.\ {\textit{pending}}(n_1,n_2)\right) \vee \left( \exists n_2.\ n_1 < n_2\right) \right) \end{aligned}$$
(4)

meaning that if a node has sent its own ID but has not (yet) become leader, then there is either a message pending in the network with the node’s ID, or a node with a higher ID.

Alas, the conjunction of Eqs. (3) and (4) is still not an inductive invariant for the protocol (as we explain below). Since Eq. (4) contains \({\forall ^*\exists ^*}\) quantification, the associated inductiveness check is outside of the decidable EPR fragment. Indeed, Z3 diverges when it is used to check \(\textit{Ind}\). This is not surprising since the formula has no satisfying finite structures, but has an infinite model (a scenario that is not unusual for \({\forall ^*\exists ^*}\) formulas).

On the other hand, applying Bounded-Horizon (with any bound) to \(\textit{Ind}\) results in a formula that has finite models. These concrete models are partial models of \(\textit{Ind}\). Figure 2(b) and (c) show partial models (restricted to the pre-states) obtained with bounds of 1 and 2, respectively, on this example.

These models are not true counterexamples to induction: the sub-formula of Eq. (4) residing under the universal quantifier does not hold for all the elements of the domain. It does, however, hold for all elements with which the quantifier was instantiated, which are the elements above the dashed line. These elements have all sent their own ID, which was blocked by their successor that has a higher ID, so none of them is the leader. In a finite model, this has to end somewhere, because one of the nodes must have the highest ID. Hence, no finite counter-model exists. However, extrapolating from Fig. 2(b) and (c), we can obtain the infinite model depicted in Fig. 2(d). This model represents an infinite (“open”) ring in which each node has a lower ID than its successor. This model is a true model of the formula \(\textit{Ind}\) generated by the invariant in Eqs. (3) and (4), but the fact that it is infinite prevented Z3 from producing it.

Since we use tools that check general (un)satisfiability, which is not limited to finite structures, the only way to prove that an invariant is inductive is to exclude infinite counterexamples to induction as well. Using Bounded-Horizon instantiations, we are able to obtain meaningful partial models that provide hints to the user about what is missing. In this case, the solution is to add an axiom to the system model which states that there is a node with maximal ID: \(\exists n_1. \ \forall n_2. \ n_2 \le n_1\). With this additional assumption, the formula \(\textit{Ind}\) is unsatisfiable so the invariant is inductive, and this is proven both by Z3’s instantiation heuristics and by Bounded-Horizon with a bound of 1. This illustrates the usefulness of Bounded-Horizon when the invariant is not inductive.

6 Implementation and Initial Evaluation

We implemented a prototype of Bounded-Horizon of bound 1 on top of Z3 [11] and used it within Ivy [29] and the framework of [21]. We applied the procedure to the incorrect example of Sect. 5, and successfully verified several correct programs and invariants using bound 1. These examples are (the examples’ code can be found in [2]):

  • The client-server example of Fig. 1.

  • List reverse [21], where the invariant states that the n edges (“next” pointers) are reversed. The invariant is \(\forall ^* \exists ^*\) due to the encoding of n via \({n^*}\) as explained in [21].

  • Learning switch [6], where the invariant states every routing node has a successor.

  • Hole-punching firewall [6], where the invariant states that every allowed external node was contacted by some internal node. We explored two modeling alternativies: using a ghost history relation, or existensially quantifying over time.

  • Leader election in a ring [10, 29] with the invariant discussed in Sect. 5.

Table 1. Experimental results.
Full size table

An initial evaluation of the method’s performance appears in Table 1.

Our implementation works by adding “guards” that restrict the range of universal quantifiers to the set of constants where necessary. Technically, recall that we are considering the satisfiability of \(\textit{Ind}= {I}_{S} \wedge {\delta }_{S} \wedge {(\lnot I')}_{S}\). Let \(\forall x. \ \theta \) be a subformula of \(\textit{Ind}\). If \(\theta \) contains function symbol applicationsFootnote 4, we transform the subformula to \(\forall x. \ \bigl (\bigvee _{c}{x = c}\bigr ) \rightarrow \theta \) where c ranges over \(\mathop {\text {const}}[\textit{Ind}]\). The resulting formula is then dispatched to the solver. This is a simple way to encode the termination criterion of bound 1 while leaving room for the solver to perform the necessary instantiations cleverly. The translation enlarges the formula by O(#Consts \(\cdot \) #\(\forall \)) although the number of bounded instantiations grows exponentially with #\(\forall \). The exponential explosion is due to combinations of constants in the instantiation, a problem we defer to the solver.

Z3 terminates on the class of formulas because during the Model-Based Quantifier Instantiation process every instantiation of a universally quantified formula has the same truth value in the model as an instantiation using one of the existing ground terms (constants and then \( BHT _{1}\) terms). Z3’s instantiation engine will produce instantiations using existing terms rather than create superfluous new terms [8].

The results are encouraging because they suggest that the termination strategy of Bounded-Horizon, at least for bound 1, can be combined with existing instantiation techniques to assure termination with only a slight performance penalty. Most encouraging is the satisfiable example of Sect. 5. On this instance, Z3 was able to return “sat” within seconds, although to do so, in theory, the solver must exhaust the entire set of bounded instantiations. This suggests that the Bounded-Horizon termination criterion might indeed be useful for “sat” instances on which the solver may diverge.

A different approach to the implementation is to integrate the termination criterion of the bound with the solver’s heuristics more closely (see [7]).

7 Related Work

Quantifier Instantiation. The importance of formulas with quantifier-alternations for program verification has led to many developments in the SMT and theorem-proving communities that aim to allow automated reasoning with quantifier-alternations. The Simplify system [12] promoted the practical usage of quantifier triggers, which let the user affect the quantifier instantiation in a clever way. Similar methods are integrated into modern SMT solvers such as Z3 [11]. Recently, a method for annotating the source code with triggers has been developed for Dafny [27]. The notion of instantiation depth is related to the notions of matching-depth [12] and instantiation-level [14] which are used for prioritization within the trigger-based instantiation procedure.

In addition to user-provided triggers, many automated heuristics for quantifier instantiation have been developed, such as Model-Based Quantifier Instantiation [15]. Even when quantifier instantiation is refutation-complete, it is still important and challenging to handle the SAT cases, which are especially important for program verification. Accordingly, many works (e.g., [33]) consider the problem of model finding.

Local Theory Extensions and Psi-Local Theories [7, 19, 36] identify settings in which limited quantifier instantiations are complete. They show that completeness is achieved exactly when every partial model can be extended to a (total) model. In such settings Bounded-Horizon instantiations are complete for invariant checking. However, Bounded-Horizon can also be useful when completeness cannot be guaranteed.

Classes of SMT formulas that are decidable by complete instantiations have been studied by [15]. In the uninterpreted fragment, a refined version of Herbrand’s Theorem generates a finite set of instantiations when the dependencies are stratified. Bounded-Horizon is a way to bound unstratified dependencies.

Natural Proofs. Natural proofs [30] provide a sound and incomplete proof technique for deductive verification. The key idea is to instantiate recursive definitions over the terms appearing in the program. Bounded-Horizon is motivated by a similar intuition, but focuses on instantiating quantifiers in a way that is appropriate for the EPR setting.

Decidable Logics. Different decidable logics can be used to check inductive invariants. For example, Monadic second-order logic [17] obtains decidability by limiting the underlying domain to consist of trees only, and in particular does not allow arbitrary relations, which are useful to describe properties of programs. There are also many decidable fragments of first-order logic [9]. Our work aims to transcend the class of invariants checkable by a reduction to the decidable logic EPR. We note that the example of Sect. 5 does not fall under the Loosely-Guarded Fragment of first-order logic [18] due to a use of a transitivity axiom, and does not enjoy the finite-model property.

Abstractions for Verification of Infinite-State Systems. Our work is closely related to abstractions of infinite state systems. These abstractions aim at automatically inferring inductive invariants in a sound way. We are interested in checking if a given invariant is inductive either for automatic and semi-automatic verification.

The View-Abstraction approach [3,4,5] defines a useful abstraction for the verification of parameterized systems. This abstraction is closely related to universally quantified invariants. An extension of this approach [5] adds contexts to the abstraction, which are used to capture \({\forall ^*\exists ^*}\) invariants in a restricted setting where nodes have finite-state and are only related by specific topologies. Our work is in line with the need to use \({\forall ^*\exists ^*}\) invariants for verification, but applies in a more general setting (with unrestricted high-arity relations) at the cost of losing completeness of invariant checking.

Our work is related to the TVLA system [28, 35] which allows the programmers to define instrumentation relations. TVLA also employs finite differencing to infer sound update code for updating instrumentation relations [32], but generates non-EPR formulas and does not guarantee completeness. The focus operation in TVLA implements materialization which resembles quantifier-instantiation. TVLA shows that very few built-in instrumentation relations can be used to verify many different programs.

Instrumentation and Update Formulas. The idea of using instrumentation relations and generating update formulas is not limited to TVLA and was also used for more predictable SMT verification [24, 25].

8 Conclusion

We have provided an initial study of the power of bounded instantiations for tackling quantifier alternation. This paper shows that quantifier instantiation with small bounds can simulate instrumentation. This is a step in order to eliminate the need for instrumenting the program, which can be error-prone. The other direction, i.e. simulating quantifier instantiation with instrumentation, is also possible but is less appealing from a practical point of view, and is presented in the extended version [1].

We are encouraged by our initial experience that shows that various protocols can be proven with small instantiation bounds, and that partial models are useful for understanding the failures of the solver to prove inductiveness. Some of these failures correspond to non-inductive claims, especially those due to infinite counterexamples. In the future we hope to leverage this in effective deductive verification tools, and explore meaningful ways to display infinite counterexamples to the user.