Proof Assisted Symbolic Model Checking for B and Event-B

Abstract

We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B. The high-level nature of B and Event-B accounts for complicated constraints arising in these symbolic analysis techniques. In this paper we suggest using static information stemming from proof obligations to simplify occurring constraints. We show how to include proof information in the aforementioned algorithms. Using different benchmarks we compare explicit state to symbolic model checking as well as techniques with and without proof assistance. In particular for models with large branching factor, e.g., due to complicated data values being manipulated, the symbolic techniques fare much better than explicit state model checking. The inclusion of proof information results in further clear performance improvements.

S. Krings and M. Leuschel—Part of this research has been initially sponsored by the EU funded FP7 project 287563 (ADVANCE).

1 Introduction and Motivation

Model checking is one of the key techniques used in formal software development. Two variants are currently in use: explicit state model checking and symbolic model checking. In explicit state model checking, every state is computed, the invariant is verified and discovered successor states are queued to be analyzed themselves. Symbolic model checking on the other hand tries to represent the state space and possible paths through it by predicates representing multiple states at once. Instead of stepwise exploration of the state space graph, the model checking problem is encoded as a formula and given to a constraint solver.¹

So far, existing model checkers for B and Event-B like ProB [20, 21], Eboc [23], pyB [30] or TLC [31] (via [17]) rely on explicit state model checking. ProB features some symbolic techniques for error detection [14] and test-case generation [27], but not full-blown symbolic model checking. This is mostly due to the high-level nature of B and Event-B. Both the usage of higher-order constructs and the underlying non-determinism accounts for complicated constraints during symbolic model checking. Some complexity can be coped with by relying on SMT solvers [12] or SAT solvers [25], but this is not always the case.

In this paper we have implemented various symbolic model checking algorithms for B and then study various ways to use proof information to optimize them. The proof information is used to strengthen constraints and reduce the counterexample search space. For Event-B, the information stems from discharged proof obligations exported from Rodin [1]. For classical B, no automatic proof information is available at the moment within ProB.² However, we can recompute the information using ProB’s proof capabilities as outlined in [18]. Essentially, for a B operation with before-after-predicate BA we search for a solution to

$$\begin{aligned} invariant(x) \wedge BA(x,x') \wedge \lnot conjunct\_of\_invariant(x'). \end{aligned}$$

If ProB reports a contradiction, we know that the operation can not lead to a violation of the particular conjunct. In addition to the technique in [18], we developed a bridge to the Atelier B provers ml and pp.

All techniques used in this paper have been implemented both for classical B and Event-B. Both languages will be used in our empirical evaluation. For the sake of brevity we will only talk about Event-B events in the following sections instead of distinguishing events and operations.

We will introduce the model checking algorithms BMC, k-Induction and IC3 in Sects. 2.1, 2.2, and 2.3. For each of them we will show how to include proof information into the occurring constraints. Following, in Sect. 3, we will empirically compare symbolic model checking to explicit state model checking and model checking with and without proof assistance. Discussion and conclusions will be presented in Sect. 4.

2 Proof Assisted Symbolic Model Checking

When using the B method to develop a software or system, one often alternates between different phases. Among those are writing and adapting the specification, manual and automated proof efforts as well as model checking. Yet, the different steps are only loosely coupled when it comes to tool support.

In [4] the authors have shown how to augment explicit state model checking with proof information. In the following, we introduce three symbolic model checking techniques for B and incorporate proof information in a similar fashion.

Fig. 1.

A simple, erroneous B machine

We will use the running example in Fig. 1 to illustrate various concepts in our paper. First, let us introduce the notation we will be using. By x we will denote a vector of state variables. $x'$ denotes the state variables in the successor state. A predicate p over the state variables x is denoted by p(x). The same predicate over the successor state is written as $p(x')$. By $Events$ we denote the set of events of a B machine. By $Inv$ we denote its invariant.

Definition 1

