Symbolic Game Semantics for Model Checking Program Families
 8 Citations
 480 Downloads
Abstract
Program families can produce a (potentially huge) number of related programs from a common code base. Many such programs are safety critical. However, most verification techniques are designed to work on the level of single programs, and thus are too costly to apply to the entire program family. In this paper, we propose an efficient game semantics based approach for verifying open program families, i.e. program families with free (undefined) identifiers. We use symbolic representation of algorithmic game semantics, where concrete values are replaced with symbolic ones. In this way, we can compactly represent program families with infinite integers as socalled (finitestate) featured symbolic automata. Specifically designed model checking algorithms are then employed to verify safety of all programs from a family at once and pinpoint those programs that are unsafe (respectively, safe). We present a prototype tool implementing this approach, and we illustrate it with several examples.
1 Introduction
Software Product Line (SPL) [5] is an efficient method for systematic development of a family of related programs, known as variants (valid products), from a common code base. Each variant is specified in terms of features (statically configured options) selected for that particular variant. While there are different implementation strategies, many popular SPLs from system software (e.g. Linux kernel) and embedded software (e.g. cars, phones) domains [18] are implemented using a simple form of two staged computation in preprocessor style, where the programming language is extended with conditional compilation constructs (e.g. \(\texttt {\#ifdef}\) annotations from C preprocessor). At build time, the program family is first configured and a variant describing a particular product is derived by selecting a set of features relevant for it, and only then the derived variant is compiled or interpreted. One of the advantages of preprocessors is that they are mostly independent of the object language and can be applied across paradigms.
Benefits from using program families (SPLs) are multiple: productivity gains, shorter time to market, and greater market coverage. Unfortunately, the complexity created by program families (variability) also leads to problems. The simplest bruteforce approach to verify such program families is to use a preprocessor to generate all valid products of an SPL, and then apply an existing singleprogram verification technique to each resulting product. However, this approach is very costly and often infeasible in practice since the number of possible products is exponential in the number of features. Therefore, we seek for new approaches that rely on finding compact mathematical structures, which take the variability within the family into account, and on which specialized variabilityaware verification algorithms can be applied.
In this work, we address the above challenges by using game semantics models. Game semantics [1, 14] is a technique for compositional modelling of programming languages, which gives models that are fully abstract (sound and complete) with respect to observational equivalence of programs. It has mathematical elegance of denotational semantics, and stepbystep modelling of computation in the style of operational semantics. In the last decade, a new line of research has been pursued, known as algorithmic game semantics, where game semantics models are given certain kinds of concrete automatatheoretic representations [8, 12, 16]. Thus, they can serve as a basis for software model checking and program analysis. The most distinctive property of game semantics is compositionality, i.e. the models are generated inductively on the structure of programs. This is the key to achieve scalable (modular) verification, where a larger program is broken down into smaller program fragments which can be modeled and verified independently. Moreover, game semantics yields a very accurate model for any open program with free (undefined) identifiers such as calls to library functions.
In [9], a symbolic representation of algorithmic game semantics has been proposed for secondorder Idealized Algol (IA\(_2\)). It redefines the (standard) regularlanguage representation [12] at a more abstract level by using symbolic values instead of concrete ones. This allows us to give a compact representation of programs with infinite integers by using finitestate symbolic automata. Here, we extend the symbolic representation of game semantics models, obtaining socalled featured symbolic automata, which are used to compactly represent and verify safety properties of program families.
Motivating example: the program family M and its valid products
We show in Fig. 1, the standard regularlanguage representation of game semantics for these four programs where concrete values are used [12]. We can see that we obtain regularlanguages with infinite summations (i.e. infinitestate automata), since we use infinite integers as data type. Hence, they can be used for automatic verification only if the attention is restricted to finite data types. For example, the model for the product \(A \!\wedge \! \lnot B\) in Fig. 1c illustrates the observable interactions of this term of type \(\mathsf {com}\) with its environment consisting of free identifiers n and abort. So in the model are only represented moves associated with types of n and abort (which are tagged with superscripts n and abort, respectively) as well as with the toplevel type \(\mathsf {com}\) of this term. The environment (Opponent) starts the execution of the term by playing the move \(\textit{run}\); when the term (Player) asks for the value of n with the move \(\textit{q}^n\), the environment can provide any integer as answer. If the answer is 1, the abort is run; otherwise the term terminates successfully by reaching the accepting state (shown as double circle in the model). Note that each move represents an observable action that a term of a given type can perform. Thus, for commands we have a move \(\textit{run}\) to initiate a command and a move \(\textit{done}\) to signal successful termination of a command, whereas for expressions we have a move \(\textit{q}\) to ask for the value of an expression and an integer move to answer the question \(\textit{q}\).
This leads us to propose an approach that solves the general familybased model checking problem: determine for each product whether or not it is safe, and provide a counterexample for each unsafe product.

We introduce a compact symbolic representation, called featured symbolic automata, which represent game semantics of socalled annotative program families. That is, program families which are implemented by annotating program parts that vary using preprocessor directives.

We propose specifically designed (familybased) model checking algorithms for verifying featured symbolic automata that represent program families. This allows us to verify safety for all products of a family at once (in a single execution), and to pinpoint the products that are unsafe (resp., safe).

We describe a prototype tool implementing the above algorithms, and we perform an evaluation to demonstrate the improvements over the bruteforce approach where all valid products are verified independently one by one.
2 The Language for Program Families
The standard approach in semantics community is to use metalanguages for the description of certain kinds of computational behaviour. The semantic model is defined for a metalanguage, and a real programming language (C, ML, etc.) can be studied by translating it into this metalanguage and using the induced model. We begin this section by presenting a metalanguage for which algorithmic game semantics can be defined, and then we introduce static variability into it.
Writing Single Programs. We consider the metalanguage: Idealized Algol (IA) introduced by Reynolds in [17]. It is a compact language which combines callbyname typed \(\lambda \)calculus with the fundamental imperative features and locallyscoped variables. We work with its secondorder recursionfree fragment (IA\(_2\) for short), because game semantics of this fragment has algorithmic properties.
The operational semantics is defined by a bigstep reduction relation: \(\varGamma \vdash M,\mathrm {s} \Longrightarrow V,\mathrm {s}'\), where \(\varGamma \vdash M:T\) is a term in which all free identifiers from \(\varGamma \) are variables, and \(\mathrm {s}\), \(\mathrm {s}'\) represent the state before and after reduction. The state is a function assigning data values to the variables in \(\varGamma \). Canonical forms (values) are defined by \(V \,{:}{:=} \, x \, \mid \, v \, \mid \, \lambda x. M \, \mid \, \mathsf {skip} \, \mid \, \mathsf {mkvar}_{D}MN\). Reduction rules are standard (see [1, 17] for details). If M is a closed term (with no free identifiers) of type \(\mathsf {com}\), then we abbreviate the relation \(M, \emptyset \Longrightarrow \mathsf {skip},\emptyset \) with \(M \Downarrow \). We say that a term \(\varGamma \vdash M:T\) is an approximate of a term \(\varGamma \vdash N:T\), written Open image in new window , if and only if for all termswithhole \(C[]:\mathsf {com}\), such that \(\vdash C[M]:\mathsf {com}\) and \(\vdash C[N]:\mathsf {com}\) are welltyped closed terms of type \(\mathsf {com}\), if \(C[M]\Downarrow \) then \(C[N]\Downarrow \). If two terms approximate each other they are considered observationallyequivalent, denoted by \(\varGamma \vdash M \cong N\).
Writing Program Families. We use a simple form of twostaged computation to lift IA\(_2\) from describing single programs to program families. The first stage is controlled by a configuration k, which describes the set of features that are enabled in the build process. A finite set of Boolean variables describes the available features \(\mathbb {F}= \{ A_1, \ldots , A_n \}\). A configuration k is a truth assignment (a mapping from \(\mathbb {F}\) to \(\mathsf {bool}=\{tt,ff\}\)) which gives a truth value to any feature. If a feature \(A \in \mathbb {F}\) is enabled (included) for the configuration k, then \(k(A)=tt\). Any configuration k can also be encoded as a conjunction of propositional formulas: \(k(A_1) \cdot A_1 \wedge \ldots \wedge k(A_n) \cdot A_n\), where \(tt \cdot A = A\) and \(ff \cdot A = \lnot A\). We write \(\mathbb {K}\) for the set of all valid configurations defined over \(\mathbb {F}\) for a program family. The set of valid configurations is typically described by a feature model [5, 18], but in this work we disregard syntactic representations of the set \(\mathbb {K}\).
3 Symbolic Representation of Game Semantics
In this section we first recall symbolic representation of algorithmic game semantics for IA\(_2\) [9], and then we extend this representation for \(\overline{\text {IA}_2}\).
3.1 Symbolic Models of IA\(_2\)
Let Sym be a countable set of symbolic names, ranged over by upper case letters X, Y, Z. For any finite \(W \subseteq Sym\), the function new(W) returns a minimal symbolic name which does not occur in W, and sets \(W:=W \cup new(W)\). A minimal symbolic name not in W is the one which occurs earliest in a fixed enumeration \(X_1, X_2, \ldots \) of all possible symbolic names. Let Exp be a set of expressions, ranged over by e, inductively generated by using data values (\(v \in D\)), symbols (\(X \in Sym\)), and standard arithmeticlogic operations (\(\mathsf {op}\)). We use a to range over arithmetic expressions (AExp) and b over boolean expressions (BExp).
Let \(\mathcal {A}\) be an alphabet of letters. We define a symbolic alphabet \(\mathcal {A}^{sym}\) induced by \(\mathcal {A}\) as follows: \(\mathcal {A}^{sym} = \mathcal {A} \cup \{ ?X, e \mid X \in Sym, e \in Exp \}\). The letters of the form ?X are called input symbols. They represent a mechanism for generating new symbolic names, i.e. ?X means \(\mathsf {let} \, X=new(W) \, \mathsf {in} \, X \, \ldots \). We use \(\alpha \) to range over \(\mathcal {A}^{sym}\). Next we define a guarded alphabet \(\mathcal {A}^{gu}\) induced by \(\mathcal {A}\) as the set of pairs of boolean conditions and symbolic letters: \(\mathcal {A}^{gu} = \{ [ b, \alpha \rangle \mid b \in BExp, \alpha \in \mathcal {A}^{sym} \}\). A guarded letter \([ b, \alpha \rangle \) means that \(\alpha \) occurs only if b evaluates to true, i.e. \(if \, (b=tt) \, then \, \alpha \, else \, \emptyset \). We use \(\beta \) to range over \(\mathcal {A}^{gu}\). We will often write only \(\alpha \) for the guarded letter \([ tt, \alpha \rangle \). A word \([ b_1, \alpha _1 \rangle \cdot [ b_2, \alpha _2 \rangle \ldots [ b_n, \alpha _n \rangle \) over \(\mathcal {A}^{gu}\) can be represented as a pair \([ b, w \rangle \), where \(b=b_1 \wedge b_2 \wedge \ldots \wedge b_n\) is a boolean condition and \(w=\alpha _1 \cdot \alpha _2 \ldots \alpha _n\) is a word of symbolic letters.
For any (\(\beta \)normal) term, we define a (symbolic) regularlanguage which represents its game semantics, i.e. its set of complete plays. Every complete play represents the observable effects of a completed computation of the given term. It is given as a guarded word \([ b,w \rangle \), where b is also called play condition. Assumptions about a play (computation) to be feasible are recorded in its play condition. For infeasible plays, the play condition is inconsistent (unsatisfiable), thus no assignment of concrete values to symbolic names exists that makes the play condition true. If the play condition is inconsistent, this play is discarded from the final model of the corresponding term. The regular expression for \(\varGamma \vdash M : T\), denoted as \([\! [\varGamma \vdash M : T ]\! ]\), is defined over the guarded alphabet: \(\mathcal A_{[\! [\varGamma \vdash T ]\! ]}^{gu} = \big ( \sum _{x : T' \in \varGamma } \mathcal {A}_{[\! [T' ]\! ]}^{gu \, \langle x \rangle } \big ) + \mathcal {A}_{[\! [T ]\! ]}^{gu} \), where moves corresponding to types of free identifiers are tagged with their names.
Symbolic representations of some language constructs
The representations of some language constructs are given in Table 2. Note that letter conditions different than tt occur only in plays corresponding to “\(\mathsf {if}\)” and “\(\mathsf {while}\)” constructs. In the case of “\(\mathsf {if}\)” command, when the value of the first argument given by the symbol Z is true then its second argument is run, otherwise if \(\lnot Z\) is true then its third argument is run. A composite term \(\mathsf {c}(M_1, \ldots , M_k)\) built out of a language construct “\(\mathsf {c}\)” and subterms \(M_1, \ldots , M_k\) is interpreted by composing the regular expressions for \(M_1, \ldots , M_k\) and the regular expression for “\(\mathsf {c}\)”. Composition of regular expressions ( Open image in new window ) is defined as “parallel composition plus hiding in CSP” [1]. Conditions of the shared (interacting) guarded letters in the composition are conjoined, along with the condition that their symbolic letters are equal [9]. The \(\mathsf {cell}_{v}^{\langle x \rangle }\) regular expression in Table 2 is used to impose the good variable behaviour on a local variable x introduced using \(\mathsf {new}_D \, x\!:=\!v \, \mathsf {in} \, M\). Note that v is the initial value of x, and X is a symbol used to track the current value of x. The \(\mathsf {cell}_{v}^{\langle x \rangle }\) plays the most recently written value in x in response to \(\textit{read}\), or if no value has been written yet then answers \(\textit{read}\) with the initial value v. The model \([\! [\mathsf {new}_D \, x\!:=\!v \, \mathsf {in} \, M ]\! ]\) is obtained by constraining the model of M, \([\! [\mathsf {new}_D \, x \vdash M ]\! ]\), only to those plays where x exhibits good variable behaviour described by \(\mathsf {cell}_{v}^{\langle x \rangle }\), and then by deleting (hiding) all moves associated with x since x is a local variable and so not visible outside of the term [9].
The following formal results are proved in [9]. We define an effective alphabet of a regular expression to be the set of all letters that appear in the language denoted by that regular expression. The effective alphabet of a regular expression representing any term \(\varGamma \vdash M:T\) contains only a finite subset of letters from \(\mathcal A_{[\! [\varGamma \vdash T ]\! ]}^{gu}\), which includes all constants, symbols, and expressions used for interpreting free identifiers, language constructs, and local variables in M.
Theorem 1
For any IA\(_2\) term, the set \(\mathcal {L} [\! [\varGamma \vdash M : T ]\! ]\) is a symbolic regularlanguage over its effective (finite) alphabet. Moreover, a finitestate symbolic automata \(\mathcal {A} [\! [\varGamma \vdash M : T ]\! ]\) which recognizes it is effectively constructible.
Suppose that there is a special free identifier \(\mathsf {abort}\) of type \(\mathsf {com}\). We say that a term \(\varGamma \vdash M\) is safe iff Open image in new window ; otherwise we say that a term is unsafe. Hence, a safe term has no computation that leads to running \(\mathsf {abort}\). Let \(\mathcal {L} [\! [\varGamma \vdash M:T ]\! ]^{CR}\) denotes the (standard) regularlanguage representation of game semantics for a term M obtained as in [12], where concrete values are used. Since this representation is fully abstract, and so there is a close correspondence with the operational semantics, the following holds [7].
Proposition 1
A term \(\varGamma \vdash M:T\) is safe iff \(\mathcal {L} [\! [\varGamma \vdash M:T ]\! ]^{CR}\) does not contain any play with moves from \(\mathcal A_{[\! [\mathsf {com} ]\! ]}^{\langle \textit{abort} \rangle }\), which we call unsafe plays.
The following result [9] confirms that symbolic automata (models) can be used for establishing safety of terms.
Theorem 2
\(\mathcal {L} [\! [\varGamma \!\vdash \! M\!:\!T ]\! ]\) is safe (all plays are safe) iff \(\mathcal {L} [\! [\varGamma \!\vdash \! M\!:\!T ]\! ]^{CR}\) is safe.
For example, \([\! [\mathsf {abort:com^{abort}} \vdash \mathsf {skip \, ; abort:com } ]\! ] = \textit{run}\, \cdot \, \textit{run}^{abort} \, \cdot \, \textit{done}^{abort} \, \cdot \, \textit{done}\), so this term is unsafe.
Since symbolic automata are finite state, we can use modelchecking techniques to verify safety of IA\(_2\) terms with integers. The verification procedure proposed in [9] searches for unsafe plays in the symbolic automata representing a term. If an unsafe play is found, it calls an external SMT solver (Yices) to check consistency (satisfiability) of its play condition. If the condition is consistent, then a concrete counterexample is reported. We showed in [9] that the procedure is correct and semiterminating (terminates for unsafe terms, but may diverge for safe terms) under assumption that constraints generated by any program can be checked for consistency by some (SMT) solver.
Example 1
Consider the term family M from Table 1 in Sect. 1. The symbolic model for the term \(A \!\wedge \! B\) is given in Fig. 2a. The term asks for a value of the nonlocal expression n with the move \(\textit{q}^n\) two times, and the environment provides as answers symbols N and M. When the difference \(NM\) is 1, then abort command is run. The symbolic model in Fig. 2a contains one unsafe play:\([ ?X\!=\!0,\textit{run} \rangle \cdot \textit{q}^n \cdot ?N^n \cdot [ ?X\!=\!X\!+\!N, \textit{q}^n \rangle \cdot ?M^n \cdot [ ?X\!=\!X\!\!M \!\wedge \! X\!=\!1, \textit{run}^{abort} \rangle \cdot \textit{done}^{abort} \cdot \textit{done}\), which after instantiating its input symbols with fresh names becomes: \([ X_1\!=\!0,\textit{run} \rangle \cdot \textit{q}^n \cdot N^n \cdot [ X_2\!=\!X_1\!+\!N, \textit{q}^n \rangle \cdot M^n \cdot [ X_3\!=\!X_2\!\!M \!\wedge \! X_3\!=\!1, \textit{run}^{abort} \rangle \cdot \textit{done}^{abort} \cdot \textit{done}\). An SMT solver will inform us that its play condition (\(X_1\!=\!0 \!\wedge \! X_2\!=\!X_1\!+\!N \!\wedge \! X_3\!=\!X_2\!\!M \!\wedge \! X_3\!=\!1\)) is satisfiable, yielding a possible assignment of concrete values to symbols: \(X_1=0, N=1, X_2=1, M=0\), and \(X_3=1\). Thus, the corresponding concrete counterexample will be: \(\textit{run}\cdot \textit{q}^n \cdot 1^n \cdot \textit{q}^n \cdot 0^n \cdot \textit{run}^{abort} \cdot \textit{done}^{abort} \cdot \textit{done}\). Similarly, concrete counterexamples for terms \(A \!\wedge \! \lnot B\) and \(\lnot A \!\wedge \! B\) can be generated; and it can be verified that the term \(\lnot A \!\wedge \! \lnot B\) is safe. \(\square \)
3.2 Symbolic Models of \(\overline{\text {IA}}_2\)
Again, the effective alphabet of \([\! [\varGamma \vdash _{\mathbb {F}} M:T ]\! ]\) for any \(\overline{\text {IA}_2}\) term is a finite subset of \(\mathcal {A}^{gu+f}_{[\! [\varGamma \vdash _{\mathbb {F}} T ]\! ]}\). Hence, the automata corresponding to \([\! [\varGamma \vdash _{\mathbb {F}} M:T ]\! ]\) is effectively constructible, and we call it featured symbolic automata (FSA). Basically, an FSA is a SA augmented with transitions labelled (guarded) with feature expressions. We denote it as \(\mathcal {FSA} [\! [\varGamma \vdash _{\mathbb {F}} M : T ]\! ] = (Q, i, \delta , F)\), where Q is a set of states, i is the initial state, \(\delta \) is a transition function, and \(F \subseteq Q\) is the set of final states. The purpose of an FSA is to model behaviours (computations) of the entire program family and link each computation to the exact set of products able to execute it. From an FSA, we can obtain the model of one particular product through projection. This transformation is entirely syntactical and consists in removing all transitions (moves) linked to feature expressions that are not satisfied by a configuration \(k \in \mathbb {K}\).
Definition 1
The projection of \(\mathcal {FSA} [\! [\varGamma \vdash _{\mathbb {F}} M : T ]\! ] = (Q, i, \delta , F)\) to a configuration \(k \in \mathbb {K}\), denoted as \(\mathcal {FSA} [\! [\varGamma \vdash _{\mathbb {F}} M : T ]\! ] \mid _k\), is the symbolic automaton \(A=(Q, i, \delta ', F)\), where \(\delta ' = \{ (q_1, [ b,a \rangle , q_2) \mid (q_1, [ \phi ,b,a \rangle , q_2) \in \delta \wedge k \,\models \,\phi \}\).
Theorem 3
(Correctness). \(\mathcal {FSA} [\! [\varGamma \vdash _{\mathbb {F}} M : T ]\! ] \mid _k = \mathcal {A} [\! [\varGamma \vdash \pi _k{(M)} : T ]\! ]\).
Example 2
Consider the term family M from Introduction. Its FSA is given in Fig. 3. Letters represent triples, where the first component indicates which valid configurations can enable the corresponding move. For example, we can see that the unsafe play obtained after instantiating its input symbols with fresh names: \([ tt,X_1=0,\textit{run} \rangle \cdot [ A,tt,\textit{q}^n \rangle \cdot N^n \cdot [ B,X_2=X_1\!+\!N, \textit{q}^n \rangle \cdot M^n \cdot [ tt,X_3=X_2\!\!M \!\wedge \! X_3=1, \textit{run}^{abort} \rangle \cdot \textit{done}^{abort} \cdot \textit{done}\), is feasible when \(N=1\) and \(M = 0\) for the configuration \(A \!\wedge \! B\). \(\square \)
4 Model Checking Algorithms
The general model checking problem for program families consists in determining which products in the family are safe, and which are not safe. The goal is to report all products that are not safe and to provide a counterexample for each.
A straightforward but rather naive algorithm to solve the above problem is to check all valid programs individually. That is, compute the projection of each valid configuration, generate its model, and verify it using standard algorithms. This is socalled brute force approach, and it is rather inefficient. Indeed, all programs (exponentially many in the worst case) will be explored in spite of their great similarity. We now propose an alternative algorithm, which explores the set of reachable states in the FSA of a program family rather than the individual models of all its products. We aim to take advantage of the compact structure of FSAs in order to solve the above general model checking problem.
After having found an unsafe state, our algorithm will continue exploration until the entire model is explored. Since the aim is to identify violating products, it can ignore products that are already known to violate, \(\mathbb {K}_{unsafe}\), that is \(\cup _{(e,px) \in unsafe} px\). In the BFS, this can be achieved by filtering out states with products \(px \subseteq \mathbb {K}_{unsafe}\) as part of the calculation of new. This can only eliminate newly discovered states, not those that are already on the queue. States on the queue can be filtered out by removing elements (q, px) for which \(px \subseteq \mathbb {K}_{unsafe}\) (line 9).
Compared to the standard BFS, where visited states are marked with Boolean visited flags and no state is visited twice, in our algorithm visited states are marked with sets of products (for which those states are visited) and a state can be visited multiple times. This is due to the fact that when the BFS arrives at a state s for the second time, such that \(R(q)=px\), \((q,px') \in new\), and \(px' \nsubseteq px\), then s although already visited, has to be reexplored since transitions that were disallowed for px during the first visit of q might be now allowed for \(px'\).
Theorem 4
(Correctness). \(\varGamma \vdash \pi _k(M)\) is safe iff \(\mathcal {FSA} [\! [\varGamma \vdash _{\mathbb {F}} M ]\! ] \mid _k\) is safe.
As a corollary of Theorems 2, 3, 4 we obtain that the VP in Fig. 5 returns correct answers for all products. Moreover, it terminates for all unsafe products by generating the corresponding unsafe plays. The VP will find the shortest consistent unsafe play t for each unsafe product after finite number of calls to the BFS, that will first find all inconsistent unsafe plays shorter than t (which are finitely many [9]). However, the VP may diverge for safe products, producing in each next iteration longer and longer unsafe plays with inconsistent conditions.
5 Implementation
The arrays are implemented in the symbolic representation by using a special symbol (e.g., k with an initial constraint \(k>0\)) to represent the length of an array. A new symbol (e.g., I) is also used to represent the index of the array element that needs to be dereferenced or assigned to (see [9] for details). If we also want to check for arrayoutofbounds errors, we can include in the representation of arrays plays that perform \(\mathsf {abort}\) moves when \(I \ge k\).
We ran our tool on a 64bit Intel\(^\circledR \)Core\(^{TM}\) i5 CPU and 8 GB memory. All times are reported as averages over five independent executions. For our experiments, we use four families: Intro is the family from Table 1 in Sect. 1; Linear \(_3\) is the above family for linear search with three features; Linear \(_4\) is an extended version of Linear \(_3\) with one more feature D and command: \(\texttt {\#if} \, (D) \, \mathsf {then} \, j:=j+3\); and Linear \(_5\) is Linear \(_4\) extended with one additional feature E and command: \(\texttt {\#if} \, (E) \, \mathsf {then} \, j:=j2\). We restrict our tool to work with bounded number of iterations (10 in this case) since the VP loops for safe terms. For Linear\(_4\) the tool reports 13 unsafe products with corresponding counterexamples, whereas for Linear\(_5\) 21 unsafe products are found. Figure 6 compares the effect (in terms of Time, the number of states in the maximal model generated during analysis Max, and the number of states in the final model Final) of verifying benchmarks using our familybased approach vs. using bruteforce approach. In the latter case, we first compute all products, generate their models, and verify them one by one by using the tool for single programs [9]. In this case we report the sum of number of states for the corresponding models in all individual products. We can see that the familybased approach is between 2.3 and 3.6 times faster (using considerably less space) than the bruteforce. We expect even bigger efficiency gains for families with higher number of products.
6 Related Work and Conclusion
Recently, many socalled lifted techniques have been proposed, which lift existing singleprogram analysis techniques to work on the level of program families (see [18] for a survey). This includes lifted type checking [3], lifted model checking [4], lifted dataflow analysis [11], etc. Classen et al. have proposed featured transition systems (FTSs) in [4] as the foundation for behavioural specification and verification of variational systems. An FTS, which is featureaware extension of the standard transition systems, represents the behaviour of all instances of a variational system. They show how the familybased model checking algorithms for verifying FTSs against fLTL properties are implemented in the SNIP model checker. The input language to SNIP is fPromela, which is a featureaware extension of Promela. In this work, we also propose special familybased model checking algorithms. However, they are not applied on models of variational systems, but on game semantics models extracted from concrete program fragments with #ifdefs.
The first application of game semantics to model checking was proposed by Ghica and McCusker in [12]. They show how game semantics of IA\(_2\) with finite datatypes can be represented in a remarkably simple form by regularlanguages. Subsequently, several algorithms have been proposed for model checking IA\(_2\) with infinite data types [7, 9]. The automatatheoretic representation of game semantics have been also extended to programs with various features: concurrency [13], thirdorder functions [16], probabilistic constructs [15], nondeterminism [6], etc.
To conclude, in this work we introduce the featured symbolic automata (FSA), a formalism designed to describe the combined game semantics models of a whole program family. A specifically designed model checking technique allows us to verify safety of an FSA. The proposed approach can be extended to support multifeatures and numeric features. Socalled variability abstractions [10, 11] can also be used to define abstract familybased model checking.
Footnotes
 1.
For the work in this paper, we assume that the set of features \(\mathbb {F}\) is fixed and all features are globally scoped.
References
 1.Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions. Electr. Notes Theor. Comput. Sci. 3, 2–14 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
 2.Apel, S., von Rhein, A., Wendler, P., Größlinger, A., Beyer, D.: Strategies for productline verification: case studies and experiments. In: 35th International Conference on Software Engineering, ICSE 2013, pp. 482–491 (2013)Google Scholar
 3.Chen, S., Erwig, M., Walkingshaw, E.: An errortolerant type system for variational lambda calculus. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, pp. 29–40. ACM (2012)Google Scholar
 4.Classen, A., Cordy, M., Schobbens, P.Y., Heymans, P., Legay, A., Raskin, J.F.: Featured transition systems: foundations for verifying variabilityintensive systems and their application to LTL model checking. IEEE Trans. Softw. Eng. 39(8), 1069–1089 (2013)CrossRefGoogle Scholar
 5.Clements, P., Northrop, L.: Software Product Lines: Practices and Patterns. AddisonWesley, Boston (2001)Google Scholar
 6.Dimovski, A.: A compositional method for deciding equivalence and termination of nondeterministic programs. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 121–135. Springer, Heidelberg (2010)CrossRefGoogle Scholar
 7.Dimovski, A., Ghica, D.R., Lazić, R.: Dataabstraction refinement: a game semantic approach. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 102–117. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 8.Dimovski, A., Lazic, R.: Compositional software verification based on game semantics and process algebra. STTT 9(1), 37–51 (2007)CrossRefGoogle Scholar
 9.Dimovski, A.S.: Program verification using symbolic game semantics. Theor. Comput. Sci. 560, 364–379 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
 10.Dimovski, A.S., AlSibahi, A.S., Brabrand, C., Wąsowski, A.: Familybased model checking without a familybased model checker. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 282–299. Springer, Heidelberg (2015)CrossRefGoogle Scholar
 11.Dimovski, A.S., Brabrand, C., Wasowski, A.: Variability abstractions: trading precision for speed in familybased analyses. In: 29th European Conference on ObjectOriented Programming, ECOOP 2015. LIPIcs, vol. 37, pp. 247–270. Schloss Dagstuhl  LeibnizZentrum fuer Informatik (2015)Google Scholar
 12.Ghica, D.R., McCusker, G.: The regularlanguage semantics of secondorder idealized algol. Theor. Comput. Sci. 309(1–3), 469–502 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
 13.Ghica, D.R., Murawski, A.S.: Compositional model extraction for higherorder concurrent programs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 303–317. Springer, Heidelberg (2006)CrossRefGoogle Scholar
 14.Hyland, J.M.E., Luke Ong, C.H.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
 15.Legay, A., Murawski, A.S., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 173–187. Springer, Heidelberg (2008)CrossRefGoogle Scholar
 16.Murawski, A.S., Walukiewicz, I.: Thirdorder idealized Algol with iteration is decidable. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 202–218. Springer, Heidelberg (2005)CrossRefGoogle Scholar
 17.Reynolds, J.C.: The essence of Algol. In: O’Hearn, P.W., Tennent, R.D. (eds.) Algollike Languages. Birkhaüser, Basel (1997)Google Scholar
 18.Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 6 (2014)CrossRefGoogle Scholar