Inferring Inductive Invariants from Phase Structures

TL;DR

This paper introduces a user-guided approach to automatically infer inductive invariants for infinite-state systems, especially distributed protocols, by leveraging phase structures to improve inference success.

Contribution

It proposes a novel method that uses phase invariants and user-specified phase structures to guide invariant inference, enhancing applicability to complex infinite-state systems.

Findings

User guidance with phase structures improves inference success.

The approach aligns with domain experts' intuitive reasoning.

Results outperform existing invariant inference techniques.

Abstract

Infinite-state systems such as distributed protocols are challenging to verify using interactive theorem provers or automatic verification tools. Of these techniques, deductive verification is highly expressive but requires the user to annotate the system with inductive invariants. To relieve the user from this labor-intensive and challenging task, invariant inference aims to find inductive invariants automatically. Unfortunately, when applied to infinite-state systems such as distributed protocols, existing inference techniques often diverge, which limits their applicability. This paper proposes user-guided invariant inference based on phase invariants, which capture the different logical phases of the protocol. Users conveys their intuition by specifying a phase structure, an automaton with edges labeled by program transitions; the tool automatically infers assertions that hold in the automaton's states, resulting in a full safety proof.The additional structure from phases guides the inference procedure towards finding an invariant. Our results show that user guidance by phase structures facilitates successful inference beyond the state of the art. We find that phase structures are pleasantly well matched to the intuitive reasoning routinely used by domain experts to understand why distributed protocols are correct, so that providing a phase structure reuses this existing intuition.

Tables

Table 1. Table 1 : Running times in seconds of PDR ∀ superscript PDR for-all \text{PDR}^{\forall} and Phase- PDR ∀ superscript PDR for-all \text{PDR}^{\forall} , presented as the mean and standard deviation (in parentheses) over 16 different Z3 random seeds. “ ∗ ” indicates that some runs did not converge after 1 hour and were not included in the summary statistics. “> 1 hour” means that no runs of the algorithm converged in 1 hour. #p refers to the number of phases and #v to the number of view quantifiers in the phase structure. #r refers to the number of relations and |a| to the maximal arity. The remaining columns describe the inductive invariant/phase invariant obtained in inference. |f| is the maximal frame reached. #c, #q, #l are the mean number of clauses, quantifiers (excluding view quantifiers) and literals per phase, ranging across the different phases.

Program	${\text{PDR}}^{\forall }$	Phase-${\text{PDR}}^{\forall }$	#p	#v	#r	|a|	Inductive				Phase-Inductive
							|f|	#c	#q	#l	|f|	#c	#q	#l
Lock service (single lock)	2.21 (00.03)	0.67 (0.01)	4	1	5	1	11	9	15	21	6	3–4	3–4	3–6
Lock service (multiple locks)	2.73 (00.02)	1.06 (0.01)	4	1	5	2	11	9	24	21	6	4	3–4	4–6
Consensus	60.54 (2.95)	1355 (570)∗	3	1	7	2	9	6	15	15	12	5–6	10–14	9–15
KV (basic)	1.79 (0.02)	1.59 (0.02)	2	1	3	3	5	7	27	19	5	4	9–10	8–9
Ring leader	152.44 (39.41)	2.53 (0.04)	2	2	4	3	6–7	6	11	16	5	1–2	0–1	1–4
KV-R	2070 (370)∗	372.5 (35.9)	2	1	7	5	12–15	24	156	106	11–13	5–11	15–67	12–52
Cache coherence	> 1 hour	90.1 (0.82)	10	1	11	2	n/a	n/a	n/a	n/a	13	10–15	12–27	14–39

Equations

$$\text{Init}⟹\left(\forall \mathcal{V}.\underset{q_0\in {\mathcal{Q}}_0}{\bigvee }{\phi }_{q_0}\right).$$

$$\forall \mathcal{V}.\left({\phi }_q⟹\mathcal{P}\right)$$

$$\text{Init}⟹\left(\forall \mathcal{V}.I_{\iota }\right)$$

$$\text{Inductiveness.}\text{ For every }(q,p)\in \mathcal{R}:$$

$$\text{Edge Covering.}\text{ For every }q\in \mathcal{Q}:$$

$$\text{Safety.}\text{For every }q\in \mathcal{Q}:$$

$$\forall\mathcal{V}.\ \bigg{(}I_{q}\land{\textit{TR}}_{a}\Longrightarrow\bigvee_{(q,p)\in\mathcal{R}}{g^{(q,p)}_{a}}\bigg{)}.$$

$${\delta }_{(q,p)}^{\prime }={\delta }_{(q,p)}\wedge \underset{p^{\prime }<p}{\bigwedge }\neg {\delta }_{(q,p^{\prime })}$$

$$\forall \mathcal{V}.\left({\mathcal{F}}_i(q)\wedge {\delta }_{(q,p)}⟹{\left({\mathcal{F}}_{i+1}(q)\right)}^{\prime }\right).$$

$$\text{Diag}(\sigma ,v,\mathcal{V})=\exists x_1,\dots ,x_m.{\psi }_{\text{distinct}}\wedge {\psi }_{\text{identity}}\wedge {\psi }_{\text{rels}}$$

Full text

This paper proposes user-guided invariant inference based on phase invariants, which capture the different logical phases of the protocol. Users conveys their intuition by specifying a phase structure, an automaton with edges labeled by program transitions; the tool automatically infers assertions that hold in the automaton’s states, resulting in a full safety proof. The additional structure from phases guides the inference procedure towards finding an invariant.

Our results show that user guidance by phase structures facilitates successful inference beyond the state of the art. We find that phase structures are pleasantly well matched to the intuitive reasoning routinely used by domain experts to understand why distributed protocols are correct, so that providing a phase structure reuses this existing intuition.

1 Introduction

Infinite-state systems such as distributed protocols remain challenging to verify despite decades of work developing interactive and automated proof techniques. Such proofs rely on the fundamental notion of an inductive invariant. Unfortunately, specifying inductive invariants is difficult for users, who must often repeatedly iterate through candidate invariants before achieving an inductive invariant. For example, the Verdi project’s proof of the Raft consensus protocol used an inductive invariant with 90 conjuncts and relied on significant manual proof effort [60, 61].

The dream of invariant inference is that users would instead be assisted by automatic procedures that could infer the required invariants. While other domains have seen successful applications of invariant inference, using techniques such as abstract interpretation [18] and property-directed reachability [10, 21], existing inference techniques fall short for interesting distributed protocols, and often diverge while searching for an invariant. These limitations have hindered adoption of invariant inference.

Our Approach. The idea of this paper is that invariant inference can be made drastically more effective by utilizing user-guidance in the form of phase structures. We propose user-guided invariant inference, in which the user provides some additional information to guide the tool towards an invariant. An effective guidance method must (1) match users’ high-level intuition of the proof, and (2) convey information in a way that an automatic inference tool can readily utilize to direct the search. In this setting invariant inference turns a partial, high-level argument accessible to the user into a full, formal correctness proof, overcoming scenarios where procuring the proof completely automatically is unsuccessful.

Our approach places phase invariants at the heart of both user interaction and algorithmic inference. Phase invariants have an automaton-based form that is well-suited to the domain of distributed protocols. They allow the user to convey a high-level temporal intuition of why the protocol is correct in the form of a phase structure. The phase structure provides hints that direct the search and allow a more targeted generalization of states to invariants, which can facilitate inference where it is otherwise impossible.

This paper makes the following contributions:

(1) We present phase invariants, an automaton-based form of safety proofs, based on the distinct logical phases of a certain view of the system. Phase invariants closely match the way domain experts already think about the correctness of distributed protocols by state-machine refinement à la Lamport [e.g. 42].

(2) We describe an algorithm for inferring inductive phase invariants from phase structures. The decomposition to phases through the phase structure guides inference towards finding an invariant. The algorithm finds a proof over the phase structure or explains why no such proof exists. In this way, phase invariants facilitate user interaction with the algorithm.

(3) Our algorithm reduces the problem of inferring inductive phase invariants from phase structures to the problem of solving a linear system of Constrained Horn Clauses (CHC), irrespective of the inference technique and the logic used. In the case of universally quantified phase inductive invariants for protocols modeled in EPR (motivated by previous deductive approaches [50, 49, 59]), we show how to solve the resulting CHC using a variant of $\text{PDR}^{\forall}$ [39].

(4) We apply this approach to the inference of invariants for several interesting distributed protocols. (This is the first time invariant inference is applied to distributed protocols modeled in EPR.) In the examples considered by our evaluation, transforming our high-level intuition about the protocol into a phase structure was relatively straightforward. The phase structures allowed our algorithm to outperform in most cases an implementation of $\text{PDR}^{\forall}$ that does not exploit such structure, facilitating invariant inference on examples beyond the state of the art and attaining faster convergence.

It is surprising that invariant inference—operating in the realm of logical clauses and implications—can so effectively benefit from guidance by phase structures, which exhibit a much higher level of abstraction. While there remain significant challenges to applying invariant inference on complex distributed protocols—notably, inference of invariants with quantifier alternations, necessary, e.g. for Paxos [49]—our approach demonstrates that the seemingly inherent intractability of sifting through a vast space of candidate invariants can be mitigated by leveraging users’ high-level intuition.

2 Preliminaries

In this section we provide background on modeling and verifying systems using first-order logic. We assume familiarity with first-order logic. We use many-sorted first order logic, but omit sorts here to simplify the presentation. Although in this paper we will mostly deal with uninterpreted first-order logic, our definitions and results extend to logics with a background theory.

Notation. $\textit{FV}({\varphi})$ denotes the set of free variables of $\varphi$. $\mathcal{F}_{\Sigma}(V)$ denotes the set of first-order well-formed formulas $\varphi$over vocabulary $\Sigma$ with $\textit{FV}({\varphi})\subseteq V$. We extend the notation $\Longrightarrow$ to quantified formulas and write $\forall\mathcal{V}.\ \varphi\Longrightarrow\psi$ to denote that the formula $\forall\mathcal{V}.\ \varphi\to\psi$ is valid. We sometimes use $f_{a}$ as a shorthand for $f(a)$.

