## 1 Introduction

The principle of strong induction, also known as -induction, is a generalization of (simple) induction that extends the base- and inductive-cases to steps of a transition system [27]. A safety property is -inductive in a transition system iff (a) is true in the first steps of , and (b) if is assumed to hold for consecutive steps, then holds in steps of . Simple induction is equivalent to -induction. Unlike induction, strong induction is complete for safety properties: a property is safe in a transition system iff there exists a natural number such that is -inductive in (assuming the usual restriction to simple paths). This makes -induction a powerful method for unbounded SAT-based Model Checking (SMC).

Unlike other SMC techniques, strong induction reduces model checking to pure SAT that does not require any additional features such as solving with assumptions [12], interpolation [24], resolution proofs [17], Maximal Unsatisfiable Subsets (MUS) [2]

, etc. It easily integrates with existing SAT-solvers and immediately benefits from any improvements in heuristics

[23, 22], pre- and in-processing [18], and parallel solving [1]. The simplicity of applying -induction made it the go-to technique for SMT-based infinite-state model checking [9, 11, 19]. In that context, it is particularly effective in combination with invariant synthesis [20, 14]. Moreover, for some theories, strong induction is strictly stronger than -induction [19]: there are properties that are -inductive, but have no -inductive strengthening.Notwithstanding all of its advantages, strong induction has been mostly displaced by more recent SMC techniques such as Interpolation [25], Property Directed Reachability [7, 13, 15, 3], and their combinations [29]. In SMC -induction is equivalent to induction: any -inductive property can be strengthened to an inductive property [16, 6]. Even though in the worst case is exponentially larger than [6], this is rarely observed in practice [26]. Furthermore, the SAT queries get very hard as increases and usually succeed only for rather small values of . A recent work [16] shows that strong induction can be integrated in Pdr. However, [16] argues that -induction is hard to control in the context of Pdr since choosing a proper value of is difficult. A wrong choice leads to a form of state enumeration. In [16], is fixed to , and regular induction is used as soon as -induction fails.

In this paper, we present kAvy, an SMC algorithm that effectively uses -induction to guide interpolation and Pdr-style inductive generalization. As many state-of-the-art SMC algorithms, kAvy iteratively constructs candidate inductive invariants for a given safety property . However, the construction of these candidates is driven by -induction. Whenever is known to hold up to a bound , kAvy searches for the smallest , such that either or some of its strengthening is -inductive. Once it finds the right and strengthening, it computes a -inductive strengthening.

It is convenient to think of modern SMC algorithms (e.g., Pdr and Avy), and
-induction, as two ends of a spectrum. On the one end, modern SMC algorithms
fix to and *search* for a -inductive strengthening of . While
on the opposite end, -induction fixes the strengthening of to be
itself and *searches* for a such that is -inductive. kAvy *dynamically* explores this spectrum, exploiting the interplay between
finding the right and finding the right strengthening.

As an example, consider a system in Fig. 1 that counts upto and
resets. The property, , is -inductive. IC3, Pdr and Avy iteratively guess a -inductive strengthening of . In the worst case, they
require at least iterations. On the other hand, kAvy determines that
is -inductive after iterations, *computes* a -inductive invariant
, and terminates.

kAvy builds upon the foundations of Avy [29]. Avy first uses Bounded Model Checking [4] (BMC) to prove that the property holds up to bound . Then, it uses a sequence interpolant [28] and Pdr-style inductive-generalization [7] to construct -inductive strengthening candidate for . We emphasize that using -induction to construct -inductive candidates allows kAvy to efficiently utilize many principles from Pdr and Avy. While maintaining -inductive candidates might seem attractive (since they may be smaller), they are also much harder to generalize effectively [7].

We implemented kAvy in the Avy Model Checker, and evaluated it on the benchmarks from the Hardware Model Checking Competition (HWMCC). Our experiments show that kAvy significantly improves the performance of Avy and solves more examples than either of Pdr and Avy. For a specific family of examples from [21], kAvy exhibits nearly constant time performance, compared to an exponential growth of Avy, Pdr, and -induction (see Fig. (b)b in Section 5). This further emphasizes the effectiveness of efficiently integrating strong induction into modern SMC.