For an event $evt \in Events$ let $BA _{evt}(x,x')$ denote the before-after-predicate connecting state variables in x to their successors in $x'$.

Definition 2

For a predicate $p = \bigwedge _{i \in I} p_i$ and event evt let $proven _{evt,p}$ denote a set of conjuncts $p_i$ that are proven to hold after the execution of evt on a p-state, i.e., we have $proven _{evt,p} = \bigwedge _{i \in J} p_i$ for some $J \subseteq I$ such that

$$\begin{aligned} \forall x,x' . p(x) \wedge BA _{evt}(x,x') \Rightarrow proven _{evt,p}(x'). \end{aligned}$$

Let $unproven _{evt,p} = \bigwedge _{i \in I \setminus J} p_i$ denote the complement of $proven _{evt,p}$, i. e., all the conjuncts of p that are not in $proven _{evt,p}$. We also define $proven _{evt}$ = $proven _{evt, Inv }$ and $unproven _{evt}$ = $unproven _{evt, Inv }$.

For the example in Fig. 1, we have $BA _{incby}(c,c')$ = $\exists i \in 1..64 \wedge c'=c+i$. Furthermore, $proven _{incby}(c)$ = $c\ge 0$; the invariant $c\ge 0$ is preserved by incby. This implies $unproven _{incby}(c)$ = $c \le m$.

In our current implementation, we have that $proven _{evt,p} = \bigwedge _{j \in J} p_j$ with $J \subseteq I$. This however is not a strict limitation. One could add other predicates discovered to be implied to $proven _{evt,p}$ so as to further strengthen the predicates given below.

Lemma 1

A valid solution for Definition 2 is always $proven _{evt,p} = true$, meaning that nothing is proven for the event evt. At the other extreme, if all conjuncts of p are proven to hold after the execution of evt then $proven _{evt,p} = p$ and $unproven _{evt,p} = true$.

Definition 3

By $T$ we refer to a monolithic transition predicate, i. e., the disjunction of all before-after-predicates: $T (x,x')$ = $\bigvee _{e\in Events } BA _{e}(x,x')$. By $I$ we denote the after predicate of the initialization; including the properties about the constants.

For Fig. 1 we have $I (c)$ = $m \in \{127,255\} \wedge c=0$.

In the following sections, we show how proof information can be embedded in the queries of bounded model checking (Sect. 2.1), k-Induction based model checking (Sect. 2.2) and IC3 (Sect. 2.3). An empirical evaluation of the algorithms and the influence of using proof information will be performed in Sect. 3.

2.1 BMC — Bounded Model Checking

BMC [5] has been suggested by Armin Biere et al. in 1999 [6]. One of the main goals is to avoid the blowup and resulting slow down of BDDs-based model checking algorithms. This is achieved by replacing the BDDs by a SAT solver.

The basic idea is as follows: For an initial state relation $I$, a transition relation $T$ and a property p and a bound k starting with $k=0$, a sequence of propositional formulas is generated. Each of the formulas is satisfiable if and only if there exists a counterexample to the property with length $\le k$. This can be expressed as:

$$\begin{aligned} BMC(p,k) = I (s_0) \wedge \bigwedge _{i=0}^{k-1} T (s_i,s_{i+1}) \wedge \bigvee _{i=0}^k \lnot p(s_i) \end{aligned}$$

In order to include proof information we have to rewrite the predicate. First of all, if we increase k step-by-step as done in ProB’s implementation of BMC, it is sufficient to check only the last state for a violation of p:

$$\begin{aligned} BMC(p,k) = I(s_0) \wedge \bigwedge _{i=0}^{k-1} T (s_i,s_{i+1}) \wedge \lnot p(s_k) \end{aligned}$$

For the example machine in Fig. 1, we have:

$$\begin{aligned} BMC( Inv ,0)&= m \in \{127,255\} \wedge c_{0}=0 \wedge \lnot (c_{0}\ge 0 \wedge c_{0} \le m) \end{aligned}$$

(1)

$$\begin{aligned} BMC( Inv ,1)&= m \in \{127,255\} \wedge c_{0}=0 \wedge \exists i.(i \in 1..64 \wedge c_{1} = c_{0}+i) \nonumber \\&~~~~ \wedge \lnot (c_{1}\ge 0 \wedge c_{1} \le m) \end{aligned}$$

(2)

$$\begin{aligned} BMC( Inv ,2)&= m \in \{127,255\} \wedge c_{0}=0 \wedge \exists i.(i \in 1..64 \wedge c_{1} = c_{0}+i) \nonumber \\&~~~~ \wedge \exists i.(i \in 1..64 \wedge c_{2} = c_{1}+i) \wedge \lnot (c_{2}\ge 0 \wedge c_{2} \le m) \end{aligned}$$

(3)

ProB’s constraint solver finds no solution for Eqs. (1) and (2), but does so for Eq. (3): $m=127,c_{0}=0,c_{1}=64,c_{2}=128$. One can see that the constraint solver has instantiated the parameter of the event in such a way as to violate the invariant. ProB’s classical model checker on the other hand “blindly” enumerates all 64 possible successor states. Using breadth-first search, the counterexample is found after having generated 325 states and 12420 transitions; taking ${\sim }1.5s$ whereas BMC finds the counterexample with $k=2$, i.e., after three calls to the constraint solver and ${\sim }1s$. A depth-first search may generate a long counterexample of up to 127 steps, depending in which order the successors are processed. ProB in this case actually processes the successors with the larger i values first; leading to a counterexample of length 4 after generating 324 states and 323 transitions. The state space is shown in Fig. 2, the corresponding counterexample is shown in Fig. 3. The larger the branching-factor, the better BMC becomes as compared to explicit state model checking. When the number of possible parameter values becomes unbounded, e.g., supposing the incby event had no upper bound on i, BMC is often the only practical solution.³

Fig. 2.

State space of explicit state model checking

Fig. 3.

Counterexample found by BMC

Next, we extend the transition relation to either assert a property after every step or assert its negation:

Definition 4

For a predicate p we define $T _{p}$ and $T ^{\lnot }_{p}$ by

$$ T _{p}(x,x') = \bigvee _{e\in Events } ( BA _{e}(x,x') \wedge p(x'))$$

$$ T ^{\lnot }_{p}(x,x') = \bigvee _{e\in Events } ( BA _{e}(x,x') \wedge proven _{evt,p}(x') \wedge \lnot unproven _{evt,p}(x'))$$

For $k\ge 1$, the proven conjuncts of p can be used to strengthen the constraint:

$$\begin{aligned} \begin{aligned} BMC(p,k)&= I (s_0) \wedge p(s_{0}) \wedge \bigwedge _{i=0}^{k-2} T _{p}(s_i,s_{i+1}) \wedge T ^{\lnot }_{p}(s_{k-1},s_{k}) \end{aligned} \end{aligned}$$

(4)

For the example machine in Fig. 1, we have that for $k=0$ the constraint remains unchanged, but for $k=1$ and $k=2$ we obtain:

$$\begin{aligned} BMC( Inv ,0)&= m \in \{127,255\} \wedge c_{0}=0 \wedge \lnot (c_{0} \le m) \\ BMC( Inv ,1)&= m \in \{127,255\} \wedge c_{0}=0 \nonumber \\&~~~\, \wedge \exists i.(i \in 1..64 \wedge c_{1} = c_{0}+i) \wedge c_{1}\ge 0 \wedge \lnot (c_{1} \le m) \\ BMC( Inv ,2)&= m \in \{127,255\} \wedge c_{0}=0 \nonumber \\&~~~\, \wedge \exists i.(i \in 1..64 \wedge c_{1} = c_{0}+i) \wedge c_{1}\ge 0 \wedge c_{1} \le m \nonumber \\&~~~\, \wedge \exists i.(i \in 1..64 \wedge c_{2} = c_{1}+i) \wedge c_{2}\ge 0 \wedge \lnot ( c_{2} \le m) \end{aligned}$$

Remember that $unproven _{evt,p}(s_k)$ evaluates to true if all conjuncts of p have been proven to hold after the execution of evt. Hence, for completely proven events $\lnot unproven _{evt,p}(s_k)$ is false and the corresponding disjunct in $T ^{\lnot }_{p}$ is obviously unsatisfiable. However, we can not remove such completely proven events from the first $k-1$ steps as they might contribute to the path to a violation of p, using another final event.

Another BMC approach is to use the test-case generation algorithm from [27], using $\lnot p$ as target predicate. In contrast to the BMC technique above, the transition predicate is not monolithic, and the algorithm builds up a tree of feasible paths. We have extended the algorithm from [27] to also use $\lnot unproven _{evt,p}$ instead of $\lnot p$, where evt is the last event of any given path. The algorithm optionally uses a static enabling analysis to filter out infeasible paths before calling the solver. In the remainder of the paper we refer to this algorithm as BMC$^*$.

2.2 k-Induction

k-Induction [29] is a mixture of BMC and proof by induction. For the method to be complete, one has to avoid getting stuck in loops. Hence, the constraints are strengthened to avoid a state occurring twice on a given path.⁴

The base condition is encoded in Eq. (5); it is basically a BMC step and tries to find a counterexample of length k starting from the initialization. Like in Sect. 2.1 we assume that we gradually increase the value of k starting from 0, as shown in Algorithm 1. The inductive step, including the uniqueness of states, is expressed in Eq. (6), where $Axm$ are the axioms on the constants of the model (e.g., $m \in \{127,255\}$ in our running example).

$$\begin{aligned} Base(p,k) = I(s_0) \wedge \bigwedge _{i=0}^{k-1} T(s_i,s_{i+1}) \wedge \lnot p(s_k) \end{aligned}$$

(5)

$$\begin{aligned} Step(p,k) = Axm \wedge \bigwedge _{0 \le i < j \le k} s_i \ne s_j \wedge \bigwedge _{i=0}^{k} T _(s_i,s_{i+1}) \wedge \bigwedge _{i=0}^k p(s_i) \wedge \lnot p(s_{k+1}) \end{aligned}$$

(6)

For $k=0$ $Step( Inv ,k)$ corresponds to trying to find counterexamples to the B invariant preservation proof obligations. In a similar fashion, $Base( Inv ,0)$ corresponds to finding initial states which violate the invariant. Hence, if Base(p, 0) and Step(T, p, 0) are unsatisfiable, we have found an inductive proof of the property p. However, the difference with B’s approach to proving invariants does appear when Step(T, p, 0) is satisfiable, i.e., there exists a state which satisfies p and a successor state violates p. The k-induction method tries to construct a real counterexample, starting from a valid initial state, not from any state satisfying p. Hence, the value of k is now increased and we try to find a real counterexample of length $k+1$ using the BMC constraint Eq. (5).

Compared to BMC, k-Induction has the advantage of including an explicit termination condition. Suppose for example we take for p the predicate $c\ge -2 \wedge c \ne -1$ for Fig. 1. In this case BMC will never terminate, as for every value of k no counterexample can be found. k-Induction, however, can already stop with $k=1$, as $Step( Inv ,1)$ is unsatisfiable. This is an interesting result, given that the state space of the model is infinite. The constraints are shown in Fig. 4 and are unsatisfiable except for $Step( Inv ,0)$. $Step( Inv ,0)$ corresponds to the B proof obligation for the event, checking that p is inductive. Hence, the B proof method is not able to prove that $c\ge -2 \wedge c \ne -1$ always holds. (A user would need to find an inductive invariant such as $c\ge 0$ implying the property. The IC3 algorithm in the next section will do just that automatically.)

Fig. 4.

Steps of k-Induction Algorithm 1 for Fig. 1 with property $c\ge -2 \wedge c \ne -1$

The Base constraint is equal to the one in BMC: Base(p, k) = BMC(p, k). Hence, we can include proof information in the same fashion and simply reuse the optimized constraint Eq. (4) from Sect. 2.1. For the inductive step, we can again use $T^{\lnot }_{p}$ for the last step, to only look for violations of $unproven$ parts of p. Following Algorithm 1, we also know that all intermediate states must satisfy the property p; this we can encode using $T_{p}$, leading to the definition in Eq. (7). As in BMC, we can not remove before-after-predicates from the first steps. Constraints are simplified but the search space is not reduced.

$$\begin{aligned} Step(p,k) = Axm \wedge p(s_{0}) \wedge \bigwedge _{0 \le i < j \le k} s_i \ne s_j \wedge \bigwedge _{i=0}^{k-1} T _{p}(s_i,s_{i+1}) \wedge T ^{\lnot }_{p}(s_k,s_{k+1}) \end{aligned}$$

(7)

2.3 IC3

In contrast to BMC presented in Sect. 2.1 and k-Induction presented in Sect. 2.2 the IC3 algorithm does not use an unwinding ($\bigwedge _{i=0}^{k} T(s_i,s_{i+1})$) of the transition system. Instead, only single step queries are performed.

In order to verify a system, IC3 tries to automatically find an inductive invariant implying the property in question. To do so, it keeps a list of frames $F_i$ over-approximating the set of states reachable in $\le i$ steps. Counterexamples reachable in one or two steps are handled as a special case, as shown in line 2 of Algorithm 2. Afterwards, for each level k IC3 tries to find a property violation in a single step, i. e., a solution to $F_k \wedge T \wedge \lnot p$.

If no solution exists, k is incremented and a new frame holding p is added. Otherwise, IC3 tries to show that the faulty state is in fact not reachable from the initialization. This is done by incrementally strengthening frames until $F_k$ becomes strong enough to prevent the property violation from occurring. A partial outline is shown in procedure strengthen in Algorithm 2. The Counterexample exception is thrown by inductivelyGeneralize if generalization fails and the counterexample can not be proven spurious.

Afterwards, a new counterexample might be found and IC3 will start to iterate between finding counterexamples and strengthening frames. If strengthening the frames eventually fails, a counterexample to the property is found. Otherwise, an inductive invariant has been found.

In the following, we will only go into details of IC3 wherever proof information can be incorporated. For a complete overview, see Bradley’s original paper [9] or the one by Een et al. in [13]. Algorithms 2 and 3 follow the implementation of [9].

The first change to incorporate proof support takes place in the main loop of IC3. When implemented as suggested by Bradley in [9], IC3 features a special case for 0-step and 1-step reachability of a property violation as explained above. This is shown in line 2 of Algorithm 2. The query on line 2 can be changed in the same way we did for BMC and k-Induction. After splitting the transition relation and adding proof information we obtain:

$$\begin{aligned} sat(I(s_{0}) \wedge \lnot p(s_{0})) \vee sat(I(s_{0}) \wedge T_p^{\lnot }(s_{0},s_{1})) \end{aligned}$$

The key point where adding proof assistance improves the performance however is inside the strengthen procedure of IC3. The original version is given in Algorithm 3. Inside, the algorithm tries to find a state included in $F_k$ that has a successor violating the property. With the usual transformation, $F_k(s) \wedge T (s,s') \wedge \lnot p(s')$ is transformed into $F_k(s) \wedge T_p^{\lnot }(s,s')$.

In addition to simplifying the query itself, we can provide the sub routines inductivelyGeneralize and pushGeneralization with the event that lead to the violating state. This enables simplifying the respective predicates considerably.

In IC3, adding proof information has more benefits than just simplifying the occurring constraints. Due to the one-step nature of queries, constraint solving can be skipped altogether if $unproven _{evt,p} = true$. As no paths are built up explicitly, fully proven events have to be considered only during strengthening. They can safely be omitted during the counterexample search. Thus, including proof information leads to a reduction of the search space.

Table 1. Runtimes (in seconds) and speedup (in percent)

3 Empirical Results

The four algorithms described above have been implemented and are available in the nightly builds of ProB ⁵. For the empirical evaluation we want to focus on two questions:

• Does the usage of proof information considerably improve the performance of symbolic model checking algorithms for B and Event-B?

• Can symbolic model checking algorithms compete with explicit state model checking (MC) as done by ProB?

We apply both the algorithms introduced in Sect. 2 as well as ProB’s explicit state model checker (MC) to a selection of models, including artificial and real benchmarks. We use the explicit state model checker with and without proof support as outlined in [4]. The following models were used:

• LargeBranching, a crafted benchmark featuring a counterexample reachable in two steps. However, the initialization has numerous outgoing edges. Discovering the counterexample thus heavily relies on picking the right transitions to follow. The model is included to show that the symbolic algorithms are not influenced by this fact.

• Search, a classical B model of a binary search algorithm. SearchEvents models the same algorithm, but is written in Event-B style with simpler events. While this leads to simpler constraints, it increases the number of conjuncts due to the increased number of events.

• TravelAgency, a classical B model of a travel agency system storing and managing car and room rentals. The model includes an invariant violation.

• Coloring, a model of a graph coloring algorithm by Andriamiarina and Méry. In this particular model, the algorithm works on a concrete graph of 40 nodes.

• f_m0 and f_m1, two hybrid models taken from [2].

• Counters(Wrong), two artificial benchmarks featuring two independent counters, one of them bounded and one counting up infinitely. Both models feature an infinite state space. CountersWrong has a finite counterexample.

• R0_Gear_Door, R1_Valve, R2_Outputs, R3_Sensors and R4_Handle are the first refinement levels of our model [15] for the ABZ 2014 landing gear case study [8].

All benchmarks were run on a MacBook Pro featuring a 2.6 GHz i7 CPU and 8 GB of RAM. We did not run anything in parallel in order to avoid issues due to hyper-threading or scheduling. For each benchmark, a number of different results can occur:

• verified, i.e., the model could be model checked exhaustively without an invariant violation being detected.

• counterexample found, i.e., a state violating the invariant was found in the model and a trace to it has been computed.

• incomplete, i.e., no invariant violation has been found but model checking was not exhaustive. This could be due to timeouts or due to ProB being unable to solve occurring constraints. Currently, we do not try to recover. In case of BMC or k-Induction one could for instance try to increase k anyway.

The results are given in Table 1 showing the runtimes on successful benchmarks as well as the speedup achieved by using proof information.

The state space of the Search model is too large to be traversed by ProB’s explicit state model checker. Unfortunately, the involved substitutions result in complex constraints that cannot be checked by the symbolic algorithms. The effect is increased by the unwinding of the transition system, as complicated constraints start to occur multiple times.

The SearchEvents model features simpler substitutions and is thus more suited for symbolic analysis. Using proof information, all symbolic algorithms are able to find the counterexample. Without proof information, k-Induction is not able to check the model anymore. LargeBranching paints a similar picture.

The TravelAgency model on the other hand has a relatively small state space and can easily be verified using MC. However, it features involved constructs like sequences resulting in complicated constraints. BMC$^*$ is the only symbolic technique to find the counterexample, albeit taking much longer than MC.

The Coloring model is quite big and can not be checked exhaustively by MC in the given time. Only IC3 and k-Induction with proof information are able to do so. For IC3 this is due to its focus on one step reachability in combination with the model being correct: Only a small amount of counterexample candidates are discovered by IC3 and are immediately detected as spurious.

Abrial’s hybrid models can be verified by MC and IC3. Here, constraints become considerably more involved with each unwinding of the transition relation done in BMC and k-Induction. IC3 is again able to verify the model thanks to its local search for counterexamples.

The infinite counters show one of the key limitations of explicit state model checking. Once a state space is infinite, exhaustive analysis is obviously impossible. For the correct model, BMC reaches its iteration limit without detecting an error. Both k-Induction and IC3 are able to analyze the models.

The landing gear model shows that the benefit of using proof information increases with the complexity of the model. As can be seen in Table 1 computation times go down once proof information is used. As for SearchEvents and LargeBranching, for R3_Handle k-Induction can only successfully be used if proof information is considered. For the first refinement steps, IC3 is quicker than explicit state model checking with ProB. However, once the fourth refinement level is reached, none of the symbolic algorithms can handle the occurring constraints anymore.

Regarding speedup, we can report from ${\sim }7\,\%$ (CountersWrong with BMC) up to ${\sim }88\,\%$ (R1_Valve with k-Induction). For most of the models, incorporating proof information leads to a speedup. Using IC3, our approach leads to a performance decline for some models. We suspect it is because adding additional constraints is not necessarily beneficial for a constraint solver.

Summarizing, we can answer the two questions stated at the beginning:

• The inclusion of proof information into the symbolic model checking algorithms does improve the performance most of the time. Furthermore, some models can only be checked if proof information is used.

• For some, albeit small, models symbolic techniques can compete with explicit state model checking. Symbolic model checkers allow to verify infinite state spaces which are beyond the scope of ProB’s classical model checker.

• Among the symbolic techniques, BMC$^*$ was the best for erroneous models, while IC3 was best for correct models.

• However, existing solvers for B and Event-B are still too weak to handle the constraints occurring in larger or more involved models. This currently hinders symbolic model checking efforts.

4 Discussion, Related Work and Conclusion

In [4] the authors presented a similar integration of proof information into explicit state model checking algorithms. As is the case with our implementation, the authors report a speedup by not checking invariants known to be true. In contrast to our approach, the use of proof information never slowed down the model checking process.

Compared with [4], we have added a way to construct proof information within ProB itself, using a bridge to the Atelier B provers and using ProB’s proving capabilities [18]. Of course this takes time and does not always pay off.

In [4], as with BMC and k-Induction, the search space itself is never reduced. Search space reduction through using proof techniques is considered in [28] and [24]. For model checking CTL and LTL properties, proof information can be used as well. In [26] the model checker SMV is coupled with theorem proving techniques. In a similar fashion, [3] combines the Alloy Analyzer with the Athena theorem prover.

Instead of using theorem provers to support model checking, one can use model checkers for theorem proving. We have done so using ProB [18, 22].

Our evaluation shows that using symbolic model checking techniques for B and Event-B models is beneficial: Several counterexamples could only be detected by the symbolic algorithms. Furthermore, some models could be model checked exhaustively. As already outlined in [14], symbolic techniques prove to be a valuable addition to explicit techniques. The techniques are actually also applicable to TLA$^+$, via ProB’s translation from TLA$^+$ to B [16]⁶.

They key weakness of employing symbolic model checking techniques lies within the expressiveness of B and Event-B. Even though constraint solvers and SMT solvers have increased their efficiency by a huge margin, the constraints occurring during symbolic model checking of high-level languages like B are still too involved. Among other abstraction techniques, integrating static (proof) information into the constraints is one way to help. It brings down computation times and sometimes enables successful validation. We are also working on strengthening the underlying constraint solver, by integrating SMT solvers such as Z3 [19]. Still, more improvements need to be achieved until full symbolic verification of B and Event-B models becomes viable.

Regarding the different model checking algorithms, especially IC3 seems promising. In contrast to the other two algorithms, its focus on one step reachability keeps occurring constraints easier. This makes it more suited for symbolic model checking of high-level languages like B and Event-B. Additionally, the integration of proof information can lead to a reduced search space. As IC3 has originally been developed for hardware model checking, it is not trivial to lift it to the software world. To do so, we would like to investigate IC3 for B together with abstraction techniques as introduced in [11] or [7].

Another direction of future work could be to generate missing proof obligations from the model checking run. Analyzing predicates that lead to a timeout one could find problematic properties and try to prove them externally or in an independent run. Once the constraint solver gets stuck we could ask an external solver⁷ to proof or disprove further invariants. Afterwords, one could extend the set of properties under consideration.

In summary, we have implemented four symbolic model checking algorithms for B and Event-B and have shown how to integrate proof information to improve the algorithms’ performance. Our evaluation shows that bounded model checking can effectively find counterexamples in models with very large branching factors and that IC3 is capable of automatically proving models with infinite state spaces correct. Further research is, however, needed to scale up the symbolic techniques to models with more involved events.