Transition systems. We represent transition systems symbolically, via formulas in first-order logic. The definitions are standard. A vocabulary $\Sigma$ consisting of constant, function, and relation symbols is used to represent states(each function and relation symbol is associated with its arity). Post-states of transitions are represented by a copy of $\Sigma$ denoted $\Sigma^{\prime}=\{a^{\prime}\mid a\in\Sigma\}$(where the arity of each function and relation symbol is inherited from $\Sigma$). A first-order transition system over vocabulary$\Sigma$ is a tuple ${\textit{TS}}=(\textit{Init},{\textit{TR}})$, where $\textit{Init}\in\mathcal{F}_{\Sigma}(\emptyset)$ describes the initial states, and ${\textit{TR}}\in\mathcal{F}_{\hat{\Sigma}}(\emptyset)$ with $\hat{\Sigma}=\Sigma\uplus\Sigma^{\prime}$ describes the transition relation.The states of TS are first-order structures over $\Sigma$, denoted ${{\mbox{STRUCT}}[\Sigma]}$. Each state ${s}\in{{\mbox{STRUCT}}[\Sigma]}$ is a pair ${s}=({D},{\mathcal{I}})$ where ${D}$ is the domain and ${\mathcal{I}}$ is the interpretation function mapping each symbol in $\Sigma$ to its interpretation over ${D}$. We denote by ${{\mbox{STRUCT}}[\Sigma]}|_{{D}}$ the set of structures with domain ${D}$. In this way, every closed formula over $\Sigma$ represents the set of states (first-order structures) that satisfy it. In particular, a state ${s}$ is initial if ${s}\models\textit{Init}$. A transition of TS is a pair of states ${s}_{1}=({D},{\mathcal{I}}_{1}),{s}_{2}=({D},{\mathcal{I}}_{2})$ with a shared domain such that $({s}_{1},{s}_{2})\models{\textit{TR}}$, where $({s}_{1},{s}_{2})$ is a shorthand for the structure ${s}=({D},{\mathcal{I}})$ obtained by defining ${\mathcal{I}}(a)={\mathcal{I}}_{1}(a)$ if $a\in\Sigma$, and ${\mathcal{I}}(a)={\mathcal{I}}_{2}(a)$ if $a\in\Sigma^{\prime}$. ${s}_{1}$ is also called the pre-state and ${s}_{2}$ the post-state. Traces are finite sequences of states $\sigma_{1},\sigma_{2},\ldots$ starting from an initial state such that there is a transition between each pair of consecutive states. The reachable states of TSare those that reside on traces starting from an initial state.

Safety. A safety property $P$ is a formula in $\mathcal{F}_{\Sigma}(\emptyset)$. We say that TS is safe if all the reachable states satisfy $P$, in which case we also say that $P$ is an invariant of TS. A prominent way to prove safety is via inductive invariants. An inductive invariant Inv is a closed first-order formula over $\Sigma$ such that the following requirements hold:

(i) $\textit{Init}\Longrightarrow\textit{Inv}$(initiation), and

(ii) $\textit{Init}\wedge{\textit{TR}}\Longrightarrow\textit{Inv}^{\prime}$(consecution),

where $\textit{Inv}^{\prime}$ is obtained from Inv by replacing each symbol from $\Sigma$ with its primed counterpart.Initiation and consecution ensure that all the reachable states satisfy Inv. If, in addition, Inv satisfies:

(iii) $\textit{Inv}\Longrightarrow P$(safety),

it follows that all the reachable states satisfy $P$, and TS is safe.

3 Running Example: Distributed Key-Value Store

We begin with a description of the running example we refer to throughout the paper.

The sharded key-value store with retransmissions (KV-R), adapted from IronFleet [32, §5.2.1], is a distributed hash table where each node owns a subset of the keys, and keys can be dynamically transferred among nodes to balance load. The safety property ensures that each key is globally associated with one value, even in the presence of key transfers. Messages might be dropped by the network, and the protocol uses retransmissions and sequence numbers to maintain availability and safety.

Fig. 1 shows code modeling the protocol in a relational first-order language akin to Ivy [44], which compiles to EPR transition systems. The state of nodes and the network is modeled by global relations. Lines 1 to 4 declare uninterpreted sorts for keys, values, clients, and sequence numbers. Lines 6 to 14 describe the state, consisting of:

(i) local state of clients pertaining to the table (which nodes are $\mathtt{owner}$s of which keys, and the local shard of the $\mathtt{table}$ mapping keys to values);

(ii) local state of clients pertaining to sent and received messages ($\mathtt{seqnum\_sent}$, $\mathtt{unacked}$, $\mathtt{seqnum\_recvd}$); and

(iii) the state of the network, comprised of two kinds of messages ($\mathtt{transfer\_msg}$, $\mathtt{ack\_msg}$). Each message kind is modeled as a relation whose first two arguments indicate the source and destination of the message, and the rest carry the message’s payload. For example, $\mathtt{ack\_msg}$ is a relation over two nodes and a sequence number, with the intended meaning that a tuple $(c_{1},c_{2},s)$ is in $\mathtt{ack\_msg}$ exactly when there is a message in the network from $c_{1}$ to $c_{2}$ acknowledging a message with sequence number $s$.

The initial states are specified in lines 17 to 18. Transitions are specified by the actions declared in lines 20 to 28. Actions can fire nondeterministically at any time when their precondition ($\mathtt{require}$ statements) holds. Hence, the transition relation comprises of the disjunction of the transition relations induced by the actions. The state is mutated by modifying the relations. For example, message sends are modeled by inserting a tuple into the corresponding relation (e.g. line 27), while message receives are modeled by requiring a tuple to be in the relation (e.g. line 32), and then removing it (e.g. line 33). The updates in lines 23 and 27 remove a set of tuples matching the pattern.

KV-R protocol. Transferring keys between nodes begins by sending a $\mathtt{transfer\_msg}$ from the owner to a new node (line 20), which stores the key-value pair when it receives the message (line 1). Upon sending a transfer message the original node cedes ownership (line 26) and does not send new transfer messages. Transfer messages may be dropped (line 30). To ensure that the key-value pair is not lost, retransmissions are performed (line 35) with the same sequence number until the target node acknowledges (which occurs in line 9). Acknowledge messages themselves may be dropped (line 15). Sequence numbers protect from delayed transfer messages, which might contain old values (line 4).

KV-R safety property. Lines 30 to 33 specify the key safety property: at most one value is associated with any key, anywhere in the network. Intuitively, the protocol satisfies this because each key $k$ is either currently

(1) ownedby a node, in which case this node is unique, or

(2) it is in the process of transferring between nodes, in which case the careful use of sequence numbers ensures that the destination of the key is unique.

As is typical, it is not straightforward to translate this intuition into a full correctness proof. In particular, it is necessary to relate all the different components of the state, including clients’ local state and pending messages.

Invariant inference strives to automatically find an inductive invariant establishing safety. This example is challenging for existing inference techniques (Section 6). This paper proposes user-guided invariant inference based on phase-invariants to overcome this challenge. The rest of the paper describes our approach, in which inference is provided with the phase structure in Fig. 2, matching the high level intuitive explanation above. The algorithm then automatically infers facts about each phase to obtain an inductive invariant. Section 4 describes phase structures and inductive phase invariants, and Section 5 explains how these are used in user-guided invariant inference.

4 Phase Structures and Invariants

Phase invariants describe the protocol as transitioning between different logical stages. In this section we introduce phase structures and inductive phase invariantsand explain their role in verifying safety properties. In Section 5 we explain how we use these in guiding automatic invariant inference. For brevity, proofs are deferred to Appendix 0.E.

4.1 Phase Invariants

Definition 1 (Quantified Phase Automaton)

A quantified phase automaton (phase automaton for short) over $\Sigma$ is a tuple $\mathcal{A}=(\mathcal{Q},\iota,\mathcal{V},\delta,\varphi)$ where:

• •

$\mathcal{Q}$ is a finite set of phases.

• •

$\iota\in\mathcal{Q}$ is the initial phase.

• •

$\mathcal{V}$ is a set of variables, called the automaton’s quantifiers .

• •

$\delta:\mathcal{Q}\times\mathcal{Q}\to\mathcal{F}_{\hat{\Sigma}}(\mathcal{V})$ is a function labeling every pair of phases by a transition relation formula, such that $\textit{FV}({\delta_{(q,p)}})\subseteq\mathcal{V}$ for every $(q,p)\in\mathcal{Q}\times\mathcal{Q}$.

• •

$\varphi:\mathcal{Q}\to\mathcal{F}_{\Sigma}(\mathcal{V})$ is a function labeling every phase by a phase characterization formula, such that $\textit{FV}({\varphi_{q}})\subseteq\mathcal{V}$ for every phase $q\in\mathcal{Q}$.

Intuitively, $\mathcal{V}$ should be understood as free variables that are implicitly universally quantified outside of the automaton’s scope. For each assignment to these variables, the automaton represents the progress along the phases from the point of view of this assignment, and thus $\mathcal{V}$ is also called the view (or view quantifiers).

We refer to $(\mathcal{Q},\iota,\mathcal{V},\delta)$, where $\varphi$ is omitted, as the phase structure (or the automaton structure) of $\mathcal{A}$.

We refer by the edges of $\mathcal{A}$ to $\mathcal{R}=\{(q,p)\in\mathcal{Q}\times\mathcal{Q}\mid\delta_{(q,p)}\not\equiv{\textit{false}}\}.$

A trace of $\mathcal{A}$ is a sequence of phases $q_{0},\ldots,q_{n}$ such that $q_{0}=\iota$ and $(q_{i},q_{i+1})\in\mathcal{R}$ for every $0\leq i<n$.

We say that $\mathcal{A}$ is deterministic if for every $(q,p_{1}),(q,p_{2})\in\mathcal{R}$ s.t. $p_{1}\neq p_{2}$, the formula $\delta_{(q,p_{1})}\wedge\delta_{(q,p_{2})}$ is unsatisfiable.

Example 1 (Quantified Phase Automaton and Structure)