The rest of the paper is structured as follows. After describing the most relevant related work, we present the necessary background in Section 2 and give an overview of SAT-based model checking algorithms in Section 3. kAvy is presented in Section 4, followed by presentation of results in Section 5. Finally, we conclude the paper in Section 6.

##### Related work.

kAvy builds on top of the ideas of IC3 [7] and Pdr [13]. The use of interpolation for generating an inductive trace is inspired by Avy [29]. While conceptually, our algorithm is similar to Avy, its proof of correctness is non-trivial and is significantly different from that of Avy. We are not aware of any other work that combines interpolation with strong induction.

There are two prior attempts enhancing Pdr-style algorithms with -induction. Pd-Kind [19] is an SMT-based Model Checking algorithm for infinite-state systems inspired by IC3/Pdr. It infers -inductive invariants driven by the property whereas kAvy infers -inductive invariants driven by -induction. Pd-Kind uses recursive blocking with interpolation and model-based projection to block bad states, and -induction to propagate (push) lemmas to next level. While the algorithm is very interesting it is hard to adapt it to SAT-based setting (i.e. SMC), and impossible to compare on HWMCC instances directly.

The closest related work is KIC3 [16]. It modifies the counter example queue management strategy in IC3 to utilize -induction during blocking. The main limitation is that the value for must be chosen statically ( is reported for the evaluation). kAvy also utilizes -induction during blocking but computes the value for dynamically. Unfortunately, the implementation is not available publicly and we could not compare with it directly.

## 2 Background

In this section, we present notations and background that is required for the description of our algorithm.

##### Safety Verification.

A symbolic transition system is a tuple
, where is a set of Boolean *state*
variables. A state of the system is a complete valuation to all variables in
(i.e., the set of states is ). We write ) for the set of *primed* variables, used to represent
the next state. and are formulas over denoting the set of
initial states and bad states, respectively, and is a formula over , denoting the transition relation. With abuse of notation, we use
formulas and the sets of states (or transitions) that they represent
interchangeably. In addition, we sometimes use a state to denote the formula
(cube) that characterizes it. For a formula over , we use
, or in short, to denote the formula in which every
occurrence of is replaced by . For simplicity of
presentation, we assume that the property is true in the initial
state, that is .

Given a formula , an -to--*unrolling* of , where
holds in all intermediate states is defined by the formula:

(1) |

We write when and when .

A transition system is UNSAFE iff there exists a state
s.t. is reachable, and is SAFE otherwise. Equivalently, is UNSAFE
iff there exists a number such that the following *unrolling* formula
is satisfiable:

(2) |

is SAFE if no such exists. Whenever is UNSAFE and is a
reachable state, the path from to is called a
*counterexample*.

An *inductive invariant* is a formula that satisfies:

(3) |

A transition system is SAFE iff there exists an inductive
invariant s.t. . In this case we say that
is a *safe* inductive invariant.

The *safety* verification problem is to decide whether a transition
system is SAFE or UNSAFE, i.e., whether there exists a safe inductive
invariant or a counterexample.

##### Strong Induction.

Strong induction (or -induction) is a
generalization of the notion of an inductive invariant that is similar to how
“simple” induction is generalized in mathematics. A formula is
*-invariant* in a transition system if it is true in the first
steps of . That is, the following formula is valid:
.
A formula is a *-inductive invariant*
iff is a -invariant and is inductive after steps of , i.e., the
following formula is valid: .
Compared to simple induction, -induction strengthens the hypothesis in the
induction step: is assumed to hold between steps to and is
established in step . Whenever , we say that is a safe
-inductive invariant. An inductive invariant is a -inductive
invariant.

###### Theorem 2.1

Given a transition system . There exists a safe inductive invariant w.r.t. iff there exists a safe -inductive invariant w.r.t. .

