SOURCE ARCHIVE
EXTRACTED CONTENT
74,192 charsEfficient State Space Exploration: Interleaving Stateless and State-based Model Checking
Malay K. Ganai Chao Wang Weihong Li
NEC Laboratories America NEC Laboratories America NEC Laboratories America
Abstract—State-based model checking methods comprise computing are interleaved seamlessly in order to systematically search the state and storing reachable states, while stateless model checking methods space of the model, at the same time avoiding the storage of the directly reason about reachable paths using decision procedures, thereby entire (explored) reachable state set. More specifically, at any point avoiding computing and storing the reachable states. Typically, state- based methods involve memory-intensive operations, while stateless of time, the hybrid procedure stores only a set of frontier states, as methods involve time-intensive operations. We propose a divide-and- illustrated in Fig. 1 (b), which are the states reachable from the initial conquer strategy to combine the complementary strengths of these states in a fixed number of execution steps. methods for efficient verification of embedded software. Specifically, We focus on verifying reachability properties of sequential pro- our model checking engine uses both state decomposition and state grams under the assumptions of finite recursion and finite data. prioritization to guide the combination of a Presburger arithmetic based symbolic traversal algorithm (state-based) and an SMT based Both user-defined assertions and common programming errors (array bounded model checking algorithm (stateless). These two underlying bounds violations, null pointer de-referencing, uninitialized variables, algorithms are interleaved—based on memory/time bounds and dynamic etc.) can be formulated into the reachability of some error blocks. task partitioning—in order to systematically explore the state space and Our HMC procedure is designed specifically to target bugs that are to avoid storing the entire reachable state set. We have implemented our new method in a tightly integrated verification tool called HMC (Hybrid hard-to-find by either state-based or stateless methods in isolation. Model Checker). We demonstrate the efficacy of the proposed method The search engine of HMC implements a state traversal algo- on some industry examples. rithm [12], [13] based on a Presburger arithmetic solver [10], and a I. INTRODUCTION SMT-based bounded model checking algorithm [14], [15]. The finite- state model is represented as combination of a set of linear integer Model checking [1]–[4] plays an important role today in the constraints whenever possible, as opposed to the more conventional, automated verification of hardware [5] and safety-critical embedded bit-blasted, pure Boolean logic. Our choice of using higher level software [6]–[9]. In this paper, we focus on model checking tech- reasoning rather than pure Boolean logic is because, as shown in niques that are based on symbolic reasoning. Based on whether they [12]–[15], for example, it tends to scale much better when applied to compute and store the reachable states, symbolic model checking models of embedded software. Since state-based methods typically techniques can be classified as either state-based or stateless. involve memory-intensive operations, regardless of the logic levels to State-based model checking methods, e.g. those based on Boolean which they are applied, whereas stateless methods typically involve level reasoning using BDDs [2] and integer level reasoning using time-intensive operations, we have designed a heuristic algorithm Presburger arithmetic solvers [11]–[13], comprise computing and to automatically interleave the state traversal and the path-based storing sets of states. Given the transition relation of the model and reasoning. To improve the overall robustness, we use a memory bound a set of states, they use image computations to repeatedly obtain a to switch from ST to PR and use a depth/time bound to switch from set of states reachable in either the forward (image) or the backward PR back to ST; we repeatedly switch between these two modes to (pre-image) directions. This process is often referred to as unbounded avoid blowup within a particular method. model checking due to its capability of exploring the entire state space We use both state partitioning and state prioritization to guide the without a predetermined bound on the execution depth. State-based interleaving of state traversal and path-based reasoning in our hybrid methods generally perform well when the state sets have compact search. Large frontier state sets are partitioned dynamically based on representations, but can suffer from memory explosion otherwise. heuristics with respect to their size, in terms of the number of linear Stateless model checking methods, e.g. SAT based bounded model equations (for Presburger arithmetic) and BDD nodes. The partitioned checking (BMC) [3], [4] and high-level bounded model check- state sets are ranked to decide their processing order, and the ranking ing [14], [15] based on Satisfiability Modulo Theory (SMT) solvers functions are designed to favor those with a higher likelihood of (e.g. [16], [17]) directly reason about the execution paths of the reaching the error states. model, thereby avoiding the explicit manipulation of state sets. Typ- The divide-and-conquer style of our HMC procedure introduces ically memory explosion is less severe; however, stateless methods data parallelism, which can be exploited by parallelization for many- often involve time-intensive computations. They generally perform core CPUs. Below are some highlights of HMC: well when the execution paths required to decide the validity of the • It employs a divide-and-conquer procedure to compute the properties are short, but can perform poorly when paths are long. frontier states and to represent them efficiently. In this paper, we propose a unified model checking framework for • Although it has avoided storing the entire reachable state set, for verifying embedded software called HMC (Hybrid Model Checking), terminating programs, it still guarantees exhaustive coverage. which combines the often complementary strengths of the state- • It employs abstract interpretation to over-approximate the set of based [12], [13] and stateless [14], [15] methods. The goal is to states backward-reachable from error states in k steps, allowing provide a robust verification solution for industrial-strength embedded the search to target states likely to lead to errors quicker. software applications. In our unified framework, as illustrated in • It employs control-state reachability to build simplified transition Fig. 1 (a), the state traversal (ST) and the path-based reasoning (PR) relations on-the-fly, to guide both ST and PR.
PR: Find CEX to Error blocks |
Switch E from states σ Explored states Un-explored PR↔ST BMC (σ,E) (not stored) states
State Error Partitioning ST: Compute Image, Partition, states
Store frontier states F
State D= Img(σ) Initial
Prioritization F = (F\ σ) ∪ Partition(D) states Frontier States (stored)
Heuristics H M C: Hybrid Model Checking
(a) (b)
Fig. 1. (a) Overview of the HMC procedure; and (b) the set of frontier states
.
The remainder of this paper is organized as follows. After es- C and X, respectively. Furthermore, let X = Xᴮ ∪ Xᴵ , where Xᴮ tablishing notation in Section II and review the basics of symbolic and Xᴵ are the subsets of Boolean variables and integer variables computation in Section III, we present our main contributions in in X, respectively. We use Boolean and Linear integer arithmetic Sections IV-VI. This is followed by the experimental results in expressions to represent the update and guarded transition relations Section VII, and the review of related work in Section VIII. We of Xᴮ and Xᴵ , respectively. give our conclusions in Section IX. A transition from 〈ci, di〉 to 〈cj, dj〉 under enabling predicate gij g/u II. PRELIMINARIES and update relation ui with n assignments is denoted 〈ci, di〉 −→ We briefly discuss the essential model building steps under the 〈cj, dj〉. Let Tij be its transition relation. The transition relation of typical assumptions of bounded heap/stack for embedded software. the entire model M, denoted T (C, X, C′, X′), is the union of all Consider the C program in Fig. 2(a), which has a while loop these individual transitions. ∨ = (C︸ = ci ∧ C′ = cj ∧ gij ∧ u (1) and some embedded assertions. Fig. 2(b) shows the corresponding T def control and data flow graph. The boxes associated with control Γ(ci,cj)=true ︷︷ ︸ⁱ) states (i.e. basic blocks) show their unique id’s. An edge between Tij blocks corresponds to the control flow between associated program Let xₖ := ei,k be an assignment to variable xₖ in control state ci. points. Each edge is associated with an enabling predicate. Updates of ~ Let x′ₖ be the next-state variable of xₖ. The update relation ui is program variables (i.e. assignments) are shown at each control state. defined as follows: Embedded assertions and common programming errors, such as array k∨ =n bounds violation, null pointer dereferencing, and failed assertion, can ui def = (C = ci) ∧ (x′ₖ = ei,k) (2) be modeled as the reachability of some error blocks. In this figure, k=1 for example, blocks 12 and 14 correspond to the assertions P 1 (line We assume x′ = x x 18) and P 2 (line 19), respectively. k k if variable k is not explicitly updated. The control flow graph (CFG), denoted G = (V, E, r), can be A. Modeling C Programs as EFSMs viewed as the control-state abstraction of the EFSM. The set V of An Extended Finite State Machine (EFSM) is a 3-tuple M = nodes corresponds to the set of control states in the EFSM. E is (C, X , T ), where C is a set of control states, X is an n-dimensional the set of control flow edges. r ∈ V is the entry block. The CFG space of valuations of the datapath variables, and T is a set of transi- can be obtained from an EFSM by ignoring all enabling predicates tions. Each transition is a 4-tuple (c i, di, cj, dj), where ci, cj ∈ C are and updated transitions. More formally, we assume that V = C, control states, and di, dj ∈ X are valuations of datapath variables. E = {(c, c′) | Γ(c, c′) = true}, and r is the unique entry block We use C to denote the program counter variable which takes values with no incoming transition. from the set C. We use X = {x₁, · · · , xₙ} to denote the set of B. Symbolic Expressions and Solvers datapath variables, which take values from the set X . A state of M is an ordered pair 〈ci, di〉 ∈ C ×X . Let gij : X 7 →B = {0, 1} be the We represent both the transition relations and the state sets sym- guarded transition predicate associated with the transition from ci to bolically as logic formulas, with Boolean level expressions as well cj. Let ui : X × I → X be the update transition relation associated as integer expressions in Presburger arithmetic. Presburger arithmetic with the assignments in ci. Let Γ : C × C 7 → {0, 1} be the Boolean is a decidable fragment of quantifier-free first-order logic. predicate such that, for ci, cj ∈ C, Γ(ci, cj) = true iff gij is defined. Solving Decision Problems using SMT: A Satisfiability Modulo We construct a symbolic transition relation for the EFSM to capture Theory (SMT) problem for a theory T , denoted SM T (T ), comprises the set of all guarded transitions between basic blocks. For each a formula with arbitrary Boolean combination of a set of elementary data variable, we add an update transition relation based on the constraints, each of which is expressed in the theory T . For example, expressions assigned to the variable in various basic blocks. Recall if T is the theory of linear integer arithmetic (LIA), then each that C is the program counter variable and X is the set of datapath elementary constraint is of the form (a₁x₁ + . . . aₙxₙ ≤ c), where variables. We shall use C′ and X′ to denote the next-state copies of a , . . . , aₙ and c are integer constants, and x₁, . . . , xₙ are integer 1
1. void foo(void) { i=x=0 Control Reachable Set R, Replace transition
2. i=x=0; blocks: 1 State -disjunct Dr@d, r∈∈∈R(d) | _ by Dr@4, r∈∈∈∈R(4) J
3. while(1){ Error
4. if (i==x) { P1, P2 2 k=0 1 D1@0 R(0) = {1} | T0,1
5. x = i+3; 22
6. if (i==0) { 4 D @1 T1,2 D9@4
7. y = ND(); 3 k=1 2 2 R(1) = {2} ∨∨∨∨
8. assume (y ≤ 0);
9. }else y++; [ i==0 ] x=i+3 on x++ k=2 3 D3@2 4 D4@2 || T2,3 D10@4 |
10. }else { 5 y=? 6 y++ y=? 7 y++ z R(2) = {3,4} |
11. if (i==0) { 8
12. y = ND(); k=3 5 6 7 8 R(3) = {5,6,7,8} T3,4 i
13. assume(y < 0); 16 10 k=4 9 10 R(4) = {9,10} T4,5
14. } else y--; 9 | D9@4 D10@4
15. } Sink [ x==15 11 =
16. if (x==15 && i>35) && i>35] lng k=5 11 R(5) = {11} T5,6 T5,6
17. break; 13 R(6) = {12,13,14,16} T6,7
18. assert(y>5); /*P1*/ Err: P1 NOP Err: P2 k=6 16 12 14 T6,7
19. assert(y<-5); /*P2*/
20. i++; 12 13 14 =
21. } k=7 15 R(7) = {15} T7,8 T7,8
22.} 15 i++ k=8 1 R(8) = {1} T8,9 T8,9
(a) (b) (c) (d)
Fig. 2. (a) An example C program, (b) its EFSM M, (c) the CSR for depth 8, and (d) the replacing transition T 0,5 by a reachable set.
variables. Given an SMT formula φ, the decision problem is to III. SYMBOLIC COMPUTATIONS
determine whether φ is T -satisfiable, i.e., there exists a valuation A. Path-based Reasoning of the Boolean and integer variables in φ such that φ evaluates to Let s true. In this work, we use an off-the-shelf SMT solver [16] to decide sequenceⁱ π≡0,k〈C, X 〉 denote a symbolic state. A path is a finite the formulas in SMT modulo linear integer arithmetic (LIA). = (s₀, . . . , sₖ) satisfying the following predicate: ∧ = T (si, si+1) (3) Simplifying Presburger formulas: We use a Disjunctive Normal T 0,k def Form (DNF) representation for the formulas representing state sets, i.e., formula Ω expressed as Ω = ∨ⁿi=1Ω Ωᴮi ∧ Ωᴵi , where Ωᴮi is a 0≤i<k = true. In Boolean formula, Ωᴵ where T is the transition relation as in Eq. (1). Let T 0,0 def and nΩ i is an integer formula in Presburger arithmetic, bounded model checking, whether an LTL property φ can be falsified is the number of disjunctions, respectively. Let vᴵ be the in k execution steps from some initial state ψ is formulated as a set of integer variables and vᴮ be the sets of Boolean variables. We assume that the formulas, i.e. Ωᴵi and Ωᴮi , are always type-consistent; satisfiability problem [3]: that is, vᴮ ∩ vᴵ = ∅. ∨ BM Cᵏ(ψ, φ) def Consider two DNF formulas Ω and f = nf (f B ∧ f I ). = ψ(s₀) ∧ T 0,k ∧ ¬φ(sₖ) (4) i=1∩), negationi i where φ(sₖ) means that φ holds in state sₖ, and ψ(s₀) means ψ Common set operations such as union (∪), conjunction ( (¬), and existential quantification (∃v.) can be defined over DNF holds in state s₀. Given a predetermined bound n, BMC iteratively formulas [11], [12]. The union of two DNF formulas is simply the checks the satisfiability of BM Cᵏ for 0 ≤ k ≤ n using a SAT or union of their subformulas. The conjunction is the union of the pair- SMT solver. We define BM Ck,k⁺ᵈ between depths k and k + d as wise conjunctions of their subformulas. BM Ck,k⁺ᵈ(ψ, φ) def = ψ(sₖ) ∧ T k,k⁺ᵈ ∧ ¬φ(sₖ+d) (5) nΩ∨ ,nf Ω ∧ f = (Ωᴮj ∧ fiᴮ) ∧ (Ωᴵj ∧ fiᴵ ) For each variable v ∈ X, let vᵏ be the copy of v at the BMC i=1,j=1 unrolling depth k. When considering the reachability of error block Since there is no common variable, subformulas from different Err from a source block Src, we define ψ := (C = Src) and domains do not interfere with each other. The negation of a DNF ¬φ := F(C = Err), where F is the LTL operator eventually. formula is implemented in a similar way. Since there is no common B. State Traversal variable, existential quantification distributes not only over unions (as Given the entry block c₀ ∈ C and initial values for datapath in general) but also over subformulas in different domains: variables (x₁ = e0,1; · · · xₙ = e0,n), the initial state formula I is ∨ⁿΩ = (C = c₀) ∧ ∧ⁿ (xₖ = e0,k) (6) ∃vᴮ, vᴵ . Ω = (∃vᴮ . Ωᴮi ) ∧ (∃vᴵ . Ωᴵi ) I def i=1 k=1 The DNF representation is not a canonical form, and there exist Similarly, given a subset ρ ⊆ C of control states, the set Dρ(C, X ) heuristic algorithms [11], [12] to compact the result. Although the of concrete states in ρ is defined as follows: resulting DNF can be (nΩ × nf ) for conjunction (and 2ⁿΩ for Dρ def ∨ negation), such worst-case results rarely happen in practice. In = (C = c) ∧ fcᴮ ∧ fcᴵ (7) our implementation, we use CUDD [18] to represent and simplify c∈ρ Boolean formulas, and the Omega library [10] to represent and where fcᴮ and fcᴵ denote the subformulas over datapath variables simplify Presburger arithmetic formulas. in Boolean logic and Presburger arithmetic, respectively. We refer
to a state set like Dρ as a state-disjunct. Given a transition rela- the error states BErr (in the error block Err) iff some error states tion T (C, X, C′, X′) and a state-disjunct Dρ(C, X ), symbolic state in BErr are reachable from F in k steps; that is, there exists D ∈ F traversal typically comprises a series of image computations [12] such that BErr ∩ Imgᵏ(D) = ∅, with Img⁰(D) def = D. till a fixpoint is reached. Let f(X/X′) denote the substitution of X′ variables in function f by the corresponding X. The image operation Lemma 1: If F is a frontier set with respect to BErr and BErr ∩ Img, which computes the set of states reachable from Dρ in one D = ∅, then F := F {D} ∪ {Img(D)} is also a frontier set. execution step, is defined as: Essentially, F maintains a set of state-disjuncts that divides the Img(Dρ) def reachable state space into explored and unexplored as in Fig. 1 (b). = (∃C,X T ∧ Dρ)(X/X′,C/C′) (8) In HMC, we pick the next to-be-explored state-disjunct Dρ ∈ F Similarly, the pre-image operation P re is defined as: using a state prioritization heuristic (Section V-B). The set Dρ is then encoded as a SMT(LIA) formula sc, to be used as reachable state P re(Dρ) def = (∃C′,X′ T ∧ (Dρ)(X′/X,C′/C)) (9) constraints in BM Ck,k⁺ᵈ(ψ, φ). Based on the disjunctive partition We use Imgᵏ(Dρ) and P reᵏ(Dρ) to denote the result of k suc- of F , we can solve a series of independent satisfiability problems cessive Img and P re operations from D ρ, respectively. We use given by = BM Ck,k⁺ᵈ(ψ, φ) ∧ (ψ = sc) (12) P re⁺(Dρ) to denote the result of an over-approximated pre-image ω def operator [19], which is a superset of states backward-reachable from Dρ in one step. where each sc is the constraint for a small subset of the frontier F computed symbolically. More specifically, we employ the following C. Control State Reachability strategies in HMC to avoid the memory blowup: A control path γ0,k = (c₀, . . . , cₖ) is a sequence of control states • We store only the frontier sets, not the entire set of reached satisfying the following predicate: states. Γ0,k def ∧ • When the size of a state-disjunct ∈ F exceeds a threshold, we = Γ(ci, ci+1) (10) partition it further (Section V-A) to make its image computation 0≤i<k less memory-intensive. Recall that Γ(ci, cj) = true iff the guarded transition gij is defined • For computing Img(Dρ), we build a simplified transition rela- for ci and cj. Let Γ0,0 = true. A control state reachability (CSR) tion T |D 1 on the fly and release its memory immediately after analysis is a breadth-first traversal of the CFG where control state b ρ the computation (ref. Section V). is one step reachable from a iff Γ(a, b) = true, i.e, We switch between computing reachable states and solving the = {b|a ∈ c,˜ Γ(a, b) = true} (11) satisfiability problem based on some predetermined memory/time CSR(˜c) def bounds. We use CSRᵈ(˜c) to denote the result of d successive CSR op- erations from a set c˜ of control states. At an execution depth d, B. Completeness Discussion let R(d) be the set of control states reachable from R(d − 1) in In HMC we do not accumulate the entire set of reachable states, one step in the CFG by ignoring the guards. Let R(0) = c₀, then R(d) = CSRᵈ(R(0)). Consider computing CSR for the CFG in therefore avoiding the main memory bottleneck in symbolic state Fig. 2 (b). The resulting set R(d) is shown in Fig. 2 (c). We will use traversal. This also means, in general, that we cannot guarantee control state reachability to simplify the formulas in both state-based to detect the reachable fixpoint. Fortunately, if the programs under and stateless computations. verification are terminating programs, state traversal with frontier sets is guaranteed to terminate after L steps, where L is the longest IV. HMC: THE OVERVIEW program path [12]. We illustrate the basic ideas behind the hybrid model checking in For path-based reasoning, we can also obtain a completeness this section, and provide formal exposition in Sections V- VI. criteria [3], [4] from the BMC completeness threshold CT . For A. Basic Strategy example, for a state set ψ, we know that the threshold CT is reached if the formula below becomes unsatisfiable: Consider the example in Fig. 2 (a-b). We first obtain an unrolled = BM Ck,k⁺ᵈ(ψ, φ) ∧ ∧ (si = sj) (13) CFG by unwinding the CFG up to depth k = 8 as shown in LF P k,k+d def Fig. 2 (c). Each program (concrete) path in the depth-k BMC instance k≤i<j≤k+d corresponds to a control (abstract) path in this unrolled CFG. As the In our HMC implementation, we also use the more recent improve- unrolling depth increases, the number of control paths will increase ment in [15], which requires solving a formula of only size O(d) quickly, thereby making each successive BMC instance harder to as opposed to the conventional O(d²). The key is to note that for solve. As shown in Fig. 2 (c), the number of control paths from a terminating problem, the SINK control state (exit block) does not block 1 at k = 0 to block 12 at k = 6 is 4, but is only 1 from have outgoing transitions. block 11 at k = 5. Clearly, if we can replace the unrolled transitions kT 0,4 in the dotted rectangle by the set of concrete reachable states at N T P k,k+d def= (BM Ck,k⁺ᵈ(ψ, φ) ∧ (φ = BSINK )) (14) = 4, we can reduce the size of the BMC instances for k > 4, thus making BMC search faster and deeper. Let Dc@k be a state-disjunct Lemma 2: For terminating programs, N T P k,k⁺ᵈ is satisfiable if in control state c at depth k from the initial states. We replace T 0,4 by D₉@4 ∨ D₁₀@4. and only if LF P k,k⁺ᵈ⁺¹ is satisfiable. Definition 1 (Frontier Set): Let F be a set of state-disjuncts 1 reachable from the initial states. F is a frontier set with respect to thatForf|gf=andf ifg, we define a constraint (or simplify) operator, denotedg f|g, so = 1; otherwise, f|g = don′t care. Thus, f|g ∧g = f ∧g.
V. STATE DECOMPOSITION AND PRIORITIZATION Given Dρ, we define a no-need-to-partition predicate N P (Dρ):
We use the cheap control state reachability analysis to simplify N P (Dρ) def
the subsequent precise image computations in state traversal. Given = (size(Dρ) < tsize) ∧ (size(T Dρ)) < isize) (18)
the transition relation T and a state-disjunct Dρ(C, X) with the The partitioning problem is stated as follows. Given the threshold
corresponding control states ρ ⊆ C, conceptually we can obtain T |Dρ sizes tsize and isize and a state-disjunct Dρ, divide Dρ into a set by projecting T to Dρ, {D1,ρ₁ , · · · Dm,ρₘ } such that, for 1 ≤ i = j ≤ m, ρi ⊆ ρ, T ∧ Dρ = T |Dρ ∧ Dρ = (∨︸ ci∈ρ,cj∈︷︷ ) i Partition and Group, which are geared toward CSR(ρ)Tij︸ ∧Dρ (15) N P (Di,ρ ) is true, and m is minimum. We use two low-overhead greedy procedures, Tρ,CSR(ρ) minimizing the number of partitions and at the same time obtaining The number of disjuncts in Tρ,CSR(ρ) is bounded by the number of a good balance among the partition sizes. distinct control edges. Typically the number of outgoing edges from Partition: Given Dρ s.t N P (Dρ) = f alse. a basic block is either 1 or 2 (for if-else); therefore the number of • Initialize H = {D1,ρ , · · · , D disjuncts is between |ρ| and 2|ρ|. In contrast, the number of disjuncts • For each D 1 n,ρn }, s.t. ρi = {ci}, ci ∈ ρ. i in T , as in equation (1), is bounded by total number of control edges greedily s.t.i,ρDⁱ ∈ H, if N P (Di,ρDi) = f alse, bi-partition Di,ρ i,ρ = D . Update H, i.e., H := in the CFG. Thus, instead of building T , we build Tρ,CSR(ρ) on i,ρi } ∪ {Da,ρi i, D a,ρi ∧ b,ρi the fly for each given Dρ using the CSR information. Since the H{D b,ρ i }. symbolic representation of Tρ,CSR(ρ) is often smaller than that of • Repeat till all partitions in H satisfies predicate N P . T , the peak memory requirement during the state traversal can be Group: Given a set J = {D1,ρ₁ , · · · , Dm,ρₘ } s.t. ρi ∈ R(k). reduced significantly. Further, since CSR is an over-approximated • Merge two smallest state-disjuncts in J, i.e. D12,ρ₁ ∪ρ = analysis, the precise image Img(Dρ), where Dρ is a subset of the D 2 2{D1,ρ, D2,ρ}∪{D12,ρ } and repeat the previous set ρ of control states, is always a subset of CSR(ρ) as stated in the • 1,ρ1 ∨ D2,ρ . (Implemented using priority-queues.) Update J = J 1 following: step if N P (D ) = ; otherwise stop. 12,ρ1 ∪ρ2 true Lemma 3: Let Dρ′ ′ = Img(Dρ). If ρ ∈ R(k), then ρ′ ⊆ B. State Prioritization CSR(ρ) ⊆ R(k + 1). We propose two heuristics, one is goal-directed and another is Lemma 4: If Dρ ⊆ Imgᵏ(I), then ρ ⊆ R(k). driven by the search depth, to prioritize the processing of state- A. State Decomposition disjuncts in the frontier set F . Following the terminology of [21], we Our DNF representations in general are not canonical. In particular, use lighthouses to refer the intermediate states serving as guidance the polyhedrons used to represent linear integer constraints may of the search for error states. become fragmented after being propagated through branching and Goal-directed lighthouses (glh). These lighthouses are derived re-converging points of the CFG during image computation. This based on the observation that a state is more likely to reach an error often lead to memory blow up when verifying large programs. We block if the block is only few execution steps away. We compute the mitigate this problem by dynamically decomposing the frontier sets. over-approximated execution steps using the P re⁺ operator (below). The goal is to avoid computing images/pre-images for large Let BRᵏ be a set of abstract (backward) states obtained by applying state representations. Given a state-disjunct ∨ Dρ and its disjunction D ∈ F is given an abstract distance k iff D∩BRᵏ = ∅ and ∀0≤i<k, {D1,ρ , · · · Di,ρₘ } s.t. Dρ = mi (Di,ρ ), ρ = ⋃ᵐ ρ , we divide P re⁺ operator k times from the error block. Then each state-disjunct the image computation into multiple steps to avoid memory blowups, over D₂ ∈ F if the abstract distance of D₁ is less than that of D₂. Lemma¹ 5: Img(Dρ) = ∨ᵐ Img(Dⁱ i i D ∩ BRⁱ = ∅. Our glh strategy is to give D₁ ∈ F a higher priority i=1 i,ρi) P re⁺ operator: From a given state disjunct D, we first compute its In general computing a good state partition is hard due to often pre-image using equation (9), then obtain an over-approximation by conflicting requirements. Larger partitions can make each subproblem computing the convex union of the disjuncts, i.e., (P re(D))⁺. Let K more difficult to solve but can reduce the partitioning overhead. be a predetermined threshold for the maximal number of polyhedra Whereas smaller partitions can result in easier image computation allowed in each state-disjunct. If the actual number of polyhedra subproblems but can significantly increase the partitioning overhead. in P re(D) exceeds K, we replace the Polyhedra-part of the state- Here we use low-overhead partitioning heuristics based on the CSR disjunct with at most K number of polyhedra, the later of which is information. We note that the size of Img(Dρ) often depends on computed by heuristically merging the polyhedra as in [12], [13]. the sizes of both T and Dρ. We want to partition Dρ but want to minimize the need for partitioning Img(Dρ). We propose a simple Example: Let K = 1, and the state disjunct D be mechanism to estimate the size of a state-disjunct and its image. Given Dρ = ∨ci∈ρ(C = ci) ∧ fiᴮ ∧ fiᴵ , we define size(Dρ) as D = (C = 0) ∧ (x = 0) ∧ (y = 0) ∨ (C = 1)∧ ( (x ≥ 1) ∧ (x ≤ 5) ∧ (y ≥ 2) ∨ (x ≥ 10) ∧ (y ≥ 1) )
size(Dρ) def
= Σci∈ρ(#P (fiᴵ ) + #B(fiᴮ)) (16) where the expressions C = 0 and C = 1 are in Boolean logic and
are represented as BDDs. The over-approximated set D⁺ is
where #P is the number of polyhedra in fiᴵ , and #B is the number
of BDD nodes in fiᴮ. We estimate the size of Img(Dρ) before (C = 0) ∧ (x = 0) ∧ (y = 0) ∨ (C = 1) ∧ (x ≥ 1) ∧ (y ≥ 1)
actually computing it. The size, denoted size(T Dρ), is defined based
on the size of Tρ,CSR(ρ) ∧ Dρ: Targeting deeper states (dfs): To target deep error blocks, we give
priority to the state-disjuncts at a deeper execution depth. Let Dc˜ ∈
k
size(T Dρ) def
= Σ F be the set reachable from the initial states in the k execution
#B(fiᴮ ∧ uᴮi ) ∗ (Σcj∈CSR(ρ)#B(gᴮ)) (17) Dc˜ₖ ∈ F over priority over Dc˜j ∈ F , iff k > j.
+ Σci∈ρᶜⁱ∈ρ#P (fⁱᴵ ∧ uᴵⁱ ) ∗ (Σᶜʲ∈CSR(ρ)#P (gⁱʲᴵ )) steps. In the dfs strategy, we give a higher priority to state-disjunct
ij
C. BMC Simplification Algorithm 1 HMC
We also use CSR information to simplify the BMC instances. The 1: input: CFG: G, Initial States: I, Transition: T , Error Block: Err
set of control paths of length d from c ∈ c˜ₖ(⊆ R(k)) is 2: output: F AIL/P ASS
3:
γ˜c˜ₖ,d = {(cₖ · · · ci · · · cₖ+d) | ∀ₖ≤i≤k+d ci ∈ CSRⁱ(˜cₖ)} (19) 4: F = I
We constrain BM Ck,k⁺ᵈ using γ˜c˜ₖ,d; that is, BM Ck,k⁺ᵈ|γ˜ , to 5: //Switch between PR and ST
remove the statically unreachable control paths: c˜k ,d 6: while true do
7: PR(G, F, T, Err)
BM Ck,k⁺ᵈ|γ˜ (ψ, φ) def k,k+d 8: ST(G, F, T, Err)
c˜k ,d = T |U BC(˜γc˜k ,d) ∧ ψ ∧ ¬φ(sₖ+d) 9: end while
(20)
where U BC, or Unreachable Block Constraint, uses unreachable 1: Procedure PR (G, F, T, Err) //Perform CSR, BMC
control states to simplify T k,k⁺ᵈ using on-the-fly size reduction 2: //Stop if time bound is reached
techniques such as hashing and constant folding [14]. Note that B 3: //Pick a state-disjunct with highest priority
is a control-state predicate, i.e., Bᵣ ≡ (C = r). r 4: for all Dc˜ ∈ F, c˜ R(k) do
k k ∈
∧ 5: Compute CSR (CF G, c˜k, d) //depth bound is d
= ¬Bᵣᵏ⁺ⁱ (21) 6: for k ≤ i ≤ k + d do
U BC(˜γc˜ₖ,d) def
c˜
0≤i<d,r∈CSRi(˜ck) 7: BM Ck,kγ˜ +i := BM Ck,k+i|
8: = Enc
sc k ,i2LIA(Dc˜k ) γ˜c˜k ,i //Section V-C
//Encode into SMT
Lemma 6: BM Ck,k⁺ᵈ|γ˜ ⇐⇒ BM Ck,k⁺ᵈ 10: if SIN K ∈ R(k) then
R(k),d SAT . 9: //Completeness: is block other than SINK reachable?
VI. HMC: THE PROCEDURE 11: is sat = SAT (BM Cγk,k˜ +i(sc, B ))
c˜
k ,i SINK
The pseudo code of our HMC procedure is shown in Algorithm 12: if (is sat = f alse) then
1. Given an error block Err and the initial states I, the procedure 13: F := F \Dc˜ₖ //Remove dead-end states
interleaves subprocedures PR and ST till Err is proved to be either 14: end if
reachable or unreachable from I. The frontier set F of state-disjuncts 15: end if
is stored in a priority queue (Section V-B). F is initialized to I. 16: if Err ∈ R(k) then
17: is sat = SAT (BM Cγk,k˜ +i(sc, ¬B ))
c˜
18: if (is sat = true) then
Subprocedure PR. It always chooses the state Dc˜ ∈ F with the k ,i Err
k CSRⁱ(˜cₖ) for 19: return F AIL //Err is reachable
highest priority. For k ≤ i ≤ k + d, it first computes
a fixed depth d. It then obtains the BM Ck,i instance as follows: (a) 20: end if
for each i, build a simplified transition relation T k,k⁺ⁱ (Section V-C), 21: end if
and (b) translate Dc˜ into a state constraint sc at depth k. For 22: end for k 23: end for each BM Ck,i instance, it performs following two checks. When the depth/time bound is reached, we switch from PR to ST. 1: Procedure ST (G, F, T, Err) //Compute new frontier set Completeness Check: If SIN K ∈ CSRⁱ(˜cₖ) and if only SINK state 2: (i.e. no non-SINK state) is reachable from Dc˜ , then we can remove 3: while true do k 4: if F = ∅ then state-disjunct D from as it will never lead to any new state. c˜k F 5: return P ASS //Err is unreachable Error Check: If Err ∈ CSRⁱ(˜cₖ) and if Err is reachable from Dc˜ , 6: end if k 7: P rioritize(F ) then HMC terminates with a return value F AIL as the Err block is 8: if Σd∈F size(d) > fsize then reached. Subprocedure ST. If F = ∅, HMC terminates with a return value 9: fsize := 2 ∗ fsize 10: break //Switch to PR P ASS since the fixpoint is reached. Otherwise, a switching condition 11: end if from ST to PR is checked as follows: if the sum of the sizes of all 12: if Err ∈ ρ then state-disjuncts in F is above a predetermined memory bound fsize, 13: return F AIL //Err is reachable then fsize is scaled up by factor 2, and simultaneously a switch is 14: end if made to BMC. Such a switching heuristic allows us to have a finer 15: //Pick a state-disjunct with highest priority ρ control over the overall memory usage. 16: Tρ,CSR(ρ) = T |D 17: img = Img(Dρ) If no switching is needed, it computes a new frontier set as 18: //Move the frontier forward follows: (1) Pick Dc˜ ∈ F with the highest priority. If Err ∈ c˜ₖ, HMC terminates with kF AIL; otherwise, obtain a simplified transition 19: F := F \Dρ 20: F := F ∪ Partition(img) //Section V-A relation Tρ,CSR(ρ) (Section V). (2) Compute img := Img(Dc˜ ), 21: F := Group(F ) //Section V-A k 22: end while and if required, partition img further (Section V-A). (3) Remove Dc˜ from F and then add img or its partitions. If required, also merge small state-disjuncts in process is repeated.ᵏ F together (Section V-A). The entire Lemma 9: ∨Dρ∈ BM Ck,k⁺ᵈ(ψ, φ) ∧ (ψ = Dρ) ⇐⇒ A. Correctness of HMC BM Cᵏ(I, φ) F SAT If Lemma 7: States in F are reachable from the initial state I, i.e., Theorem 1: The procedure HMC will terminate eventually with Dρ ∈ F , then Dρ ∈ Imgᵏ(I) and ρ ⊆ R(k) for some k ≥ 0. a decision F AIL if the error block is reachable. Further, for a Lemma 8: F is indeed a frontier set (definition 1), i.e., if Err is terminating programs, HMC will terminate eventually with a decision reachable from I, then it is reachable from some states in F . P ASS if the error block is unreachable.
Proof of termination: From Lemma 8, we have the set F as a computations. The memory usage for BMC is often small. (Witnesses frontier set. After every image computation, the frontier set moves in HMC may be longer since it is not a breadth-first traversal.) closer to the Err block. If the Err block is reachable, the procedure In Table II, we provide statistics for HMC with both dfs and glh. will eventually find it reachable from some state-disjunct in F , and Columns 2–5, and 6–9 present the peak number of switches i.e., it will terminate. If the Err block is unreachable, the frontier set PR→ST→PR (#S), the number of image computations (#I), the size F will eventually become ∅ for a terminating program model, and of frontier set (#F), and the number of calls to Partition (#P), therefore, the procedure will also terminate. respectively. For examples such as s10, s11, s12, where glh is Proof of correctness: Using Lemma 6 we show that PR correctly able to perform better than dfs, the number of image computations decides F AIL when the Err block is reachable. Using Lemmas 2 and partitioning is also fewer for glh than that for dfs. and 6 we show that PR correctly decides unreachability of Err from VIII. RELATED WORK a given state in F . Using Lemmas 7 and 8 we show that ST correctly decides F AIL. Further, when there are no new frontier states, i.e, Prior work on integrating multiple verification algorithms can be F = ∅, it correctly decides P ASS as all states have been explored, classified as either Combination strategies or Partition strategies. and no violation was previously reported as per Lemma 9. 2 Combination Strategies. In software verification, various comple- VII. EXPERIMENTS mentary techniques, including testing, have been combined to address We have implemented the HMC algorithm using the SMT solver the scalability problem [21], [23], [24]. Typically, testing is used yices-1.0.20 [22], the CUDD Library [18], and the Omega li- to reach a concrete state, which is then used as a seed for the brary [10]. We obtained EFSMs from C programs of several in- subsequent symbolic traversal. In particular, lighthouses have been dustry applications as benchmarks, including information manage- used to guide the seed selection [21]. Other methods have used target ment system utilities, ftp utilities, network applications, embedded enlargement [25] and retrograde analysis [26]. The goal is to increase applications in portable devices, lightweight directory access protocol the set of states that are known to lead to errors. Over-approximated (LDAP), and Dhrystone benchmark programs. After aggressive pro- pre-images of the error states [19] have been used as the enlarged gram slicing and constant value propagation, each EFSM has control target either to guide simulation [27] or to improve BMC search [28]. states ranging from 300 to 400. We checked for reachability errors In an interpolant-based approach [29], a bounded over- related to array bound violations, pointer validity, memory leaks, and approximated reachable state set is derived using interpolants, and illegal string operations. used as initial state constraints for the subsequent SAT-based BMC. We present our experimental results for 23 benchmarks (s1-s23), The difference is that such initial state constraints are not precise whose error blocks are known to be hard reach by either state- (as is in our case), and therefore needs multiple refinement steps. based methods or path-based methods in isolation. We compare the In [30], a state-based approach using BDDs is applied to obtain a set performance of HMC with a SMT-based BMC algorithm (BMC) and of reachable set for some bound. This reachable set is then used as a Presburger arithmetic solver based state traversal algorithm (MIX). an initial state constraint for witness search in a stateless approach For a fair comparison, we have used the same set of EFSM models, using SAT-based BMC. The approach is severely limited by the fact the same SMT solvers, the same BDD packages, and the same that it invokes BDD-based model checking only once, and therefore Presburger solvers. may run into severe memory blowup. In contrast, we interleave state Our experiments were conducted on a Linux workstation with a traversal with path-based reasoning at finer granularity, rather than 3.4GHz CPU and 2GB of RAM. The time limit is 2000 seconds and invoke the state-based approach only once as in [30]. the memory limit is 2GB for each run. In HMC, we used 100s time- Partition Strategies. There are prior work on state partitioning, bound and 30 depth-bound (whichever is reached earlier) to switch applied both to stateless and state-based model checking algorithms. from PR to ST. We used tsize = 10, isize = 10, and initial value of In CFG-based traversal methods [31], path conditions are generated fsize = 30 to switch from ST to PR. We experimented with both the for a chosen program path in order to execute it symbolically. In deep-state (dfs) and the goal-directed (glh) prioritization strategies. a recently improvement [32], BMC instances are partitioned based For glh, we set a time limit of 60s, and a threshold K = 1 for the on the control paths, to disjunctively decompose the problem into size of polyhedra to compute the abstract states. smaller subproblems in tunnels. The work in [33] decompose BDD The results are shown in Table I. Column 1 shows the benchmark representations of reachable states in order to parallelize the fixpoint names. Columns 2—4 show the results of BMC, i.e., time (T, in computation. In several other BDD-based approaches [34]–[36], the sec), mem (M, in Mb), and witness depth (wd) if a witness is transition relations, rather than the state sets, are decomposed dis- found (highlighted in bold); otherwise, the peak depth reached (d*). junctively in order to break down the image computation over smaller Columns 5—7 shows the results of MIX. Columns 8—10, 11—13, components. However, these methods do not repeatedly interleave the and 14—16 shows the results of HMC without state partitioning, and state traversal with a path-based reasoning procedure such as PR. the full-blown HMC with two different prioritization strategies dfs IX. CONCLUSION and glh, respectively. For BMC and MIX, d* is the maximum search depth for all paths from the initial state; for HMC, it is the depth for We presented a hybrid model checking algorithm that interleaves a some paths from the initial state. state-based procedure and a stateless symbolic procedure specifically Overall, HMC with dfs and glh find 19 and 15 witnesses, targeted to analyze embedded software. We combine the complemen- respectively, while BMC and MIX in isolation can only find 6 and tary strengths of both procedures in a tightly integrated framework. 14 witnesses, respectively. Furthermore, HMC with dfs finds 4 We use control flow reachability information to simplify the transition unique witnesses (not found by other methods). We also observe relation for both path-based reasoning and state traversal. We present that the MIX times out in several examples, which is due to the time- a simple and yet efficient mechanism to partition state sets for effi- consuming polyhedral simplification inside the Omega library which cient image computation. Furthermore, we present state prioritization gets invoked if the memory usage increases significantly during image techniques that are targeted to find errors quicker. Our experimental
TABLE I TABLE II
COMPARISON OF HMC WITH BMC(STATELESS), MIX(STATE-BASED) STATISTICS OF HMC RUNS
Ex BMC [14] MIX [12] HMC-no-part HMC(glh) HMC(dfs) Ex glh dfs
T M d*/wd T M d*/wd T M d*/wd T M d*/wd T M d*/wd #S #I #F #P #S #I #F #P
s1 0.1 156 16 43 631 16 60 560 16 95 561 16 36 543 16 s1 1 17 0 2 0 16 1 0
s2 102 156 55 TO 1G 31* 606 MO 39* 1.8K MO 108* 201 738 59 s2 5 145 22 14 4 59 18 7
s3 1.8K 156 81 TO 1G 31* 601 MO 39* 991 1.1G 87 562 1G 90 s3 3 106 10 13 4 90 18 11
s4 1.7K 156 80 TO 1G 31* 600 MO 39* 1K 1.1G 86 543 1G 89 s4 3 105 10 13 4 89 18 11
s5 1.1K 156 75 TO 1G 31* 592 MO 39* 1K 1.3G 80 1.1K 1.6G 86 s5 3 108 22 14 4 133 27 16
s6 752 156 69 TO 1G 31* 589 MO 39* 1K 1.3G 75 977 1.3G 78 s6 3 108 22 14 4 120 18 12
s7 TO 160 71* TO 1G 31* 593 MO 39* 1.3K MO 108* 951 1.2G 76 s7 5 145 22 14 4 118 18 12
s8 TO 160 75* TO 1G 31* 605 MO 39* 1.7K MO 51* 1.1K 1.6G 101 s8 4 141 22 14 4 133 27 16
s9 TO 160 68* TO 1G 31* 594 MO 39* 1.8K MO 108* 289 837 69 s9 5 145 22 14 4 69 18 9
s10 TO 160 114* 69 504 114 197 1G 114 324 952 117 1.3K 1.3G 220 s10 1 153 1 2 4 328 11 17
s11 TO 160 117* 132 550 117 190 1.1G 117 334 960 120 1.7K 1.3G 223 s11 1 157 1 2 4 331 11 17
s12 TO 160 120* 189 686 128 246 1.2G 128 353 1G 132 TO 1.6G 258* s12 1 166 16 3 4 368 26 21
s13 TO 160 113* 40 504 113 192 989 113 TO MO 521* TO 1.6G 152* s13 7 646 58 58 4 368 26 21
s14 TO 160 120* 896 1.7G 180 525 2G 180 TO MO 550* TO 1.6G 259* s14 7 681 64 62 4 368 26 21
s15 TO 160 122* 231 711 131 260 1.2G 131 353 1G 135 1.9K 1.6G 239 s15 1 166 16 3 4 368 26 21
s16 TO 160 114* 69 504 114 194 1G 114 TO MO 519* TO 1.6G 259* s16 7 645 58 58 4 368 26 21
s17 TO 160 118* 1.4K MO 184* 1.6K MO 201* TO 1.6G 252* 1.6K 1.3G 224 s17 2 516 29 10 4 332 11 17
s18 TO 160 226* 1.7 243 226 14 783 226 14 785 226 7 306 226 s18 1 226 1 0 1 226 1 0
s19 TO 160 224* 2 244 229 14 774 229 14 776 229 7 306 229 s19 1 229 1 0 1 229 1 0
s20 TO 160 213* 2.4 245 233 14 766 233 14 768 233 8 311 233 s20 1 233 1 0 1 233 1 0
s21 TO 160 226* 1.7 244 226 14 783 226 14 785 226 7 306 226 s21 1 226 1 0 1 226 1 0
s22 TO 160 222* 2 244 229 14 774 229 14 776 229 7 306 229 s22 1 229 1 0 1 229 1 0
s23 TO 160 214* 2.4 245 233 14 766 233 14 768 233 8 311 233 s23 1 233 1 0 1 233 1 0
no-part: no state partition glh,dfs: state prioritization #S: # of switches (PR→ST→PR)
T: Time used (sec) TO: Time out (>2000 s) #F: Peak size of frontier set F
M: Mem used (default Mb, G ≡ Gb) MO: Mem out (>2 Gb) #I: # of image computations
d*: Peak depth before MO/TO wd: Witness Depth #P: # of calls to Partition
results show that the hybrid approach is more robust than applying [18] F. Somenzi. CUDD: CU decision digram package. university of colorado
both the state-based and stateless methods in isolation. at boulder. ftp://vlsi.colorado.edu/pub/.
[19] H. Cho, G. Hatchel, E. Macii, B. Plessier, and F. Somenzi. Algorithms
REFERENCES for approximate fsm traversal based on state space decomposition. IEEE
Trans. on CAD, 1996.
[1] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, [20] T. Yavuz-kahveci, M. Tuncer, and T.Bultan. A library for composite 1999. symbolic representations. In TACAS, 2001. [2] K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, [21] M. Ganai and W. Li. Bang for the buck: Improvising and scheduling 1993. verification engines for effective resource utilization. In Formal Methods [3] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model and Models for Co-Design, 2009. checking without BDDs. In TACAS, 1999. [22] SRI. Yices: An SMT solver. http://fm.csl.sri.com/yices. [4] M. Sheeran, S. Singh, and G. Stalmarck. Checking safety properties [23] P. Godefroid, N. Klarlund, and K. Sen. DART: Directed automated using induction and a SAT solver. In FMCAD, 2000. random testing. In Proc. of PLDI, 2005. [24] R. Majumdar and K. Sen. Hybrid concolic testing. In Proc. of ICSE, [5] M. Ganai and A. Gupta. SAT-based Scalable Formal Verification 2007. Solutions. Springer, 2007. [25] D. Yang and D. Dill. Validating and guided search of the state space. [6] G. Holzmann. The model checker spin. IEEE Trans. Software In DAC, 1998. Engineering, 1997. [26] J. Yuan, J. Shen, J. Abraham, and A. Aziz. On Combining Formal and [7] T. Ball and S. Rajamani. The SLAM toolkit. In CAV, 2001. Informal Verification. In CAV, July 1997. [8] E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C [27] S. Shyam and V. Bertacco. Distance-guided hybrid verification with programs. In TACAS, 2004. guido. In DATE, 2006. [9] F. Ivanˇci´c, Z. Yang, M. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. [28] A. Gupta, M. Ganai, C. Wang, and Z. Yang. Abstraction and bdds F-Soft: Software verification platform. In CAV, 2005. complement SAT-based bmc in diver. In CAV, 2003. [10] W. Pugh. The omega test: a fast and practical integer programming [29] K. McMillan. Interpolation and sat-based model checking. In CAV, algorithm for dependence analysis. In Proc. of Supercomputing, 1991. 2003. [11] T. Bultan, R. Gerber, and C. League. Composite model checking: [30] G. Bischoff, K. Brace, G. Cabodi, S. Nocco, and S. Quer. Exploiting verification with type-specific symbolic representations. In ACM Trans. target enlargement and dynamic abstraction within mixed bdd and sat on Software Engineering Method, 2000. invariant checking. In BMC workshop, 2004. [12] Z. Yang, C. Wang, A. Gupta, and F. Ivanˇci´c. Mixed symbolic represen- [31] T. Arons, E. Elster, S. Ozer, J. Shalev, and E. Singerman. Efficient tations for model checking software programs. In Formal Methods and symbolic simulation of low level software. In DATE, 2008. Models for Co-Design, 2006. [32] M. Ganai and A. Gupta. Tunneling and Slicing: Towards Scalable BMC. [13] C. Wang, Z. Yang, A. Gupta, and F. Ivanˇci´c. Using counterexamples for In DAC, 2008. improving the precision of reachability computation with polyhedra. In [33] A. Narayan, A. Isles, J. Jain, R. Brayton, and A. Sangiovanni-Vincentelli. CAV, 2007. Reachability analysis using partitioned-ROBDDs. In ICCAD, 1997. [14] M. Ganai and A. Gupta. Accelerating high-level bounded model [34] S. Barner and I. Rabinovitz. Efficient Symbolic Model Checking of checking. In ICCAD, 2006. Software Using Partial Disjunctive Partitioning. In Proc. of CHARME, [15] M. Ganai and A. Gupta. Completeness in SMT-based BMC for software 2003. programs. In DATE, 2008. [35] C. Wang, Z. Yang, F. Ivanˇci´c, and A. Gupta. Disjunctive image [16] B. Dutertre and L. de Moura. A fast linear-arithmetic solver for computation for embedded software verification. In DATE, 2006. DPLL(T). In CAV, 2006. [36] D. Ward and F. Somenzi. Decomposing image computation for symbolic [17] H. Kim, F. Somenzi and H. Jin. Efficient Term-ITE Conversion for reachability analysis using control flow information. In ICCAD, 2006. Satisfiability Modulo Theories. In SAT, 2009.