Fig. 2 shows a phase automaton for the running example, with the view of a single key $k$. It describes the protocol as transitioning between two distinct (logical) phases of $k$: owned ($\texttt{O}[k]$) and transferring ($\texttt{T}[k]$). The edges are labeled by actions of the system. A wildcard * means that the action is executed with an arbitrary argument. The two central actions are (i) reshard, which transitions from $\texttt{O}[k]$ to $\texttt{T}[k]$, but cannot execute in $\texttt{T}[k]$, and (ii) recv_transfer_message, which does the opposite. The rest of the actions do not cause a phase change and appear on a self loop in each phase. Actions related to keys other than $k$ are considered as self-loops, and omitted here for brevity. Intuitively, the automaton transitions between phases when the protocol executes an action that matches the automaton’s edge between the phases. Some actions are disallowed in certain phases, namely, do not label any outgoing edge from a phase, such as recv_transfer_msg($k$) in $\texttt{O}[k]$. Characterizations for each phase are depicted in Fig. 2 (bottom). Without them, Fig. 2 represents a phase structure, which serves as the input to our inference algorithm.

Remark 1

We remark that the choice of automaton aims to reflect the safety property of interest. In our example, one might instead imagine taking the view of a single node as it interacts with multiple keys, which might seem intuitive from the standpoint of implementing the system. However, it is not appropriate for the proof of value uniqueness, since keys pass in and out of the view of a single clientover their lifetime. The phase automaton should not aim to capture the phase structure of the implementation but that arising from the correctness intuition.

We now formally define phase invariants as phase automata that overapproximate the behaviors of the original system.

Definition 2 (Language of Phase Automaton)

Let $\mathcal{A}$ be a quantified phase automaton over $\Sigma$, and $\overline{\sigma}=\sigma_{0},\ldots,\sigma_{n}$ a finite sequence of states (first-order structures)in ${{\mbox{STRUCT}}[\Sigma]}$, all with domain ${D}$. Let $v:\mathcal{V}\to{D}$ be a valuation of the automaton quantifiers. We say that:

• •

$\overline{\sigma},v\models\mathcal{A}$ if there exists a trace of phases $q_{0},\ldots,q_{n}$ such that $(\sigma_{i},\sigma_{i+1}),v\models\delta_{(q_{i},q_{i+1})}$ for every $0\leq i<n$ (in particular, $q_{0},\ldots,q_{n}$ is a trace of $\mathcal{A}$)and $\sigma_{i},v\models\varphi_{q_{i}}$ for every $0\leq i\leq n$.

• •

$\overline{\sigma}\models\mathcal{A}$ if $\overline{\sigma},v\models\mathcal{A}$ for every valuation $v$.

The language of $\mathcal{A}$ is $\mathcal{L}(\mathcal{A})=\{\overline{\sigma}\mid\overline{\sigma}\models\mathcal{A}\}$.

4.2 Phase Invariants

Definition 3 (Phase Invariant)

A phase automaton $\mathcal{A}$ is a phase invariant for a transition system TS (both over $\Sigma$)if $\mathcal{L}({\textit{TS}})\subseteq\mathcal{L}(\mathcal{A})$, where $\mathcal{L}({\textit{TS}})$ denotes the set of allfinite traces of TS.

Trace inclusion ensures that a phase invariant $\mathcal{A}$ can be soundly used to verify safety properties of TS.

Example 2 (Phase Invariant)

The phase automaton of Fig. 2 is a phase invariant for the protocol: intuitively, whenever an execution of the protocol reaches a phase, its characterizations hold. This fact may not be straightforward to establish. To this end we develop the notion of inductive phase invariants.

4.3 Establishing Phase Invariants with Inductive Phase Invariants

To establish phase invariants, we use inductiveness:

Definition 4 (Inductive Phase Invariant)

$\mathcal{A}$ is inductive w.r.t. ${\textit{TS}}=(\textit{Init},{\textit{TR}})$ ifthe following conditions hold:

Initiation:

$\textit{Init}\Longrightarrow\left(\forall\mathcal{V}.\ \varphi_{\iota}\right)$ .

Inductiveness:

for all $(q,p)\in\mathcal{R}$,  $\forall\mathcal{V}.\ \left(\varphi_{q}\land\delta_{(q,p)}\Longrightarrow\varphi_{p}^{\prime}\right)$.

Edge Covering:

for every $q\in\mathcal{Q}$,  $\forall\mathcal{V}.\ \left(\varphi_{q}\land{\textit{TR}}\Longrightarrow\bigvee_{(q,p)\in\mathcal{R}}{\delta_{(q,p)}}\right)$ .

Example 3 (Inductive Phase Invariant)

The phase automaton in Fig. 2 is an inductive phase invariant: the characterizations are such that in every possible phase, when the protocol executes a valid action starting from a state satisfying the current phase characterizations, there is an outgoing edge that matches this action (covering), and the resulting program state satisfies the characterization of the target phase (inductiveness). For example, the only disallowed transition in O[$k$] is recv_transfer_message, which indeed cannot execute in O[$k$] according to the characterization in line 41. Further, if, for example, a protocol’s transition from O[$k$] matches the labeling of the edge to T[$k$] (i.e. a reshard action on $k$), the post-state necessarily satisfies the characterizations of T[$k$]: for instance, the post-state satisfies the uniqueness of unreceived transfer messages (line 48) because in the pre-state there are none (line 41).

Lemma 1

If $\mathcal{A}$ is inductive w.r.t. TS then it is a phase invariant for TS.

Remark 2

The careful reader may notice that the inductiveness requirement is stronger than needed to ensure that the characterizations form a phase invariant. It could be weakened to require for every $q\in\mathcal{Q}$: $\forall\mathcal{V}.\ \varphi_{q}\wedge{\textit{TR}}\Longrightarrow\bigvee_{(q,p)\in\mathcal{R}}{\delta_{(q,p)}\wedge\varphi_{p}^{\prime}}.$ However, as we explain in Section 5, our notion of inductiveness is crucial for inferring inductive phase automata, which is the goal of this paper. Furthermore, for deterministic phase automata, the two requirements coincide.

Inductive invariants vs. inductive phase invariants. Inductive invariants and inductive phase invariants are closely related: an inductive phase invariant induces a “standard” inductive invariant, and vice versa:

Lemma 2

If $\mathcal{A}$ is inductive w.r.t. TS then $\forall\mathcal{V}.\ \bigvee_{q\in\mathcal{Q}}{\varphi_{q}}$ is an inductive invariant for TS. Conversely, if Inv is an inductive invariant for TS, then the phase automaton $\mathcal{A}_{\textit{Inv}}=(\{q\},\{q\},\emptyset,\delta,\varphi)$, where $\delta_{(q,q)}={\textit{TR}}$ and $\varphi_{q}=\textit{Inv}$ is an inductive phase automaton w.r.t. TS.

In this sense, phase inductive invariants are as expressive as inductive invariants. However, as we show in this paper, their structure can be used by a user as an intuitive way to guide an automatic invariant inference algorithm.

Remark 3

It is straightforward to add more flexibility to a phase automaton by allowing a set of initial states, $\mathcal{Q}_{0}$. In this case, for the automaton to over-approximate all the reachable states of TS, it suffices that every initial state corresponds to some initial phase of TS, possibly depending on the valuation of $\mathcal{V}$. Therefore, the initiation constraint in the definition of an inductive phase invariant for TS may be relaxed into:

[TABLE]

4.4 Safe Inductive Phase Invariants

Next we show that an inductive phase invariant can be used to establish safety.

Definition 5 (Safe Phase Automaton)

Let $\mathcal{A}$ be a phase automaton over $\Sigma$ with quantifiers $\mathcal{V}$ , and let $\forall\mathcal{V}.\ \mathcal{P}$ be a safety property. Then $\mathcal{A}$ is safe w.r.t. $\forall\mathcal{V}.\ \mathcal{P}$ if

[TABLE]

holds for every $q\in\mathcal{Q}$.

Lemma 3

If $\mathcal{A}$ is inductive w.r.t. TS and safe w.r.t. $\forall\mathcal{V}.\ \mathcal{P}$ then $\forall\mathcal{V}.\,\mathcal{P}$ is an invariant of TS.

5 Inference of Inductive Phase Invariants

In this section we turn to the inference of safe inductive phase invariants over a given phase structure, which guides the searchfor invariant.

This section defines the problem, shows that it can be reduced to a set of Constrained Horn Clauses, discusses the aspects by which a phase structure guides inference, and considers witnesses for the case that no solution exists. Formally, the problem we target is:

Definition 6 (Inductive Phase Invariant Inference)

Given a transition system ${\textit{TS}}=(\textit{Init},{\textit{TR}})$, a phase structure $\mathcal{S}=(\mathcal{Q},\iota,\mathcal{V},\delta)$ and a safety property $\forall\mathcal{V}.\ \mathcal{P}$, all over $\Sigma$, find a safe inductive phase invariant $\mathcal{A}$ for TS over the phase structure $S$, if one exists.

Example 4

Inference of an inductive phase invariant is provided with the phase structure in Fig. 2, which embodies an intuitive understanding of the different phases the protocol undergoes (see Example 1). The algorithm automatically finds phase characterizations forming a safe inductive phase invariant over the user-provided structure. We note that inference is valuable even after a phase structure is provided: in the running example, finding an inductive phase invariant is not easy; in particular, the characterizations in Fig. 2 relate different parts of the state and involve multiple quantifiers.

5.1 Reduction to Constrained Horn Clauses

We view each unknown phase characterization, $\varphi_{q}$, which we aim to infer for every $q\in\mathcal{Q}$, as a predicate $I_{q}$. The definition of a safe inductive phase invariant induces a set of second-order Constrained Horn Clauses (CHC) over $I_{q}$:

[TABLE]

where $\mathcal{V}$ denotes the quantifiers of $\mathcal{A}$. The number of constraints is $1+|\mathcal{R}|+2|\mathcal{Q}|$.

All the constraints are linear, namely at most one unknown predicate appears at the lefthand side of each implication.