Theorem 2.1 states that -induction principle is as complete as -induction. One direction is trivial (since we can take ). The other can be strengthened further: for every -inductive invariant there exists a -inductive strengthening such that . Theoretically might be exponentially bigger than [6]. In practice, both invariants tend to be of similar size.

We say that a formula is *-inductive relative* to if it is a
-invariant and .

##### Craig Interpolation [10].

We use an extension of Craig Interpolants to sequences, which is common in Model
Checking. Let such that is
unsatisfiable. A *sequence interpolant* for is a
sequence of formulas such that (a) ,
(b) , (c) , and (d) is over variables that are shared between the
corresponding prefix and suffix of .

## 3 SAT-based Model Checking

In this section, we give a brief overview of SAT-based Model Checking algorithms: IC3/Pdr [7, 13], and Avy [29]. While these algorithms are well-known, we give a uniform presentation and establish notation necessary for the rest of the paper. We fix a symbolic transition system .

The main data-structure of these algorithms is a sequence of candidate
invariants, called an *inductive trace*. An *inductive trace*, or
simply a trace, is a sequence of formulas that satisfy the
following two properties:

(4) |

An element of a trace is called a *frame*.
The index of a frame is called a *level*. is *clausal*

when all its elements are in CNF. For convenience, we view a frame as a set of clauses, and assume that a trace is padded with

until the required length. The*size*of is . For , we write for the -suffix of .

A trace of size is *stronger* than a trace of size iff
. A trace is
*safe* if each is safe: ;
*monotone* if . In a monotone
trace, a frame over-approximates the set of states reachable in up to
steps of the . A trace is closed if .

We define an unrolling formula of a -suffix of a trace as :

(5) |

We write to denote an unrolling of a -suffix of (i.e itself).
Intuitively, is satisfiable iff there is a -step execution of
the that is consistent with the -suffix . If a transition system
admits a safe trace of size , then does not admit
counterexamples of length less than . A safe trace , with is
*extendable* with respect to level iff there exists a safe
trace stronger than such that and . and the corresponding level are called an
*extension trace* and an *extension level* of , respectively.
SAT-based model checking algorithms work by iteratively extending a given safe
trace of size to a safe trace of size .

An extension trace is not unique, but there is a largest extension level. We denote the set of all extension levels of by . The existence of an extension level implies that an unrolling of the -suffix does not contain any states:

###### Proposition 1

Let be a safe trace. Then, , , is an extension level of iff the formula is unsatisfiable.

###### Example 1

For Fig. 1, is a safe trace of size . The formula is satisfiable. Therefore, there does not exists an extension trace at level . Since is unsatisfiable, the trace is extendable at level . For example, a valid extension trace at level is .

Both Pdr and Avy iteratively extend a safe trace either until the extension is closed or a counterexample is found. However, they differ in how exactly the trace is extended. In the rest of this section, we present Avy and Pdr through the lens of extension level. The goal of this presentation is to make the paper self-contained. We omit many important optimization details, and refer the reader to the original papers [13, 7, 29].

Pdr maintains a monotone, clausal trace with as the first frame
(). The trace is extended by recursively computing and blocking (if
possible) states that can reach (called *bad states*). A bad state
is blocked at the largest level possible. Alg. 1 shows
PdrBlock, the backward search procedure that identifies and blocks bad states.
PdrBlock maintains a queue of states and the levels at which they have to be
blocked. The smallest level at which blocking occurs is tracked in order to show
the construction of the extension trace. For each state in the queue, it is
checked whether can be blocked by the previous frame
(line 1). If not, a predecessor state of
that satistisfies is computed and added to the
queue (line 1). If a predecessor state is found at level ,
the trace is not extendable and an empty trace is returned. If the state is
blocked at level , PdrIndGen, is called to generate a clause that
blocks and possibly others. The clause is then added to all the frames at
levels less than or equal to . PdrIndGen is a crucial optimization
to Pdr. However, we do not explain it for the sake of simplicity. The procedure
terminates whenever there are no more states to be blocked (or a counterexample
was found at line 1). By construction, the output trace
is an extension trace of at the extension level . Once Pdr extends its trace, PdrPush is called to check if the clauses it learnt
are also true at higher levels. Pdr terminates when the trace is closed.

