1 Introduction
-
We generalize explicit-value abstraction to be able to enumerate a predefined, configurable number of successor states, improving its precision while still avoiding state space explosion.
-
We adapted a search strategy to the context of CEGAR that estimates the distance from the erroneous state in the abstract state space based on the structure of the original system.
-
We study different splitting techniques applied to complex predicates in order to generalize the result of refinement.
-
We introduce an interpolation strategy based on backward reachability, which traces back the reason of infeasibility to the earliest point.
-
We describe an approach for refinement based on multiple counterexamples, which provides better quality refinement since more information is available.
-
We present combinations of different interpolation strategies that enable selection from different refinements.
2 Background
2.1 Control Flow Automata
-
\(V = \{v_1, v_2, \ldots , v_n\}\) is a set of variables with domains \(D_{v_1}, D_{v_2}, \ldots , D_{v_n}\),
-
\(L\) is a set of program locations modeling the program counter,
-
\(l_0 \in L\) is the initial program location,
-
\(E\subseteq L\times \textit{Ops}\times L\) is a set of directed edges representing the operations that are executed when control flows from the source location to the target.
2.2 Counterexample-Guided Abstraction Refinement (CEGAR)
2.2.1 Abstraction
-
\(S\) is a (possibly infinite) lattice of abstract states,
-
\(\top \in S\) is the top element,
-
\(\bot \in S\) is the bottom element,
-
\(\sqsubseteq {}{} \subseteq S\times S\) is a partial order conforming to the lattice and
-
\(\mathsf {expr}:S\mapsto \textit{FOL}\) is the expression function that maps an abstract state to its meaning (the concrete data states it represents) using a FOL formula.
-
\(N\) is the set of nodes, each corresponding to an abstract state in some domain with locations \(D_L\).
-
\(E\subseteq N\times \textit{Ops}\times N\) is a set of directed edges labeled with operations. An edge \((l_1, s_1, \textit{op}, l_2, s_2) \in E\) is present if \((l_2, s_2)\) is a successor of \((l_1, s_1)\) with \(\textit{op}\).
-
\(C\subseteq S\times S\) is the set of covered-by edges. A covered-by edge \((l_1, s_1, l_2, s_2) \in C\) is present if \((l_1, s_1) \sqsubseteq {}(l_2, s_2)\).
2.2.2 Refinement
-
A implies \(I\),
-
\(I\wedge B\) is unsatisfiable,
-
\(\mathsf {var}(I) \subseteq \mathsf {var}(A) \cap \mathsf {var}(B)\).
-
\(I_0 = \textit{true}\), \(I_n = \textit{false}\),
-
\(I_i \wedge A_{i+1}\) implies \(I_{i+1}\) for \(0 \le i < n\),
-
\(\mathsf {var}(I_i) \subseteq (\mathsf {var}(A_1) \cup \ldots \cup \mathsf {var}(A_i)) \cap (\mathsf {var}(A_{i+1} \cup \ldots \cup \mathsf {var}(A_n)))\) for \(1 \le i < n\).
2.2.3 CEGAR Loop
3 Algorithmic Improvements
3.1 Abstraction
3.1.1 Configurable Explicit Domain
3.1.2 Error Location-Based Search
-
\((w_E= 0, w_D= 1)\) is a traditional breadth-first search.
-
\((w_E= 0, w_D= -1)\) is a traditional depth-first search.
-
\((w_E= 1, w_D= 0)\) considers only the distance from the error location.
-
\((w_E= 2, w_D= 1)\) combines the distance from the error with the depth (BFS), but with less weight.
-
\((w_E= 1, w_D= 2)\) also uses depth and the distance from the error but is biased towards depth.
3.1.3 Splitting Predicates
-
\(\mathsf {atoms}(\varphi )\) splits predicates to their atoms, which is the finest granularity that can be achieved syntactically.9 For example, \(\mathsf {atoms}(p_1 \wedge (p_2 \vee \lnot p_3)) = \{p_1, p_2, p_3\}\).
-
\(\mathsf {conjuncts}(\varphi )\) is a middle ground that splits predicates to their conjuncts. For example, \(\mathsf {conjuncts}(p_1 \wedge (p_2 \vee \lnot p_3)) = \{p_1, (p_2 \vee \lnot p_3)\}\).
-
\(\mathsf {whole}(\varphi ) \equiv \varphi \), i.e., the identity function keeps predicates as a whole, which is the coarsest granularity. It is motivated by Boolean variables, where the atoms are the variables themselves and the valuable information learned by the interpolation procedure lies in the logical connections.
3.2 Refinement
3.2.1 Backward Binary Interpolation
3.2.2 Multiple Counterexamples for Refinement
3.2.3 Multiple Refinements for a Counterexample
4 Evaluation
4.1 Experiment Planning
4.1.1 Research Questions
4.1.2 Subjects and Objects
Source | Category | Models | Tasks | Vars | Locs | Edges | CC |
---|---|---|---|---|---|---|---|
SV-COMP | Locks | 13 | 143 | 4–32 | 9–40 | 10–57 | 3–23 |
Loops | 59 | 105 | 1–11 | 4–26 | 3–33 | 2–19 | |
ECA | 3 | 180 | 9–30 | 302–1301 | 375–1516 | 73–231 | |
ssh-simpl. | 12 | 17 | 64–81 | 187–267 | 262–375 | 87–121 | |
CERN | PLC | 6 | 90 | 1–596 | 8–4614 | 7–4782 | 4–188 |
HWMCC | HWMCC | 300 | 300 | 0–245278 inputs, 0–460501 latches, 0–4806245 gates | |||
Total | 393 | 835 |
4.1.3 Variables
Category | Name | Type | Description |
---|---|---|---|
Model (indep.) | Model | String | Unique name of the model (i.e., verification task) |
Category | Enum. | Category of the model. Possible values: eca, hwmcc, locks, loops, plc, ssh | |
Config. (indep.) | Domain | Enum. | Domain of the abstraction. Possible values: EXPL, PRED_BOOL, PRED_CART, PRED_SPLIT |
MaxEnum | Integer | Maximal number of successors to enumerate in the explicit domain (k). Only applicable if Domain is EXPL | |
PrecGranularity | Enum. | Granularity of the precision. Possible values: GLOBAL, LOCAL | |
PredSplit | Enum. | Predicate splitting method. Possible values: ATOMS, CONJUNCTS, WHOLE. Only valid if Domain is \({ \textsf {PRED\_}}^{ \textsf {*}}\) | |
Refinement | Enum. | Refinement strategy. Possible values: BW_BIN_ITP, FW_BIN_ITP, MAX_PRUNE, MIN_PRUNE, MULTI_SEQ, SEQ_ITP | |
Search | Enum. | Search strategy. Possible values: BFS, DFS, ERR, DFS_ERR, ERR_DFS | |
Metrics (dep.) | Succ | Boolean | Indicates whether the algorithm successfully provided a correct result within the given resource limits |
Termination | Enum. | Indicates the termination reason. Possible values: success, time, memory, exception | |
Result | Boolean | Result of the algorithm, indicates whether the model is safe according to the algorithm | |
TimeMs | Integer | CPU time used by the algorithm (in milliseconds) | |
Memory | Integer | Peak memory consumption of the algorithm (in bytes) |
-
The variable Model represents the unique name of each model (verification task).
-
Furthermore, models have a Category based on their origin.
-
The variable Domain represents the abstract domain used. The values PRED_BOOL and PRED_CART stand for Boolean and Cartesian predicate abstraction, while EXPL stands for explicit-value analysis. Furthermore, our Boolean predicate abstraction with state splitting (Sect. 3.1.3) is encoded by PRED_SPLIT.
-
The integer variable MaxEnum corresponds to the maximal number of successors allowed to be enumerated (denoted by k) in our configurable explicit domain (Sect. 3.1.1). The value 0 represents \(k = \infty \), i.e., there is no limit on the number of successors. Furthermore, the value \(1^*\) enumerates at most one successor without using an SMT solver (corresponding to traditional explicit-value analysis [15]).
-
The variable PrecGranularity represents the granularity of the precision. When the granularity is LOCAL, a different precision can be assigned to each location, whereas GLOBAL granularity means that the precision is the same for each location.
-
The variable PredSplit defines the way complex predicates are split into smaller parts before introducing them in the refined precision (Sect. 3.1.3). Possible values are ATOMS, CONJUNCTS and WHOLE (no splitting).
-
The variable Refinement corresponds to the refinement strategy used. The values FW_BIN_ITP and SEQ_ITP represent traditional binary and sequence interpolation (Sect. 2.2.2). The value BW_BIN_ITP is our novel backward search-based binary interpolation strategy (Sect. 3.2.1), whereas MAX_PRUNE and MIN_PRUNE refer to combined refinements with maximal and minimal prune index (Sect. 3.2.3). The value MULTI_SEQ uses sequence interpolation and our approach of multiple counterexamples (Sect. 3.2.2).
-
The variable Search represents the search strategy in the abstract state space. Values BFS and DFS denote breadth and depth first search. Other values correspond to our error location-based strategy (Sect. 3.1.2) with different weights \(w_D\) and \(w_E\). The strategy ERR only takes into account the error location, i.e., \(w_D= 0\) and \(w_E= 1\). The values ERR_DFS and DFS_ERR use both weights but are biased towards one or the other (\(w_D= 2\), \(w_E= 1\) and \(w_D= 1\), \(w_E= 2\) respectively).
-
The dependent variable Succ indicates whether the algorithm terminated and provided a correct result (no false negative/positive) successfully within the given CPU time and memory limits (effectiveness).
-
The variable Termination indicates the reason for termination (success, timeout, out-of-memory, exception) in a finer way than Succ. It is only used in the detailed plots of the supplementary report [42].
-
The variable Result denotes whether the model is safe or unsafe according to the algorithm. We check that the result matches the expected (if available) and that all configurations agree.
-
The variable TimeMs holds the execution time (CPU time) of the algorithm in milliseconds (efficiency).
-
The variable Memory measures the peak (maximal) memory consumption during the execution of the algorithm in bytes (efficiency).
4.1.4 Experiment Design
4.1.5 Measurement Procedure
4.1.6 Threats to Validity
4.2 Results and Analysis
4.2.1 RQ1: Configurable Explicit Domain
4.2.2 RQ2: Error Location-Based Search
4.2.3 RQ3: Splitting Predicates
4.2.4 RQ4: Backward Binary Interpolation
4.2.5 RQ5: Multiple Counterexamples for Refinement
4.2.6 RQ6: Multiple Refinements for a Counterexample
4.3 Comparison to Other Tools
Configuration name | Domain | MaxEnum | PredSplit | Refinement | Search | PrecGran. |
---|---|---|---|---|---|---|
theta-pred-seq | PRED_CART | ATOMS | SEQ_ITP | BFS | GLOBAL | |
theta-expl-seq | EXPL | \(1^*\) | SEQ_ITP | BFS | GLOBAL | |
theta-pred-bw | PRED_CART | WHOLE | BW_BIN_ITP | ERR | GLOBAL | |
theta-expl-multiseq | EXPL | 1 | MULTI_SEQ | ERR | GLOBAL |