Constraint (4) captures the original safety requirement, whereas (3) can be understood as additional safety properties that are specified by the phase automaton (since no unknown predicates appear in the righthand side of the implications).

A solution $\mathbf{I}$ to the CHC system associates each predicate $I_{q}$ with a formula $\psi_{q}$ over $\Sigma$ (with $\textit{FV}({\psi_{q}})\subseteq\mathcal{V}$) such that when $\psi_{q}$ is substituted for $I_{q}$, all the constraints are satisfied (i.e., the corresponding first-order formulas are valid). A solution to the system induces a safe inductive phase automaton through characterizing each phase $q$ by the interpretation of $I_{q}$, and vice versa. Formally:

Lemma 4

Let $\mathcal{A}=(\mathcal{Q},\mathcal{R},\iota,\mathcal{V},\delta,\varphi)$ with $\varphi_{q}={\mathbf{I}}_{q}$. Then $\mathcal{A}$ is a safe inductive phase invariant wrt. TS and $\forall\mathcal{V}.\ \mathcal{P}$ if and only if $\mathbf{I}$ is a solution to the CHC system.

Therefore, to infer a safe inductive phase invariant over a given phase structure, we need to solve the corresponding CHC system. In Section 6.1 we explain our approach for doing so for the class of universally quantified phase characterizations. Note that the weaker definition of inductiveness discussed in Remark 2 would prevent the reduction to CHC as it would result in clauses that are not Horn clauses.

Completeness of inductive phase invariants. There are cases where a given phase structure induces a safe phase invariant ${\cal A}$, but not an inductive one, making the CHC system unsatisfiable. However, a strengthening into an inductive phase invariant can always be used to prove that $\mathcal{A}$ is an invariant if

(i) the language of invariants is unrestricted, and

(ii) the phase structure is deterministic, namely, does not cover the same transition in two outgoing edges. Determinism of the automaton does not lose generality in the context of safety verification since every inductive phase automaton can be converted to a deterministic one; non-determinism is in fact unbeneficial as it mandates the same state to be characterized by multiple phases (see also Remark 2).

These topics are discussed in detail in Appendix 0.A.

Remark 4

Each phase is associated with a set of states that can reach it, where a state $\sigma$ can reach phase $q$ if there is a sequence of program transitions that results in $\sigma$ and can lead to $q$ according to the automaton’s transitions. This makes a phase structure different from a simple syntactical disjunctive template for inference, in which such semantic meaning is unavailable.

Remark 5

When the safety property is of the form $\forall\mathcal{V}.\ \textit{Grd}\to\psi$ where $\textit{Grd},\psi\in\mathcal{F}_{\Sigma}(\mathcal{V})$, we sometime seek an inductive phase invariant where Grd guards the entire phase structure of the automaton. This may be represented by splitting the initial phase into two: one whose characterization includes Grd, and another “dummy” initial phase whose characterization is $\neg\textit{Grd}$. The dummy initial phase has a single self loop labeled TR, whereas the other maintains the actual phase structure. Moreover, Grd is added to the characterization of all other phases.

5.2 Phase Structures as a Means to Guide Inference

The search space of invariants over a phase structure is in fact larger than that of standard inductive invariants, because each phase can be associated with different characterizations. Sometimes the disjunctive structure of the phases (Lemma 2) uncovers a significantly simpler invariant than exists in the syntactical class of standard inductive invariants explored by the algorithm, but this is not always the case.111 As an illustration, Appendix 0.C includes an inductive invariant for the running example which is comparable in complexity to the inductive phase invariant in Fig. 2.

Nonetheless, the search for an invariant over the structure is guided, through the following aspects:

(1) Phase decomposition. Inference of an inductive phase invariant aims to find characterizations that overapproximate the set of states reachable in each phase (Remark 4). The distinction between phases is most beneficial when there is a considerable difference between the sets associated with different phases and their characterizations. For instance, in the running example, all states without unreceived transfer messages are associated with O[$k$], whereas all states in which such messages exist are associated with T[$k$]—a distinction captured by the characterizations in lines 41 and 48 in Fig. 2.

Differences between phases would have two consequences. First, since each phase corresponds to fewer states than all reachable states, generalization—the key ingredient in inference procedures—is more focused. The second consequence stems from the fact that inductive characterizations of different phases are correlated. It is expected that a certain property is more readily learnable in one phase, while related facts in other phases are more complex. For instance, the characterization in line 41 in Fig. 2 is more straightforward than the one in line 48. Simpler facts in one phase can help characterize an adjacent phase when the algorithm analyzes how that property evolves along the edge. Thus utilizing the phase structure can improve the gradual construction of overapproximations of the sets of states reachable in each phase.

(2) Disabled transitions. A phase automaton explicitly states which transitions of the system are enabled in each phase, while the rest are disabled. Such impossible transitions induce additional safety properties to be established by the inferred phase characterizations. For example, the phase invariant in Fig. 2 forbids a recv_transfer_message($k$) in O[$k$], a fact that can trigger the inference of the characterization in line 41. These additional safety properties direct the search for characterizations that are likely to be important for the proof.

(3) Phase-awareness. Finally, while a phase structure can be encoded in several ways (such as ghost code), a key aspect of our approach is that the phase decomposition and disabled transitions are explicitly encoded in the CHC system in Section 5.1, ensuring that they guide the otherwise heuristic search.

In Section 6.2.3 we demonstrate the effects of aspects (1)–(3) on guidance.

6 Implementation and Evaluation

In this section we apply invariant inference guided by phase structures to distributed protocols modeled in EPR, motivated by previous deductive approachesto safety of distributed protocols [50, 49, 59].

The work-flow for our approach is illustrated in Fig. 3.

6.1 Phase-$\text{PDR}^{\forall}$ for Inferring Universally Quantified Characterizations

We now describe our procedure for solving the CHCs system of Section 5.1. It either (i) returns universally quantified phase characterizations that induce a safe inductive phase invariant, (ii) returns an abstract counterexample trace demonstrating that this is not possible, or (iii) diverges.

EPR. Our procedure handles transition systems expressed using the extended Effectively PRopositional fragment (EPR) of first order logic [51, 50], and infers universally quantified phase characterizations. Satisfiability of (extended) EPR formulas is decidable, enjoys the finite-model property, and supported by existing SMT solvers such as Z3 [45] and first order logic provers such as iProver [40].

Phase-$\text{PDR}^{\forall}$. Our procedure is based on $\text{PDR}^{\forall}$ [39], a variant of PDR [10, 21] that infers universally quantified inductive invariants. PDR computes a sequence of frames $\mathcal{F}_{0},\ldots,\mathcal{F}_{n}$ such that $\mathcal{F}_{i}$ overapproximates the set of states reachable in $i$ steps. In our case, each frame $\mathcal{F}_{i}$ is a mapping from a phase $q$ to characterizations. The details of the algorithm are standard for PDR; we describe the gist of the procedure in Appendix 0.D. We only stress the following: Counterexamples to safety take into account the safety property as well as disabled transitions. Search for predecessors is performed by going backwards on automaton edges, blocking counterexamples from preceding phases to prove an obligation in the current phase. Generalization is performed w.r.t. all incoming edges. As in $\text{PDR}^{\forall}$, proof obligations are constructed via diagrams [12]; in our setting these include the interpretation for the view quantifiers (see Appendix 0.D for details).

Edge covering check in EPR. When the transition relation formula is in EPR and the phase characterizations are universally quantified, the checks induced by Equations 1, 2 and 4 translate to checking (un)satisfiability of EPR formulas, potentially causing divergence of the solver. Equation 3 is trickier as checking implication between two EPR transition relations falls outside of EPR. To use a decidable edge covering check, we exploit the typical structure of transition relations in our setting, which is a disjunction between the transition relation of exported actions (the different actions in Fig. 1). In the phase automaton we label an edge $(q,p)$ by a set of exported actions, each action $a$ with a guard $g^{(q,p)}_{a}$ which is an alternation-free formula (a Boolean combination of universal and existential closed formulas). The edge covering check (Equation 3) can now be written

[TABLE]

The righthand side of the implication is alternation-free and thus the check falls into the decidable EPR class. Such edge labeling is sufficiently expressive for the phase structures ofall our examples. Alternatively, sound but incomplete bounded quantifier instantiation [23] could be used, potentially allowing more complex decompositions of TR.

Absence of Inductive Phase Characterizations.

What happens when the user gets the automaton wrong? One case is when there does not exist an inductive phase invariant with universal phase characterizations over the given structure. When this occurs, our tool can return an abstract counterexample trace—a sequence of program transitions and transitions of the automaton (inspired by [39, 48])—which constitutes a proof of that fact (see Appendix 0.B). The counterexample trace can assist the user in debugging the automaton or the program and modifying them. For instance, missing edges occurred frequently when we wrote the automata of Section 6, and we used the generated counterexample traces to correct them.

Another type of failure is when an inductive phase invariant exists but the automaton does not direct the search well towards it. In this case the user may decide to terminate the analysis and articulate a different intuition via a different phase structure. In standard inference procedures, the only way to affect the search is by modifying the transition system; instead, phase structures equip the user with an ability to guide the search.

6.2 Evaluation

We evaluate our approach for user-guided invariant inference based on phase structures by comparing Phase-$\text{PDR}^{\forall}$ to standard $\text{PDR}^{\forall}$, its inductive invariant inference counterpart. We implemented $\text{PDR}^{\forall}$ and Phase-$\text{PDR}^{\forall}$ in mypyvy [2], a new system for invariant inference inspired by Ivy [44], over Z3 [45]. We studythe following effects of guidance by phase structures:

Can Phase-$\text{PDR}^{\forall}$ converge to a proof when $\text{PDR}^{\forall}$ does not (in reasonable time)? 2. 2.

Is Phase-$\text{PDR}^{\forall}$ faster than $\text{PDR}^{\forall}$? 3. 3.

Which aspects of Phase-$\text{PDR}^{\forall}$ contribute to its performance benefits?