Avy, shown in Alg. 2, is an alternative to Pdr that combines interpolation and recursive blocking. Avy starts with a trace , with , that is extended in every iteration of the main loop. A counterexample is returned whenever is not extendable (line 2). Otherwise, a sequence interpolant is extracted from the unsatisfiability of . A longer trace is constructed using the sequence interpolant (line 2). Observe that is an extension trace of . While is safe, it is neither monotone nor clausal. A helper routine AvyMkTrace is used to convert to a proper Pdr trace on line 2 (see [29] for the details on AvyMkTrace). Avy converges when the trace is closed.

## 4 Interpolating -Induction

In this section, we present kAvy, an SMC algorithm that uses the principle of strong induction to extend an inductive trace. The section is structured as follows. First, we introduce a concept of extending a trace using relative -induction. Second, we present kAvy and describe the details of how -induction is used to compute an extended trace. Third, we describe two techniques for computing maximal parameters to apply strong induction. Unless stated otherwise, we assume that all traces are monotone.

A safe trace , with , is *strongly extendable* with respect
to , where , iff there exists a safe inductive trace
stronger than such that and . We
refer to the pair as *a strong extension level (SEL)*, and to the
trace as an *-extension trace*, or simply a *strong
extension trace (SET)* when is not important. Note that for ,
is just an extension trace.

###### Example 2

For Fig. 1, the trace is strongly extendable at level . A valid -externsion trace is . Note that is -inductive relative to , i.e. .

We write for the set of all SELs of . We define an order on SELs by : iff (i) ; or (ii) . The maximal SEL is .

Note that the existence of a SEL means that an unrolling of the -suffix
with repeated times does not contain any bad states. We use to denote this *characteristic formula* for SEL :

(6) |

###### Proposition 2

Let be a safe trace, where . Then, , , is an SEL of iff the formula is unsatisfiable.

The level in the maximal SEL of a given trace is greater or equal to the maximal extension level of :

###### Lemma 1

Let , then .

Hence, extensions based on maximal SEL are constructed from frames at higher level compared to extensions based on maximal extension level.

###### Example 3

#### 4.0.1 kAvy Algorithm

kAvy is shown in Fig. 3. It starts with an inductive trace and iteratively extends using SELs. A counterexample is returned if the trace cannot be extended (line 3). Otherwise, kAvy computes the largest extension level (line 3) (described in Section 4.2). Then, it constructs a strong extension trace using kAvyExtend (line 3) (described in Section 4.1). Finally, PdrPush is called to check whether the trace is closed. Note that is a monotone, clausal, safe inductive trace throughout the algorithm.

### 4.1 Extending a Trace with Strong Induction

In this section, we describe the procedure kAvyExtend (shown in Alg. 4) that given a trace of size and an SEL of constructs an -extension trace of size . The procedure itself is fairly simple, but its proof of correctness is complex. We first present the theoretical results that connect sequence interpolants with strong extension traces, then the procedure, and then details of its correctness. Through the section, we fix a trace and its SEL .

##### Sequence interpolation for SEL.

Let be an SEL of . By Proposition 2, is unsatisfiable. Let be a partitioning of defined as follows:

Since , is unsatisfiable. Let be a sequence interpolant corresponding to . Then, satisfies the following properties:

() | ||||||

Note that in ( ‣ 4.1), both and are fixed — they are the -extension level. Furthermore, in the top row is fixed as well.

The conjunction of the first interpolants in is -inductive relative to the frame :

###### Lemma 2

The formula is -inductive relative to .

###### Proof

Since and are consecutive frames of a trace, . Thus, . Moreover, by ( ‣ 4.1), and . Equivalently, . By induction over the difference between and , we show that , which concludes the proof.∎

We use Lemma 2 to define a strong extension trace :

###### Lemma 3