Protocols. We applied $\text{PDR}^{\forall}$ and Phase-$\text{PDR}^{\forall}$ to the most challenging examples admitting universally-quantified invariants, which previous works verified using deductive techniques. The protocols we analyzed are listed below and in Table 1. The full models appear in [1]. The KV-R protocol analyzed is taken from one of the two realistic systems studied by the IronFleet paper [32] using deductive verification.

Phase structures. The phase structures we used appear in [1]. In all our examples, it was straightforward to translate the existing high-level intuition of important and relevant distinctions between phases in the protocol into the phase structures we report. For example, it took us less than an hour to finalize an automaton for KV-R. We emphasize that phase structures do not include phase characterizations; the user need not supply them, nor has to understand the inference procedure. Our exposition of the phase structures below refers to an intuitive meaning of each phase, but this is not part of the phase structure provided to the tool.

6.2.1 (1) Achieving Convergence Through Phases

In this section we consider the effect of phases on inference for examples on which standard $\text{PDR}^{\forall}$ does not converge in 1 hour.

Examples. Sharded key-value store with retransmissions (KV-R): see Section 3 and Example 1. This protocol has not been modeled in decidable logic before.

Cache coherence. This example implements the classic MESI protocol for maintaining cache coherence in a shared-memory multiprocessor [35], modeled in decidable logic for the first time. Cores perform reads and writes to memory, and caches snoop on each other’s requests using a shared bus and maintain the invariant that there is at most one writer of a particular cache line. For simplicity, we consider only a single cache line, and yet the example is still challenging for $\text{PDR}^{\forall}$. Standard explanations of this protocol in the literature already use automata to describe this invariant, and we directly exploit this structure in our phase automaton. Phase structure: There are 10 phases in total, grouped into three parts corresponding to the modified, exclusive, and shared states in the classical description. Within each group, there are additional phases for when a request is being processed by the bus. For example, in the shared group, there are phases for handling reads by cores without a copy of the cache line, writes by such cores, and also writes by cores that do have a copy. Overall, the phase structure is directly derived from textbook descriptions, taking into account that use of the shared bus is not atomic.

Results and discussion. Measurements for these examples appear in Table 1. Standard $\text{PDR}^{\forall}$ fails to converge in less than an hour on 13 out of 16 seeds for KV-R and all 16 seeds for the cachecoherence protocol. In contrast, Phase-$\text{PDR}^{\forall}$ converges to a proof in a few minutes in all cases. These results demonstrate that phase structures can effectively guide the search and obtain an invariant quickly where standard inductive invariant inference does not.

6.2.2 (2) Enhancing Performance Through Phases

In this section we consider the use of phase structures to improve the speed of convergence to a proof.

Examples. Distributed lock service, adapted from [60], allows clients to acquire and release locks by sending requests to a central server, which guarantees that only one client holds each lock at a time. Phase structure: for each lock, the phases follow the 4 steps by which a client completes a cycle of acquire and release. We also consider a simpler variant with only a single lock, reducing the arity of all relations and removing the need for an automaton view. Its phase structure is the same, only for a single lock.

Simple quorum-based consensus, based on the example in [59]. In this protocol, nodes propose themselves and then receive votes from other nodes. When a quorum of votes for a node is obtained, it becomes the leader and decides on a value. Safety requires that decided values are unique. The phase structure distinguishes between the phases before any node is elected leader, once a node is elected, and when values are decided. Note that the automaton structure is unquantified.

Leader election in a ring [13, 50], in which nodes are organized in a directional ring topology with unique IDs, and the safety property is that an elected leader is a node with the highest ID. Phase structure: for a view of two nodes $n_{1},n_{2}$, in the first phase, messages with the ID of $n_{1}$ are yet to advance in the ring past $n_{2}$, while in the second phase, a message advertising $n_{1}$ has advanced past $n_{2}$. The inferred characterizations include another quantifier on nodes, constraining interference (see Section 7).

Sharded key-value store (KV) is a simplified version of KV-R above, without message drops and the retransmission mechanism. The phase structure is exactly as in KV-R, omitting transitions related to sequence numbers and acknowledgment. This protocol has not been modeled in decidable logic before.

Results and discussion. We compare the performance of standard $\text{PDR}^{\forall}$ and Phase-$\text{PDR}^{\forall}$ on the above examples, with results shown in Table 1. For each example, we ran the two algorithms on 16 different Z3 random seeds. Measurements were performed on a 3.4GHz AMD Ryzen Threadripper 1950X with 16 physical cores, running Linux 4.15.0, using Z3 version 4.7.1. By disabling hyperthreading and frequency scaling and pinning tasks to dedicated cores, variability across runs of a single seed was negligible.

In all but one example, Phase-$\text{PDR}^{\forall}$ improves performance, sometimes drastically; for example, performance for leader election in a ring is improved by a factor of 60. Phase-$\text{PDR}^{\forall}$ also improves the robustness of inference [26] on this example, as the standard deviation falls from 39 in $\text{PDR}^{\forall}$ to 0.04 in Phase-$\text{PDR}^{\forall}$.

The only example in which a phase structure actually diminishes inference effectiveness is simple consensus. We attribute this to an automaton structure that does not capture the essence of the correctness argument very well, overlooking votes and quorums. This demonstrates that a phase structure might guide the search towards counterproductive directions if the user guidance is “misleading”. This suggests that better resiliency of interactive inference framework could be achieved by combining phase-based inference with standard inductive invariant-based reasoning. We are not aware of a single “good” automaton for this example. The correctness argument of this example is better captured by the conjunction of two automata (one for votes and one for accumulating a quorum) with different views, but the problem of inferring phase invariants for mutually-dependent automata is a subject for future work.

6.2.3 (3) Anatomy of the Benefit of Phases

We now demonstrate that each of the beneficial aspects of phases discussed in Section 5.2 is important for the benefits reported above.

Phase decomposition. Is there a benefit from a phase structure even without disabled transitions? An example to a positive answer to this question is leader election in a ring, which demonstrates a huge performance benefit even without disabled transitions.

Disabled transitions. Is there a substantial gain from exploiting disabled transitions? We compare Phase-$\text{PDR}^{\forall}$ on the structure with disabled transitions and a structure obtained by (artificially) adding self loops labeled with the originally impossible transitions, on the example of lock service with multiple locks (Section 6.2.2), seeing that it demonstrates a performance benefit using Phase-$\text{PDR}^{\forall}$ and showcases several disabled transitions in each phase. The result is that without disabled transitions, the mean running time of Phase-$\text{PDR}^{\forall}$ on this example jumps from 2.73 seconds to 6.24 seconds. This demonstrates the utility of the additional safety properties encompassed in disabled transitions.

Phase-awareness. Is it important to treat phases explicitly in the inference algorithm, as we do in Phase-$\text{PDR}^{\forall}$ (Section 6.1)? We compare our result on convergence of KV-R with an alternative in which standard $\text{PDR}^{\forall}$is applied to an encoding of the phase decomposition and disabled transition by ghost state: each phase is modeled by a relation over possible view assignments, and the model is augmented with update code mimicking phase changes; the additional safety properties derived from disabled transitions are provided; and the view and the appropriate modification of the safety property are introduced. This translation expresses all information present in the phase structure, but does not explicitly guide the inference algorithm to use this information. The result is that with this ghost-based modeling the phase-oblivious $\text{PDR}^{\forall}$ does not converge in 1 hour on KV-R in any of the 16 runs, whereas it converges when Phase-$\text{PDR}^{\forall}$ explicitly directs the search using the phase structure.

7 Related Work

Phases in distributed protocols. Distributed protocols are frequently described in informal descriptions as transitioning between different phases. Recently, PSync [19] used the Heard-Of model [14], which describes protocols as operating in rounds, as a basis for the implementation and verification of fault-tolerant distributed protocols. Typestates [e.g. 58, 24] also bear some similarity to the temporal aspect of phases. State machine refinement [3, 27] is used extensively in the design and verification of distributed systems (see e.g. [46, 32]). The automaton structure of a phase invariant is also a form of state machine; our focus is on inference of characterizations establishing this.

Interaction in verification. Interactive proof assistants such as Coq [8] and Isabelle/HOL [47] interact with users to aid them as they attempt to prove candidate inductive invariants. This differs from interaction through phase structures and counterexample traces. Ivy uses interaction for invariant inference by interactive generalization from counterexamples [50]. This approach is less automatic as it requires interaction for every clause of the inductive invariant. In terminology from synthesis [29], the use of counterexamples is synthesizer-driven interaction with the tool, while interaction via phase structures is mainly user-driven. Abstract counterexample traces returned by the tool augment this kind of interaction. As [37] has shown, interactive invariant inference, when considered as a synthesis problem (see also [26, 54]) is related to inductive learning.

Template-based invariant inference. Many works employ syntactical templates for invariants, used to constrain the search [e.g. 16, 53, 56, 57, 7]. The different phases in a phase structure induce a disjunctive form, but crucially each disjunct also has a distinct semantic meaning, which inference overapproximates, as explained in Section 5.2.

Automata in safety verification. Safety verification through an automaton-like refinement of the program’s control has been studied in a number of works. We focus on related techniques for proof automation. The Automizer approach to the verification of sequential programs [33, 34] is founded on the notion of a Floyd-Hoare automaton, which is an unquantified inductive phase automaton; an extension to parallel programs [22] uses thread identifiers closed under the symmetry rule, which are related to view quantifiers. Their focus is on the automatic, incremental construction of such automata as a union of simpler automata, where each automaton is obtained from generalizing the proof/infeasibility of a single trace. In our approach the structure of the automaton is provided by the user as a means of conveying their intuition of the proof, while the annotations are computed automatically. A notable difference is that in Automizer, the generation of characterizations in an automaton constructed from a single trace does not utilize the phase structure (beyond that of the trace), whereas in our approach the phase structure is central in generalization from states to characterizations.

In trace partitioning [52, 43], abstract domains based on transition systems partitioning the program’s control are introduced. The observation is that recording historical information forms a basis for case-splitting, as an alternative to fully-disjunctive abstractions. This differs from our motivation of distinguishing between different protocol phases. The phase structure of the domain is determined by the analyser, and can also be dynamic. In our work the phase structure is provided by the user as guidance. We use a variant of $\text{PDR}^{\forall}$, rather than abstract interpretation [17], to compute universally quantified phase characterizations.

Techniques such as predicate abstraction [28, 25] and existential abstraction [15], as well as the safety part of predicate diagrams [11], use finite languages for the set of possible characterizations and lack the notion of views, both essential for handling unbounded numbers of processes and resources.

Finally, phase splitter predicates [55] share our motivation of simplifying invariant inference by exposing the different phases the loop undergoes. Splitter predicates correspond to inductive phase characterizations [55, Theorem 1], and are automatically constructed according to program conditionals. In our approach, decomposition is performed by the user using potentially non-inductive conditions, and the inductive phase characterizations are computed by invariant inference. Successive loop splitting results in a sequence of phases, whereas our approach utilizes arbitrary automaton structures. Borralleras et al. [9] also refine the control-flow graph throughout the analysis by splitting on conditions, which here are discovered as preconditions for termination (the motivation is to expose termination proof goals to be established): in a sense, the phase structure is grown from candidate characterizations implying termination. This differs from our approach in which the phase structure is used to guide the inference of characterizations.

Quantified invariant inference. We focus here on the works on quantifiers in automatic verification most closely related to our work. In predicate abstraction, quantifiers can be used internally as part of the definitions of predicates, and also externally through predicates with free variables [25, 41]. Our work uses quantifiers both internally in phases characterizations and externally in view quantifiers. The view is also related to the bounded number of quantifiers used in view abstraction [6, 5]. In this work we observe that it is useful to consider views of entities beyond processes or threads, such as a single key in the store.

Quantifiers are often used to their full extent in verification conditions, namely checking implication between two quantified formulas, but they are sometimes employed in weaker checks as part of thread-modular proofs [4, 38]. This amounts to searching for invariants provable using specific instantiations of the quantifiers in the verification conditions [30, 36]. In our verification conditions, the view quantifiers are localized, in effect performing a single instantiation. This is essential for exploiting the disjunctive structure under the quantifiers, allowing inference to consider a single automaton edge in each step, and reflecting an intuition of correctness. When necessary to constrain interference, quantifiers in phase characterizations can be used to establish necessary facts about interfering views. Finally, there exist algorithms other than $\text{PDR}^{\forall}$ for solving CHC by predicates with universal invariants [e.g. 31, 20].

8 Conclusion

Invariant inference techniques aiming to verify intricate distributed protocols must adjust to the diverse correctness arguments on which protocols are based. In this paper we have proposed to use phase structures as means of conveying users’ intuition of the proof, to be used by an automatic inference tool as a basis for a full formal proof. We found that inference guided by a phase structure can infer proofs for distributed protocols that are beyond reach for state of the art inductive invariant inference methods, and can also improve the speed of convergence. The phase decomposition induced by the automaton, the use of disabled transitions, and the explicit treatment of phases in inference, all combine to direct the search for the invariant. We are encouraged by our experience of specifying phase structures for different protocols. It would be interesting to integrate the interaction via phase structures with other verification methods and proof logics, as well as interaction schemes based on different, complementary, concepts. Another important direction for future work is inference beyond universal invariants, required for example for the proof of Paxos [49].

Acknowledgements

We thank Kalev Alpernas, Javier Esparza, Neil Immerman, Oded Padon, Andreas Podelski, Tom Reps, and the anonymous referees for insightful comments which improved this paper. This publication is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No [759102-SVIS]). The research was partially supported by Len Blavatnik and the Blavatnik Family foundation, the Blavatnik Interdisciplinary Cyber Research Center, Tel Aviv University, the Israel Science Foundation (ISF) under grant No. 1810/18, the United States-Israel Binational Science Foundation (BSF) grant No. 2016260, and the National Science Foundation under Grant No. 1749570. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation.

Appendix 0.A Completeness of Inductive Phase Invariants

There are cases where a phase automaton $\mathcal{A}$ is a phase invariant for TS, but this cannot be established via an inductive phase invariant since there is no strengthening of its phase characterizations that leads to an inductive phase invariant for TS. This may happen for two reasons.

First, as with standard inductive invariants, it is possible that the strengthening necessary to ensure inductiveness is not expressible in the logic available to us.

Second, even if we assume an unrestricted language of phase characterizations, it is possible that the edge labeling is too permissive, thus adding transitions that are not necessary for the edge covering requirement. Such “redundant” transitions may sometimes be harmless, but they may also violate preservation along some edge. Namely, if no state that has such an outgoing transition can reach the corresponding phase $q$ from previous phases, such violations can be overcome by strengthening $\varphi_{q}$ to exclude all states that have such an outgoing transition (assuming an unrestricted language of phase characterizations), thus disabling the problematic transition along the edge. In these cases, an inductive automaton can be obtained. However, in other cases, strengthening the phase characterizations in this way would exclude states that can reach phase $q$ and as such would damage the inductiveness property along incoming edges of $q$. In such cases, the only way to disable problematic transitions along automaton edges is by strengthening the transition relation formulas (i.e., updating the automaton structure). Hence, no inductive automaton exists for the given phase structure. The second reason has no counterpart in standard inductive invariants; it reflects the additional structure expressed by a phase automaton, which is enforced by our stronger definition of inductiveness (as opposed to the weaker definition mentioned in Remark 2). Fortunately, this reason can be avoided by considering deterministic phase automata:

Lemma 5

Let $\mathcal{A}$ be a deterministic phase automaton, and assume an unrestricted language of phase characterizations. Then $\mathcal{A}$ is a phase invariant for TS if and only if it has a strengthening $\mathcal{A}^{\prime}$ that is inductive w.r.t. TS.

Proof (Proof (sketch))

The implication from right to left is clear. Consider the other direction. For a deterministic phase automaton, $\mathcal{L}({\textit{TS}})\subseteq\mathcal{L}(\mathcal{A})$ if and only if there exists a simulation relation between TS and $\mathcal{A}$. Furthermore, in this case, the inductiveness requirement coincides with the requirement that the phase characterizations induce a simulation relation. Hence, in this case, by defining the characterization of $q$ to include all the states simulated by it, we obtain an inductive strengthening of $\mathcal{A}$.

Non-determinism is generally unbeneficial as it only mandates some states to be characterized by multiple phases in the inductive phase invariant (see also Remark 2). We point out that restricting our attention to deterministic phase automata does not lose generality in the context of safety verification since every inductive phase invariant, which are the ones we seek, can be translated into a deterministic one, as the following lemma shows. Thus a structure admitting an inductive phase invariant can be converted to a deterministic one with the same property.

Lemma 6

Let $\mathcal{A}=(\mathcal{Q},\iota,\mathcal{V},\delta,\varphi)$ be an inductive phase invariant w.r.t. TS. Define an arbitrary total order, $<$, on $\mathcal{Q}$, and define $\mathcal{A}^{\prime}=(\mathcal{Q},\iota,\mathcal{V},\delta^{\prime},\varphi)$ where

[TABLE]

Then $\mathcal{A}^{\prime}$ is a deterministic inductive phase invariant w.r.t. TS.

We note that when the language of phase characterizations is restricted and an inductive phase automaton does not exist for this reason, it may be possible to overcome the limitations of the language and obtain one by changing the automaton structure.

Appendix 0.B Abstract Counterexample Traces

Phase structures may not admit a safe inductive phase invariant. In this section we discuss causes for this, and notions of concrete and abstract counterexample traces constituting a proof that inductive phase characterizations cannot be found over the given structure in the given language of candidate characterizations.

0.B.1 Concrete Counterexample Traces

We first consider the case where no safe inductive phase invariant exists, regardless of the language of phase characterizations. Such a case may be witnessed by a counterexample trace that exhibits a violation of one of the safety properties induced by $\mathcal{S}$.

Definition 7 (Counterexample Trace)

A trace $\sigma_{1},\ldots,\sigma_{n}$ of TS with a valuation $v$ for $\mathcal{V}$ is a counterexample trace for $\mathcal{S}$, TS and $\forall\mathcal{V}.\ \mathcal{P}$ if there exists a trace $q_{0},\ldots,q_{n}$ of $\mathcal{S}$ such that $({\sigma}_{i},\sigma_{i+1}),v\models\delta_{(q_{i},q_{i+1})}$ for every $1\leq i<n$, but one of the following holds:

A state in the trace is not safe: $\sigma_{i},v\not\models\mathcal{P}$ for some $i$. 2. 2.

A state in the trace allows a transition that is not covered by any outgoing edge: There exists $\sigma^{\prime}$ s.t. $(\sigma_{i},\sigma^{\prime})\models{\textit{TR}}$ for some $i$, but no edge can cover this transition, i.e. $(\sigma_{i},\sigma^{\prime}),v\not\models\delta_{(q_{i},q^{\prime})}$ for all $q^{\prime}\in\mathcal{Q}$.

Lemma 7

If a counterexample trace exists then there is no safe inductive phase invariant with structure $\mathcal{S}$, even if the language of phase characterizations is unrestricted.

In case 1, the trace violates the original safety property (enforced by Equation 4). This means that the transition system at hand is not safe and no safe inductive phase invariant can be expected, for any phase structure (by Lemma 3).

In case 2, the trace violates the “additional” safety property specified by the phase structure (Equation 3). This does not indicate that the transition system is not safe, but rather that the choices of the phase structure are intrinsically incorrect: it includes a trace such that a corresponding trace of the transition system reaches a state that allows a transition that is not covered by any outgoing edge in the automaton. If the phase structure is nondeterministic, this may indicate that some of the edges are redundant and prevent obtaining phase inductive characterizations even if it is a phase invariant. If the structure is deterministic (where every trace of TS corresponds to at most one trace of $\mathcal{A}$), this means that the automaton excludes true traces of the transition system and is therefore not a phase invariant, hence no corresponding inductive phase invariant exists. In both cases, TS may be safe but the user has to modify the phase structure in order to be able to verify it.

0.B.2 Abstract Counterexample Traces