Let , be an inductive trace defined as follows:

Then, is an -extension trace of (not necessarily monotone).

###### Proof

By Lemma 2, is -inductive relative to . Therefore, it is sufficient to show that is a safe inductive trace that is stronger than . By definition, . By ( ‣ 4.1), and . By induction over , for all . Since is monotone,

By ( ‣ 4.1), . Again, since is a trace, we conclude that . Combining the above, for . Since is safe and , then is safe and stronger than . ∎

Lemma 3 defines an obvious procedure to construct an -extension trace for . However, such is neither monotone nor clausal. In the rest of this section, we describe the procedure kAvyExtend that starts with a sequence interpolant (as in Lemma 3), but uses PdrBlock to systematically construct a safe monotone clausal extension of .

The procedure kAvyExtend is shown in Alg. 4. For simplicity of the presentation, we assume that PdrBlock does not use inductive generalization. The invariants marked by rely on this assumption. We stress that the assumption is for presentation only. The correctness of kAvyExtend is independent of it.

kAvyExtend starts with a sequence interpolant according to the partitioning
. The extension trace is initialized to and is
initialized to (line 4). The rest proceeds in three phases:
*Phase 1* (lines 4–4) computes the prefix
using the first elements of ;
*Phase 2* (line 4) computes using ;
*Phase 3* (lines 4–4) computes the suffix
using the last elements of . During this phase, PdrPush (line 4) pushes clauses forward so that they can be used in the next iteration. The correctness of the
phases follows from the invariants shown in Alg. 4. We
present each phase in turn.

Recall that PdrBlock takes a trace (that is safe up to the last frame) and a transition system, and returns a safe strengthening of , while ensuring that the result is monotone and clausal. This guarantee is maintained by Alg 4, by requiring that any clause added to any frame of is implicitly added to all frames below .

##### Phase 1.

By Lemma 2, the first elements of the sequence interpolant computed at line 4 over-approximate states reachable in steps of . Phase 1 uses this to strengthen using the first elements of . Note that in that phase, new clauses are always added to frame , and all frames before it!

Correctness of Phase 1 (line 4) follows from the loop invariant . It holds on loop entry since (since and ( ‣ 4.1)) and (since is initially a trace). Let and be the frame before and after execution of iteration of the loop, respectively. PdrBlock blocks at iteration of the loop. Assume that holds at the beginning of the loop. Then, since PdrBlock strengthens . Since and , this simplifies to . Finally, since is a trace, holds at the end of the iteration.

ensures that the trace given to PdrBlock at
line 4 *can* be made safe relative to . From the post-condition of
PdrBlock, it follows that at iteration , is strengthened to
such that and
remains a monotone clausal trace. At the end of *Phase 1*,
is a clausal monotone trace.

Interestingly, the calls to PdrBlock in this phase do not satisfy an expected pre-condition: the frame in might not be safe for property . However, we can see that and from , it is clear that is inductive relative to . This is a sufficient precondition for PdrBlock.

##### Phase 2.

This phase strengthens using the interpolant . After Phase 2, is -inductive relative to .

##### Phase 3.

Unlike *Phase 1*, is computed at the
iteration. Because of this, the property in this phase is
slightly different than that of Phase 1. Correctness follows from invariant
that ensures that at iteration , *can* be
made safe relative to . From the post-condition of PdrBlock, it follows
that is strengthened to such that
and is a monotone clausal trace. The invariant implies that at the end of
the loop , making safe. Thus, at the end
of the loop is a safe monotone clausal trace that is stronger than
. What remains is to show is that is -inductive relative to
.

Let be the formula from Lemma 2. Assuming that
PdrBlock did no inductive generalization, *Phase 1* maintains
, which states that at iteration ,
PdrBlock strengthens frames , .
holds on loop entry, since initially . Let
, ( ) be frame at the beginning and at
the end of the loop iteration, respectively. In the loop, PdrBlock adds clauses
that block . Thus, . Since , this simplifies to .
Expanding , we get . Thus,

Comments

There are no comments yet.