In practice, phase characterizations are restricted since actual inference algorithms restrict their search space to a certain class of formulas. This may be viewed as a form of abstraction, and may be one of the potential causes of absence of inductive phase invariant. In this case, we may obtain an abstract counterexample trace that may indicate any of the violations discussed in Section 0.B.1, but may also reflect the limitations of the language of phase characterizations.

Language of Phase Characterization. We denote by $L$ the class of formulas used to represent phase characterizations. We denote by $L_{\Sigma}(\mathcal{V})$ the set of formulas in $L$ over vocabulary $\Sigma$ with free variables from $\mathcal{V}$. We assume an implication relation over $L$: for every $\psi_{1},\psi_{2}\in L_{\Sigma}(\mathcal{V})$, a structure $\sigma$ over $\Sigma$ and a valuation $v$ we have the relation $\sigma,v\models\psi_{1}\Longrightarrow\sigma,v\models\psi_{2}$. We use the implication relation to define a preorder on structures (accompanied by valuations) that captures which structure satisfies more formulas from $L_{\Sigma}(\mathcal{V})$:

Definition 8

For finite structures over $\Sigma$ and valuation $v$ for $\mathcal{V}$, we define $(\sigma_{1},v)\sqsubseteq_{L_{\Sigma}(\mathcal{V})}(\sigma_{2},v)$ if $v$ is defined in both $\sigma_{1}$ and $\sigma_{2}$ and for all $\psi\in L_{\Sigma}(\mathcal{V})$, $\sigma_{2},v\models\psi\Rightarrow\sigma_{1},v\models\psi$.

Intuitively, $(\sigma_{1},v)\sqsubseteq_{L_{\Sigma}(\mathcal{V})}(\sigma_{2},v)$ means that $(\sigma_{2},v)$ is more abstract than $(\sigma_{1},v)$: any formula in $L_{\Sigma}(\mathcal{V})$ that is satisfied by $(\sigma_{2},v)$ is also satisfied by $(\sigma_{1},v)$. In particular, no formula that is satisfied by $(\sigma_{2},v)$ can distinguish it from $(\sigma_{1},v)$. Note that $\sqsubseteq_{L_{\Sigma}(\mathcal{V})}$ is defined for structures paired with the same valuation, which means that they interpret $\mathcal{V}$ in the same way. We often omit $\Sigma$ and $\mathcal{V}$ from the notation and write $(\sigma_{1},v)\sqsubseteq_{L}(\sigma_{2},v)$.

Example 5 (Universal Characterizations)

Consider $L={\forall^{*}}$, i.e., the class of universally quantified formulas. In this case, $(\sigma_{1},v)\sqsubseteq_{{\forall^{*}}}(\sigma_{2},v)$ if $v$ is defined in both $\sigma_{1},\sigma_{2}$ and $\sigma_{1}$ is a substructure of $\sigma_{2}$ (up to isomorphism). (The structure $\sigma_{1}=({D}_{1},{\mathcal{I}}_{1})$ is a substructure of the structure $\sigma_{2}=({D}_{2},{\mathcal{I}}_{2})$ if ${D}_{1}\subseteq{D}_{2}$ and ${\mathcal{I}}_{2}$ agrees with ${\mathcal{I}}_{1}$ on ${D}_{1}$.That is, for every constant symbol $c\in\Sigma$, ${\mathcal{I}}_{2}(c)={\mathcal{I}}_{1}(c)$, for every function symbol $f\in\Sigma$ with arity $k$, ${\mathcal{I}}_{2}(f)(d_{1},\ldots,d_{k})={\mathcal{I}}_{1}(f)(d_{1},\ldots,d_{k})$ for every $d_{1},\ldots,d_{k}\in{D}_{1}$, and for every relation symbol $r\in\Sigma$ with arity $k$, ${\mathcal{I}}_{2}(r)\cap{D}_{1}^{k}={\mathcal{I}}_{1}(r)$. )

Abstract Traces. We view the preorder $\sqsubseteq_{L}$ as an abstraction relation, and use it to define a notion of an abstract trace, where each transition consists of an “abstraction step” followed by a concrete transition of the system. An abstraction step transitions to a “less abstract” state (that cannot be distinguished by any formula satisfied by the source of the transition – the more abstract state).

Definition 9 (Abstract Trace)

Given a transition system ${\textit{TS}}=(\textit{Init},{\textit{TR}})$ over vocabulary $\Sigma$, an abstract trace is a finite sequence of states ${\sigma}_{1},\ldots,{\sigma_{n}}$ over $\Sigma$ with a valuation $v$ over $\mathcal{V}$ which is defined in all $\sigma_{i}$ such that for every $1\leq i<n$, there exists $\tilde{\sigma_{i}}$ such that $(\tilde{\sigma}_{i},v)\sqsubseteq_{L}(\sigma_{i},v)$ and $(\tilde{\sigma}_{i},\sigma_{i+1})\models{\textit{TR}}$.

Note that since $\sqsubseteq_{L}$ is reflexive, $\tilde{\sigma_{i}}$ may be equal to $\sigma_{i}$, in which case the abstract trace is concrete.

An abstract counterexample trace is similar to a counterexample trace, except that it consists of an abstract trace. While the violation exhibited by an abstract counterexample trace may not be real, it indicates that no safe inductive phase invariant exists in $L$.

Lemma 8

If an abstract counterexample trace exists then there is no safe inductive phase invariant with structure $\mathcal{S}$ and phase characterizations in $L$.

Diagnosis of Abstract Counterexample Traces. When a user is presented with an abstract counterexample trace, diagnosing the cause of the trace assists the user in understanding whether (i) the program is faulty, (ii) the phase structure needs to be modified (and how), or (iii) the language of phase characterizations is not expressive enough to capture the required characterizations. These cases can be differentiated by performing bounded model checking along the given abstract counterexample trace. If a concrete trace is found, it demonstrates whether the system is not safe or the automaton needs to be changed. Otherwise, the counterexample is attributed to the limited logical language used for candidate characterizations. In this case, the user can proceed by extending the logical language, or modify the program and/or automaton so that they admit an inductive phase invariant in the given logical language.

Appendix 0.C Inductive Invariant for Sharded Key-Value Store

Appendix 0.D Overview of Phase-$\text{PDR}^{\forall}$

Our procedure is based on $\text{PDR}^{\forall}$ [39], a variant of PDR [10, 21] that infers universally quantified inductive invariants. PDR computes a sequence of frames, $\mathcal{F}_{0},\ldots,\mathcal{F}_{n}$ such that $\mathcal{F}_{i}$ overapproximates the set of states reachable in $i$ steps. In our case, each frame $\mathcal{F}_{i}$ is a mapping from a phase $q$ to a characterization.

We describe the gist of the procedure using the terminology of phase automata. An inductive trace is a sequence of frames such that $\forall\mathcal{V}.\ \mathcal{F}_{i}(q)\Longrightarrow\mathcal{F}_{i+1}(q)$ for all $i$ and $q\in\mathcal{Q}$, the first frame satisfies $\mathcal{F}_{0}(\iota)=\textit{Init}$ where $\iota$ is the initial phase and $\mathcal{F}_{0}(q)={\textit{false}}$ for other phases (in accordance with Equation 1), all frames satisfy Equations 3 and 4, and the constraint of Equation 2 is interpreted between successive frames, namely for all $0\leq i<n$ and for all $(q,p)\in\mathcal{R}$,

[TABLE]

These properties ensure that $\mathcal{F}_{i}$ induces phase characterizations such that the language of the induced phase automaton includes all traces of TS of length at most $i$.

The procedure gradually constructs the inductive trace by generating and blocking proof obligations, where a proof obligation $(m,q,i)$ consists of system state(s) $m$ that need to be proved unreachable at phase $q$ of the automaton at frame $i$ (i.e., with traces of length bounded by $i$). When a proof obligation is shown to hold, it is generalized into a new lemma that excludes the corresponding states and is added as a conjunct to the characterization of phase $q$ at frame $i$, where the phase characterizations of each frame are initially set to true.222Our description here omits some details, such as pushing lemmas between frames; see [21] for further discussion.

Proof obligations are generated by a backward traversal. First, whenever a new frame $\mathcal{F}_{n}$ is added, proof obligations are generated from counterexamples to the safety properties of Equations 3 and 4 in some phase $q^{\prime}$ based on $\mathcal{F}_{n}(q^{\prime})$. Then, to check whether a proof obligation $\psi$ at phase $q^{\prime}$ can be blocked in frame $\mathcal{F}_{i}$, our procedure checks whether the phase characterizations of its pre-phases in the previous frame suffice to show that $\psi$ holds in $q^{\prime}$ in accordance with constraint (2), i.e. $\forall\mathcal{V}.\ \left(\mathcal{F}_{i-1}(q)\land\delta_{(q,q^{\prime})}\Longrightarrow\psi^{\prime}\right)$ for all $q$ such that $(q,q^{\prime})\in\mathcal{R}$. Otherwise, there is a pre-phase $q$, a valuation $v$ and a transition $(\sigma,\sigma^{\prime}),v\models\delta_{(q,q^{\prime})}$ such that $\sigma,v\models\mathcal{F}_{i-1}(q)$ but $\sigma^{\prime},v\not\models\psi$. This generates a proof obligation $\theta$ for phase $q$ in frame $i-1$.

In $\text{PDR}^{\forall}$, the proof obligation $\theta$ is constructed as the diagram of the counterexample, which is the strongest existentially quantified abstraction of $\sigma$ [12]. In our case, $\theta={\textit{Diag}(\sigma,v,\mathcal{V})}$ is defined by

[TABLE]

where

• •

$\sigma$ has domain $\{e_{1},\ldots,e_{m}\}$ and interpretation ${\mathcal{I}}$.

• •

$\psi_{\text{distinct}}$ is a conjunction of all inequalities $x_{i}\neq x_{j}$ for $i\neq j$.

• •

$\psi_{\text{identity}}$ is a conjunction of the equalities $x_{i}=c$ if $c$ is a constant symbol and ${\mathcal{I}}(c)=e_{i}$, and of the equalities $x_{i}=y$ if $y\in\mathcal{V}$ and $v(y)=e_{i}$.

• •

$\psi_{\text{rels}}$ is a conjunction of atomic formulas $r(x_{i_{1}},\ldots,x_{i_{a}})$ for every relation symbol $r$ of arity $a$ and elements $\overline{e}=e_{i_{1}},\ldots,e_{i_{a}}$ such that $\overline{e}\in{\mathcal{I}}(r)$, and $\neg r(x_{i_{1}},\ldots,x_{i_{a}})$ if $\overline{e}\not\in{\mathcal{I}}(r)$. Function symbols are treated similarly.

Note that ${\textit{Diag}(\sigma,v,\mathcal{V})}$ has $\mathcal{V}$ as free variables. A proof obligation $({\textit{Diag}(\sigma,v,\mathcal{V})},q,i)$ is blocked by adding to the characterization of phase $q$ at frame $i$ a universally quantified clause (possibly with free variables in $\mathcal{V}$) that implies $\neg{\textit{Diag}(\sigma,v,\mathcal{V})}$.

The procedure continues to generate (and block) proof obligations across automaton edges, going backwards in the frames, until it reaches the initial frame. If a proof obligation does not hold there, the procedure has found an abstract counter-trace, and returns it as evidence of absence of a safe inductive phase invariant. The reason is that the backward traversal is performed over diagrams, where $({\sigma},v)\models{\textit{Diag}(\tilde{\sigma},v,\mathcal{V})}$ if and only if $\tilde{\sigma}$ is a substructure of ${\sigma}$ (up to isomorphism) [12], and hence if and only if $(\tilde{\sigma},v)\sqsubseteq_{{\forall^{*}}}({\sigma},v)$ (Example 5). Otherwise, the procedure terminates if one of the frames constitutes a solution to the CHC system, namely an inductive phase invariant.

Appendix 0.E Proofs

Proof

Given a domain ${D}$ and a valuation $v$, the phase characterizations of $\mathcal{A}$ induce the following simulation relation from TS to $\mathcal{A}$: $H=\{(\sigma,q)\,|\,\sigma,v\models\varphi_{q}\}$ in the sense that:

(Labeling) $(\sigma,q)\in H$ implies $\sigma,v\models\varphi_{q}$. 2. 2.

(Initial) For every $\sigma_{0}\models\textit{Init}$, $(\sigma_{0},\iota)\in H$. This follows from the initiation property of $\mathcal{A}$ (Definition 4). 3. 3.

(Step) For every transition $(\sigma,\sigma^{\prime})\models{\textit{TR}}$, if $(\sigma,q)\in H$ then there exists $p\in\mathcal{Q}$ such that $(\sigma^{\prime},p)\in H$ and $(\sigma,\sigma^{\prime}),v\models\delta_{(q,p)}$. This holds due to the edge covering and inductiveness properties of $\mathcal{A}$ (Definition 4): From edge covering, there exists $p\in\mathcal{Q}$ such that $(\sigma,\sigma^{\prime}),v\models\delta_{(q,p)}$. From inductiveness, necessarily $\sigma^{\prime},v\models\varphi_{p}^{\prime}$. Thus $(\sigma^{\prime},p)\in H$, as required.

Hence, for every ${D},v$, trace inclusion follows. ∎

Proof

Inductive phase invariant to inductive invariant: $\textit{Init}\Longrightarrow\text{Inv}_{\mathcal{A}}$ follows from the initiation condition of $\mathcal{A}$. For consecution, assume $\sigma\models\text{Inv}_{\mathcal{A}}$ and $(\sigma,\sigma^{\prime})\models{\textit{TR}}$. Then there is some $q\in\mathcal{Q}$ such that $\sigma\models\varphi_{q}$. From edge covering condition of $\mathcal{A}$, there exists $p\in\mathcal{Q}$ such that $(\sigma,\sigma^{\prime})\models\delta_{(q,p)}$. From the inductiveness condition of $\mathcal{A}$ necessarily $\sigma^{\prime}\models\varphi_{p}^{\prime}$, and thus $\sigma^{\prime}\models\text{Inv}^{\prime}_{\mathcal{A}}$, as required. The converse direction is clear. ∎

Proof

Consider the inductive invariant $I=\forall\mathcal{V}.\ \bigvee_{q\in\mathcal{Q}}{\varphi_{q}}$ per Lemma 2. The safety of $\mathcal{A}$ (Definition 5) implies that $I\Longrightarrow\forall\mathcal{V}.\,\mathcal{P}$, and the claim follows.

It is also possible to prove the lemma through phase invariants, by claiming that if $\mathcal{A}$ is safe and an invariant for TS then TS is safe: Let $\sigma_{1},\ldots,\sigma_{n}$ be a finite trace of TS. Let $v$ be a valuation for $\mathcal{V}$. $\overline{\sigma}\models\mathcal{A}$, so there exists a trace of phases $q_{0},\ldots,q_{n}$ such that $\sigma_{i},v\models\varphi_{q_{i}}$. Since $v\models\varphi_{q_{i}}\to\mathcal{P}$, for every $i$ it holds that $\sigma_{i},v\models\mathcal{P}$. The claim follows. ∎

Proof

Assume that $\mathbf{I}$ is a solution to the CHC system. Then $\mathcal{A}$ is a safe inductive phase invariant for TS: $\mathcal{A}$ satisfies initiation due to constraint 1, satisfies inductiveness due to constraint 2, and edge covering due to constraint 3, and thus $\mathcal{A}$ is inductive w.r.t. TS (Definition 4). Finally, $\mathcal{A}$ is safe (Definition 5) due to constraint 4.

Conversely, assume that $\mathcal{A}$ is an inductive phase invariant. Then constraint 1 is satisfied because $\mathcal{A}$ satisfies initiation, constraint 2 is satisfied because $\mathcal{A}$ satisfies inductiveness, and constraint 3 because $\mathcal{A}$ satisfies edge covering—all from the definition of an inductive phase invariant (Definition 4). Finally, constraint 4 is satisfied because $\mathcal{A}$ is safe (Definition 5). ∎

Proof

The implication from right to left is a consequence of Lemma 1. Consider the other direction. We construct an inductive phase invariant as follows: For a given valuation $v$, characterize each phase by the set of states that can reach this phase: reachability of $\sigma$ to phase $q$ means that there exist trace of program states $\sigma_{0},\ldots,\sigma_{n}=\sigma$ and a matching trace of phases $q_{0},\ldots,q_{n}=q$ per Definition 2. The result is indeed an inductive phase invariant: initiation follows from $\mathcal{A}$ being a phase invariant. Inductiveness follows from taking the characterizations to be sets of reachable states (recall that the language of characterizations is assumed to be unrestricted). It remains to argue that edge covering holds. Let $\sigma$ be reachable in phase $q$ and $(\sigma,\sigma^{\prime})\models{\textit{TR}}$. Thus there is a sequence of states program states $\sigma_{0},\ldots,\sigma_{n}=\sigma$ and a matching trace of phases $q_{0},\ldots,q_{n}=q$. Now, $\sigma^{\prime}$ is also reachable, and since $\mathcal{A}$ is a phase invariant there exists a trace of phases trace of phases $q^{\prime}_{0},\ldots,q^{\prime}_{n},q^{\prime}_{n+1}=q^{\prime}$ matching $\sigma_{0},\ldots,\sigma_{n},\sigma^{\prime}$. But $\mathcal{A}$ is deterministic, so necessarily $q^{\prime}_{n}=q_{n}$ (by induction over $n$) which is $q$. In particular this gives $(\sigma,\sigma^{\prime})\models\delta_{(q,p)}$ where $p=q^{\prime}_{n+1}$, as required.

∎

Proof

The definition of $\delta^{\prime}$ ensures that it is deterministic, and inherits the edge covering property from $\delta$. Initiation is not affected by the edge labeling, and inductiveness cannot be damaged by strengthening $\delta_{(q,p)}^{\prime}$. ∎

Proof

Follows from Lemma 8 with the identity preorder (or simply by reiterating the proof while ignoring abstraction steps).

Proof

For the sake of the proof, we explicitly split each transition in an abstract trace to an abstraction step followed by a transition. Let $(\sigma_{1},\tilde{\sigma}_{1},\ldots,\sigma_{n},\tilde{\sigma}_{n}),v)$ be such a trace and $q_{1},\ldots,q_{n}$ be as in the definition. Let $\mathcal{A}^{\prime}$ be a strengthening of $\mathcal{A}$ with phase characterization $\varphi^{\prime}$. Assume that $\mathcal{A}^{\prime}$ is safe and show that $\mathcal{A}^{\prime}$ is not inductive. Assume for the sake of contradiction that it is. We claim by induction on $i$ that $\sigma_{i},v\models\varphi_{q_{i}}^{\prime}$. The base claim follows from initiation. For the induction step, assume that $\sigma_{i},v\models\varphi_{q_{i}}^{\prime}$. Since $(\tilde{\sigma}_{i},v)\sqsubseteq_{L}(\sigma_{i},v)$ and $\varphi_{q_{i}}^{\prime}\in L$, $\tilde{\sigma}_{i},v\models\varphi_{q_{i}}^{\prime}$. Now $(\tilde{\sigma}_{i},\sigma_{i+1}),v\models\delta_{(q_{i},q_{i+1})}$, and from the assumption that $\mathcal{A}^{\prime}$ is inductive necessarily $\sigma_{i+1},v\models\varphi_{q_{i+1}}^{\prime}$, as required.

Let us consider the cause of the abstract counterexample trace. In case 1, $\sigma_{i},v\not\models\mathcal{P}$ is a contradiction to the safety of $\mathcal{A}^{\prime}$ (Definition 5). In case 2, if $(\sigma_{i},\sigma^{\prime})\models{\textit{TR}}$, since we have shown $\sigma_{i},v\models\varphi_{q_{i}}^{\prime}$ it must follow from edge covering that $(\sigma_{i},\sigma^{\prime}),v\models\delta_{(q_{i},q^{\prime})}$ for some $q^{\prime}\in\mathcal{Q}$, which is a contradiction. The claim follows. ∎