Slicing Software for Model Construction.
Applying finite-state verification techniques (e.g., model checking) to software requires that program source code be translated to a finite-state transition system that safely models program behavior. Automatically checking such a transition system for a correctness property is typically very costly, thus it is necessary to reduce the size of the transition system as much as possible. In fact, it is often the case that much of a program's source code is irrelevant for verifying a given correctness property.In this paper, we apply program slicing techniques to remove automatically such irrelevant code and thus reduce the size of the corresponding transition system models. We give a simple extension of the classical slicing definition, and prove its safety with respect to model checking of linear temporal logic (LTL) formulae. We discuss how this slicing strategy fits into a general methodology for deriving effective software models using abstraction-based program specialization.
Introduction
Modern software systems are highly complex, yet they must
be extremely reliable and correct. In recent years, finite-state
verification techniques, including model checking tech-
niques, have received much attention as a software validation
method. These techniques have been effective in validating
crucial properties of concurrent software systems in a variety
of domains including: network protocols [23], railway
interlocking systems [5], and industrial control systems [3].
Despite this success, the high cost of automatically checking
a given correctness property against a software system
(which typically has an enormous state space) casts doubt
on whether broad application of finite-state verification to
software systems will be cost-effective.
Most researchers agree that the best way to attack the
state-explosion problem is to construct a finite-state transition
system that safely abstracts the software semantics
[7, 10, 26]. The transition system should be small enough
to make automatic checking tractable, yet it should large
Supported in part by NSF and DARPA under grants CCR-
9633388, CCR-9703094, CCR-9708184, and NASA under award NAG
21209.
y Supported in part by NSF under grant CCR-9701418, and NASA
under award NAG 21209.
enough to capture all information relevant to the property
being checked. One of the primary difficulties is determining
which parts of the program are relevant to the property
being checked. In this paper, we show how slicing can automatically
throw away irrelevant portions of the software
code, and hence safely reduce the size of the transition systems
that approximates the software's behavior.
We envision slicing as one of a collection of tools for
translating program source code to models that are suitable
for verification. We previously illustrated how techniques
from abstract interpretation and partial evaluation
can be integrated and applied to help automate construction
of abstract transition systems [11, 20, 21]. Applying
these techniques on several realistic software systems [12, 13]
has revealed an interesting interaction between slicing and
abstraction building: people currently perform slicing-like
operations manually to determine the portions of code that
are relevant for verifying a given property. Thus, preprocessing
software using slicing before applying partial-evaluation-
based abstraction techniques can: (i) provide a safe approximation
of the relevant portions of code, (ii) enable scaling of
current manual techniques to significantly larger and more
complex systems, (iii) reduce the number of components for
which abstractions must be selected and help guide that se-
lection, and (iv) reduce the size of the program to be treated
by abstraction-based partial evaluation tools.
This work is part of a larger project on engineering high-assurance
software systems. We are building a set of tools
that implements the transition system construction methodology
above for Ada and Java. In this paper, we use a simple
flowchart language in order to formally investigate fundamental
issues. We have implemented a prototype for the
slicing system in the paper, and based on this we are scaling
up the techniques. We refer the reader to the project
web-site http://www.cis.ksu.edu/santos/bandera for the
extended version of this paper (which contains more exam-
ples, technical extensions, and proofs), for the prototype,
and for applications of the abstraction techniques to concurrent
Ada systems.
In the next section, we describe the flowchart language
that we use throughout the paper. We then present, in
Section 3, the definition of slicing for this language. We discuss
a specific finite-state verification technique, LTL model
checking, and our approach to constructing safely abstracted
transition systems from source code in Section 4. Section 5
describes how slicing can be applied as a pre-phase to transition
system construction. Section 6 sketches several methods
for deriving slicing criteria from temporal logic specifications
based on the shape of commonly-used formula pat-
terns. Section 7 discusses related work on slicing, and Section
8 summarizes and concludes with a description of future
work.
2 The Flowchart Language FCL
2.1 Syntax
We take as our source language the simple flowchart language
FCL of Gomard and Jones [18, 25, 19]. Figure 1
presents an FCL program that computes the power func-
tion. The input parameters the program are m and n. These
variables can be referenced and assigned to throughout the
program. Other variables such as result can be introduced
at any time. The initial value of a variable is 0. The output
of program execution is the state of memory when the
return construct is executed.

Figure

2 presents the syntax of FCL. FCL programs are
essentially lists of basic blocks. The initial basic block to be
executed is specified immediately after the parameter list. In
the power program, the initial block is specified by the line
(init). Each basic block consists of a label followed a (pos-
sibly empty) list of assignments (we write \Delta for the empty
list, and this is elided when the list is non-empty). Each
block concludes with a jump that transfers control from that
block to another one. Instead of including boolean values,
any non-zero value represents true and zero represents false
in the test of conditionals.
In the presentation of slicing, we need to reason about
nodes in a statement-level control-flow graph (CFG) (i.e., a
graph where there is a separate node for each assignment
and jump) for given program p. We will assume that each
statement has a unique index i within each block. Then,
nodes can be uniquely identified by a pair [l:i] where l is
block label and i is an index value. In Figure 1, statement
indices are given as annotations in brackets [\Delta]. For exam-
ple, the second assignment in the loop block has the unique
identifier (or node number) [loop:2].
The following definition introduces notions related to
statement-level control-flow graphs.
ffl A flow graph e) consists of a set N of
statement nodes, a set E of directed control-flow edges,
a unique start node s, and unique end node e.
ffl The inverse G \Gamma1 of a flowgraph (N; E; s; e) is the flow-graph
all edges are reversed and
start/end states are swapped).
ffl Node n dominates node m in G (written dom(n; m)) if
every path from the start node s to m passes through n.
(note that this makes the dominates relation reflexive).
post-dominates node n in G
(written post-dom(m; n)) if every path from node m to
the end node e passes through n (equivalently, dom(n; m)
in G \Gamma1 ).
ffl Node n is control-dependent on m (some intuition follows
this definition) if
1. there exists a non-trivial path p from m to n such
that every node m 0 ng is post-dominated
by n, and
2. m is not post-dominated by n. [33]
We write cd(n) for the set of nodes on which n is
control-dependent.
Control dependence plays an important role in the rest of
the paper. Note that for a node n to be control-dependent
on m, m must have a least two exit edges, and there must
be two paths that connect m with e such that one contains
n and the other does not. For example, in the power
program of Figure 1, [loop:1], [loop:2], and [loop:3] are
control-dependent on [test:1], but [end:1] is not since it
post-dominates [test:1] (i.e., all paths from [test:1] to halt
go through it).
Extracting the CFG from an FCL program p is straight-
forward. The only possible hitch is that some programs
do not satisfy the "unique end node" property required by
the definition (for example, the program may have multiple
return's). To work around this problem, we assume that
when we extract the CFG from a program p, we insert an
additional node labeled halt that has no successors and its
predecessors are all the return nodes from p.
2.2 Semantics
The semantics of an FCL program p is expressed as transitions
on program states ([l:n]; oe) where l is the label of a
block in p, n is the index of the statement in block l, and oe
is a store mapping variables to values. A series of transitions
gives an execution trace through a program's statement-level
control flow graph. For example, Figure 3 gives a trace of the
power program computing 5 2 . Formally, a trace is finite non-empty
sequence of states written We
for the suffix starting at s i , i.e., -
1 . We omit a formal definition of the transition relation for
FCL programs since it is intuitively clear (a formalization
can be found in [19, 20]).
Slicing
3.1 Program slices
A program slice consists of the parts of a program p that
(potentially) affect the variable values that flow into some
program point of interest [31]. A slicing criterion
specifies the program point n (a node in p's CFG)
and a set of variables V of interest.
For example, slicing the power program with respect to
the slicing criterion yields the program
in

Figure

4. Note that the assignments to variables m and
result and the declaration of m as an input parameter have
been sliced away since they do not affect the value of n at
line [loop:2]. In addition, block init is now trivial and can
be removed, e.g., in a post-processing phase.
Slicing a program p yields a program ps such that the
traces of ps are projections of corresponding traces of p. For
example, the following trace of ps is a projection of the trace
1 Here, we consider only finite traces (corresponding to terminating
executions). The extended version of the paper treats infinite
executions, which are best expressed using co-inductive reasoning
(m n)
(init)
init: result := 1; [1] loop: result := *(result m); [1]
goto test; [2] n := -(n 1); [2]
goto test; [3]
then end
else loop; end: return; [1]

Figure

1: An FCL program to compute m n
Domains
l 2 Block-Labels[FCL]
a 2 Assignments[FCL]
al 2 Assignment-Lists[FCL]
Grammar
al ::= a al j \Delta
a ::= x :=

Figure

2: Syntax of the Flowchart Language FCL

Figure

3: Trace of power program with
(init)
init: goto test; [2] loop: n := -(n 1); [2]
goto test; [3]
then end
else loop; end: return; [1]

Figure

4: Slice of power with respect to criterion
in

Figure

3.
Intuitively, a trace -2 is a projection of a trace -1 if the
sequence of program states in -2 can be embedded into the
sequence of states in -1 . To formalize this, let oe j V denote
the restriction of the domain of oe to the variables in V .
Then, the definition of projection is as follows.
be a program. A projection
function # [M; -] for p-traces is determined by
ffl a set of nodes M from p's CFG, and
ffl a function - that maps each node in M to a set of
variables V
and is defined by induction on the length of traces as follows:
ae
In the classical definition [31, 32] of slicing criterion, one
specifies exactly one point node of interest in the CFG along
with a set of variables of interest at that node. This was the
case with the example slice of the power program above.
For our applications, we may be interested in multiple
program points, and so we generalize the notion of slicing
criterion as follows.
Definition 3 (slicing criterion) A slicing criterion C for
a program p is a non-empty set of pairs
where each n i is a node in p's statement flow-graph and V i
is a subset (possibly empty) of the variables in p. The nodes
are required to be pairwise distinct.
Note that a criterion C can be viewed as a function from
to -(Variables[FCL]). In this case, we write
domain(C) to denote nkg. Thus, a slicing criterion
C determines a projection function # [domain(C); C] which
we abbreviate as # [C]. We can now formalize the notion of
program slice.
Definition 4 (program slice) Given program p with an
associated CFG, let C be a slicing criterion for p. Then
a program ps (also called the residual program) is slice of p
with respect to C if for any p execution trace
where -s is the execution trace of ps running with initial
state s0 .
For example, let
-s be the execution traces of the power program (Figure 1)
and the slice of the power program (Figure 4), respectively.
Then,
3.2 Computing slices
Given a program p and slicing criterion C, Definition 4 admits
many programs ps as slices of p (in fact, p itself is a
(trivial) slice of p). Weiser notes that the problem of finding
a statement minimal slice of p is incomputable [32]. Below
we give a minor adaptation of Weiser's algorithm for computing
conservative slices, i.e., slices that may contain more
statements than necessary. 2
3.2.1 Initial approximation of a slice
Computing a slice involves (among other things) identifying
assignments that can affect the values of variables given in
the slicing criterion. To do this, one computes information
similar to reaching definitions. This requires keeping track
of the variables referenced and the variables defined at each
node in the CFG.
Definition 5 (definitions and references)
ffl Let def(n) be the set of variables defined (i.e., assigned
to) at node n (always a singleton or empty set).
ffl Let ref(n) be the set of variables referenced at node n.

Figure

5 shows the def and ref sets for the power program
of

Figure

1.
Next, for each node in the CFG we compute a set of
relevant variables. Relevant variables are those variables
whose values must be known so as to compute the values of
the variables in the slicing criterion.
Definition 6 (initially relevant variables)
be a slicing criterion. Then
C (n) is the set of all variables v such that either:
1.
2. n is an immediate predecessor of a node m such that
(a)
C (m).
Intuitively, a variable v is relevant at node n if (1) we are at
the line of the slicing criterion and we are slicing on v, or (2)
immediately precedes a node m such that (a) v is used to
define a variable x that is relevant at m (i.e., the value of x
depends on v), or (b) v is relevant at m and it is not "killed
" by the definition at line n. Figure 5 presents the initial
sets of relevant variables sets for the power program of Figure
1 with slicing criterion
n is relevant along all paths leading into node [loop:2]. In
the end block, n is a dead variable and thus it is no longer
relevant.
The classical definition of slicing does not require nodes
mentioned in the slice criterion to occur in the computed
slice. To force these nodes to occur, we define a set of obligatory
nodes - nodes that must occur in the slice even if they
fail to define variables that are eventually deemed relevant.
Definition 7 (obligatory nodes) The set OC of obligatory
nodes is defined as follows:
2 The algorithm we give actually is based on Tip's corrected version
of Weiser's algorithm [31].
fng fng f[test:1]g fng fng

Figure

5: Results of the slicing algorithm for the power program and slicing criteria
The initial slice set S 0
C is the set of nodes that define variables
that are relevant at a successor.
Definition 8 (initial slice set) The initial slice set S 0
C is
defined as follows:

Figure

5 presents the initial slice set S 0
C for the power program
of Figure 1. Node [loop:2] is the only node in S 0
C since
it is the only node that defines a variable that is relevant at
a successor.
Note that S 0
C does not include any conditionals since conditionals
make no definitions. How do we tell what conditionals
should be added? Intuitively, a conditional at node n
should be added if m 2 S 0
C [OC and m is control-dependent
on n. This set of conditionals B 0
C is called the branch set.
Definition 9 (branch set) The initial branch set B 0
C is
defined as follows:

Figure

5 presents the control-dependence information and
the initial branch set B 0
C for the power program of Figure 1.
As explained in Section 2.1, [loop:1], [loop:2], and [loop:3]
are control-dependent on [test:1]. Since [loop:2] is in S 0
OC , control-dependency dictates that [test:1] be included
in the B 0
C .
3.3 Iterative construction
Now we have to keep iterating this process. That is, we add
the conditionals that influence nodes already in the slice.
Then, we must add to the slice nodes that are needed to
compute expressions in the tests of conditionals, and so on
until a fixed point is reached.
ffl relevant variables
where the branch criterion That
is, the relevant variables at node n are those that were
relevant in the previous iteration, plus those that are
needed to decide the conditionals that control definitions
in the previous slice set. Finding such nodes for
a branch b is equivalent to slicing the program with
the criterion f(b; ref(b))g.
ffl slice set
That is, the slice set contains all the conditionals that
controlled nodes in the previous slice set, and all nodes
that define relevant variables.
ffl branch set
That is, the conditionals required are those that control
nodes in the current slice set or obligatory nodes.

Figure

5 presents the sets R 1
C
C which result from
the second iteration of the algorithm. On the next iteration,
a fixed point is reached since n is the only variable required
to compute the conditional test at [test:1] and it is already
relevant at [test:1].
In the iterations, the size of R i
C (n) for all nodes n and
C is increasing, and since R i
C (n) is bounded above by the
number of variables in the program and S i
C is bounded above
by the number of nodes in the CFG, then the iteration eventually
reaches a fixed points R i
C (n) and S i
C .
3.4 Constructing a residual program
Given RC and S C , the following definition informally summarizes
how a residual program is constructed. The intuition
is that if an assignment is in S C , then it must appear in
the residual program. If the assignment is not in S C but in
OC , then the assignment must be to an irrelevant variable.
Since the node must appear in the residual program, the
assignment is replaced with a skip. All goto and return
jumps must appear in the residual program. However, if an
if is not in S C , then no relevant assignment or obligatory
node is control dependent upon it. Therefore, it doesn't
matter if we take the true branch or the false branch. In
this case, we can simply jump to the point where the two
branches merge.
Definition 11 (residual program construction) Given
a program slicing criterion C, let RC ,
OC be the sets constructed by the process above. A residual
program ps is constructed as follows.
ffl For each parameter x in p, x is a parameter in ps only
l is the label of the initial block
of p.
ffl The label of the initial block of ps is the label of the
initial block of p.
ffl For each block b in p, form a residual block bs as follows

- For each assignment line a (with identifier [l:i]),
assignment a appears in the
residual program with identifier [l:i], otherwise if
then the assignment becomes a skip
with identifier [l:i] in the residual program, otherwise
the node is left out of the residual program.
- For jump j in b, if
then j is the jump in bs , otherwise we must have
Now if [l:i] 2 S C then j is the jump in bs , otherwise
the jump in bs is goto l 0 ; with identifier [l:i]
where l 0 is the label of the nearest post-dominating
block for both l 1 and l 2 .
Finally, post-processing removes all blocks that are not targets
of jumps in ps (these have become unreachable).
4 Finite-state Verification
As noted in the introduction, a variety of finite-state verification
techniques have been used to verify properties of soft-
ware. To make our presentation more concrete, we consider
a single finite-state verification technique: model checking of
specifications written in linear temporal logic (LTL). LTL
model checking has been used to reason about properties
of a wide range of real software systems; we have used it,
for example, to validate properties of a programming frame-work
that provides parallel scheduling in a variety of systems
(e.g., parallel implementations of finite-element, computational
fluid dynamics, and program flow analysis problems)
[16, 15].
4.1 Linear temporal logic
Linear temporal logic [27] is a rich formalism for specifying
state and action sequencing properties of systems. An LTL
specification describes the intended behavior of a system on
all possible executions.
The syntax of LTL includes primitive propositions P
with the usual propositional connectives, and three temporal
operators.
(propositional connectives)
(temporal operators)
When specifying properties of software systems, one typically
uses LTL formulas to reason about execution of particular
program points (e.g., entering or exiting a procedure)
as well as values of particular program variables. To capture
the essence of this for FCL, we use the following primitive
propositions.
ffl Intuitively, [l:i] holds when execution reaches
node i in the block labeled l.
ffl Intuitively, [x rop c] holds when the value of variable x
at the current node is related to [[c]] by the relational
operator rop (e.g., [x=0] where rop is =).
Formally, the semantics of a primitive proposition is defined
with respect to states.
ae
true
false otherwise
ae
true if oe(x)
false otherwise
The semantics of a formula is defined with respect to a
trace. The temporal operator 2 requires that its argument
be true from the current state onward, the 3 operator requires
that its argument become true at some point in the
future, and the U operator requires that its first argument
is true up to the point where the second argument becomes
true. Formally [24], let
there exists an i such that
Here are some simple specifications using the logic:
eventually block l5 will be executed
whenever block l2 is executed, block l3 is
always subsequently executed
whenever block l5 is executed x is non-zero
x is always less than 10
4.2 Software model construction
To apply finite-state verification to a software system, one
must construct a finite-state transition system that safely
abstracts the software semantics. The transition system
should be small enough to make automatic checking tractable,
yet it should be large enough to capture all information relevant
to the property being checked. Relevant information
can by extracted by an appropriate abstract interpretation
(AI) [9].
In our approach [12, 20], the user declares for each program
variable an abstract domain to be used for interpreting
operations on the variable. Using a process that combines
abstract interpretation and partial evaluation (which we call
abstraction-based program specialization (ABPS)), a residual
program is created by propagating abstract values and specializing
each program point with respect to these abstract
values [20, 21]. In the residual program, concrete constants
are replaced with abstract constants. The residual program
is a safely approximating finite-state program with a fixed
number of variables defined over finite abstract domains.
This program can then be submitted to a toolset [8, 14]
that generates input for existing model checking tools, such
as SMV [28] and SPIN [23]. This approach has been applied
to verify correctness properties of several software systems
written in Ada [12, 13].
In the steps described above, the user's main task is to
pick appropriate AI's, i.e., AI's that extract relevant infor-
mation, but throw away irrelevant information. The general
idea behind our methodology for chosing AI's is to start simple
(use an AI's that throw all information about dataflow
away) and incrementally refine the AI's based on information
from the specification to be verified and from the program

1. Start with the point AI: Initially all variables are
modeled with the point AI (i.e., a domain with a single
value ? where all operations return ?). In effect, this
throws away all information about a variable's value.
2. semantic features in the specification:
The specification formula to be checked includes, in
the form of propositions, different semantic features of
the program (e.g., valuations of specific program vari-
ables). These features must be modeled precisely by
an AI to have any hope of checking the property. For
example, if the formula includes a proposition [x=0],
then instead of using the point AI for x, one must use
e.g., an AI with the domain fzero; pos; ?g that we refer
to as a zero-pos AI.
3. Select controlling variables: In addition to variables
mentioned explicitly in the specification, we must
also use refined AI's for variables on which specification
variables are control dependent. The predicates
in the controlling conditionals suggest semantic features
that should be modeled by an AI. For example,
if a specification variable x is control-dependent upon a
conditional should use an even/odd
AI for y.
4. Select variables with broadest impact: When
confronted with multiple controlling variables to model,
select the one that appears most often in a conditional.
To illustrate the methodology, Figure 6 presents an FCL
rendering of an Ada process that controls readers and writers
of a common resource [8]. In the Ada system, this server
process runs concurrently with other client processes, and requests
such as start-read, stop-read are entry points (ren-
dezvouz points) in the control process. In the FCL code of

Figure

6, requests are given in the program parameter reqs
- a list of values in the subrange [1::4]. Figure 7 presents
the block-level control-flow graph for the FCL program.
Assume we are interested in reasoning about the invariance
property
The key features that are mentioned explicitly in this specification
are values of variable WriterPresent and execution
of the start-read block. The point AI does not provide
enough precision to determine the states where WriterPresent
has value zero. An effective AI for WriterPresent must
be able to distinguish zero values from positive values; we
choose the zero-pos AI.
At this point we could generate an abstracted model
and check the property or consider additional refinements
of the model; we choose the latter for illustrating our exam-
ple. We now determine the variables upon which the node
[start-read.1] and nodes with assignments to WriterPresent
are control dependent. In our example, there are three such
variables: WriterPresent, ActiveReaders and req. We are
already modeling WriterPresent and req is being used to
model external choice of interactions with the control program
via input. We could choose to bind ActiveReaders to
a more refined AI than point. Given that the conditional expressions
involving that variable are ActiveReaders=0 and
ActiveReaders?0, we might also choose a zero-pos AI. Thus,
only ErrorFlag is abstracted using the point AI.
At this point, we would generate an abstracted model
and check the property. If a true result is obtained then
we are sure that the property holds on the program, even
though the finite-state system only models two variables
with any precision. If a false result is obtained then we
must examine the counter-example produced by the model
checker. It may reveal a true defect in the program or it may
reveal an infeasible path through the model. In the latter
case, we identify the variables in the conditionals along the
counter-example's path as candidates for binding to more
precise AIs.
This methodology is essentially a heuristic search to find
the variables in the program that can influence the execution
behavior of the program relative to the property's proposi-
tions. When a variable is determined to be potentially influ-
its abstraction is refined to strengthen the resulting
system model. In the absence of such a determination, the
variable is modeled with a point abstraction which essentially
ignores any effect it may have; although in the future
it may be determined to have an influence in which case its
abstraction will be refined.
Reducing Models Using Slicing
As illustrated above, picking appropriate abstractions is non-trivial
and could benefit greatly from some form of automated
assistance. The key aspects of the methodology for
picking abstractions included
1. picking out an initial set of relevant variables V and
relevant statements (i.e., CFG nodes N) mentioned in
the LTL specification,
init:
ActiveReaders := 0; [2] raise-error:
WriterPresent := 0; [3] ErrorFlag :=
goto check-reqs; [5]
check-reqs: end:
if (null? reqs) [1] return; [1]
then end
else next-req;
next-req:
reqs := (cdr reqs); [2]
goto attempt-start-read; [3]
attempt-start-read: start-read:
if (req=1 and WriterPresent=0) [1] ActiveReaders := ActiveReaders+1; [1]
then start-read goto check-reqs; [2]
else attempt-stop-read;
attempt-stop-read: stop-read:
if (req=2 and ActiveReaders?0) [1] ActiveReaders := ActiveReaders-1; [1]
then stop-read if (WriterPresent=1) [2]
else attempt-start-write; then raise-error
else attempt-stop-write;
attempt-start-write: start-write:
if (req=3 and ActiveReaders=0 [1] WriterPresent :=
and WriterPresent=0) goto check-reqs; [2]
then start-write
else attempt-stop-write;
attempt-stop-write: stop-write:
if (req=4 and WriterPresent=1) [1] WriterPresent := 0; [1]
then stop-write else check-reqs; if (ActiveReaders?0) [2]
then raise-error
else check-reqs;

Figure

Read-write control example in FCL
2. identifying appropriate AI's for variables in V ,
3. using control dependence information, picking out an
additional set(s) of variables W that indirectly influence
V and N , and
4. identifying appropriate AI's for variables in W .
Intuitively, all variables not in V [ W are irrelevant and can
be abstracted with the point AI.
Clearly, item (1) can be automated by a simple pass over
the LTL specification. Moreover, the information in item
(3) is exactly the information that would be produced by
slicing the program p based on a criterion generated from
information in (1). Thus, pre-processing a program to be
verified using slicing provides automated support for our
methodology. Specifically, slicing can (i) identify relevant
variables (which require AI's other than the point AI), (ii)
eliminate irrelevant program variables from consideration in
the abstraction selection process (they will not be present in
the residual program ps yielded by slicing), and (iii) reduce
the size of the software and thus the size of the transition
system to be analyzed. Other forms of support are needed
for items (2) and (4) above.
For this approach, given a program p and a specification
/, we desire a criterion extraction function extract that extracts
an appropriate slicing criterion C from /. Slicing p
with respect to C should yield a smaller residual program
ps that (a) preserves and reflects the satisfaction of /, and
(b) has as little irrelevant information as possible.
The following requirement expresses condition (a) above.
Requirement 1 (LTL-preserving extract) Given program
p and a specification /, let ps the result
of slicing p with respect to C. Then for any p execution
trace
raise-error
init
attempt-stop-write
attempt-start-write
attempt-stop-read
attempt-start-read
next_req
check-reqs
stop-write
start-write
stop-read
start-read

Figure

7: Read-write control flowchart
where -s is the execution trace of ps running with initial
state s1 .
5.1 Proposition-based slicing criterion
We now consider some technical points that will guide us
in defining an appropriate extraction function. As stated
above, we want to preserve the satisfaction of the formula /
yet remove as much irrelevant information from the original
trace - as possible. We have already discussed the situation
where certain variables' values can be eliminated from the
states in a trace - because they do not influence the satifac-
tion of the formula / under -. What is important in this is
that we have used purely syntactic information (the set of
variables mentioned in /) to reduce the state space.
Let's explain this reduction in more general terms. Consider
a trace
Assume that the state transition s does not influence
the statisfaction of /. Formally, -
-s is the compressed trace (the transition s
compressed)
Another view of the change from - to -s is that the action ff
that causes the change from s i\Gamma1 to s i and the action ff 0 that
causes the change from s i to s i+1 have been combined into
an action ff 00 that moves from s i\Gamma1 to s i+1 . Intuitively, the
formula / "doesn't need to know'' about the intermediate
state s i . For example, the irrelevant transition might be an
assignment to an irrelevant variable, or a transition between
nodes [l:i] and [l:(i + 1)] not mentioned in /.
What is the technical justification for identifying compressible
transitions using a purely syntactic examination of
only the propositions in a formula /? The answer lies in
the fact that, for the temporal operators we are treating,
state transitions that don't change the satisfication of the
primitive propositions of the formula / do not influence the
satisfaction of / itself. This means that we can justify many
trace compressions by reasoning about only single transitions
and satisfaction of primitive propositions. We will see
below that this property does not hold when one includes
other temporal operators such as the next state operator ffi.
We now formalize these notions. The following definition
gives a notion of proposition invariance with respect to a
particular transition.
Definition 12 (P-stuttering transition) Let P be a primitive
proposition, and let
The transition s said to be P -stuttering when
If P is a set of primitive propositions and for each proposition
the transition is said to be P-stuttering.
The following lemma states that the satisfaction of a formula
containing primitive propositions P is invariant with
respect to expansion and compression of P-stuttering steps.
Lemma 1 Let / be a formula and let P be the set of primitive
propositions appearing in /. For all traces
where
This lemma fails when one includes the next state operator
[23] with the following semantics
For example, consider the trace
Let P be the proposition [l:3] and note -
-stuttering (P is false in both
states), but compressing the transition to obtain
does not preserve satification of the formula (i.e., -s 6j=
Intuitively, the next state operator allows one to count
states, and thus any attempt to optimize by compressing
transitions in this setting is problematic. For this reason,
some systems like SPIN [23] do not guarantee that the semantics
of ffi will be preserved during, e.g., partial-order reduction
optimizations.
Given a formula / where P is the set of propositions
in /, we now want to define an extraction function that
guarantees that transitions that are not P-stuttering are
preserved in residual program traces.
ffl For variable propositions observe that
only definitions of the variable x may cause the variable
to change value (i.e., cause a transition to be non-
P -stuttering). This suggests that for each proposition
[x rop c] in a given specification /, each assignment to
x should be included in the residual program. More-
over, x should be considered relevant.
ffl For a proposition entering or leaving CFG
node [l:i] can cause the proposition to change value
(i.e., cause the transition to be non-P -stuttering). One
might imagine that we only need the slice to include
the statement [l:i] for each such proposition in the for-
mula. However, it is possible that compression might
remove all intermediate nodes between two occurences
of the node [l:i]. This, as well as similar situations,
do not preserve that state changes associated with entering
and exiting the node. Therefore, in addition
to the node [l:i], we must ensure that all immediate
successors and all immediate predecessors of [l:i] are
included in the slice.
Based on these arguments, we define an extraction function
as follows.
(Proposition-based extraction)
Given a program p and specification /, let V be the set of
all program variables occurring in /, and let
be the set of all nodes that contain assignments to variables
in V unioned with the set NP of all nodes appearing in node
propositions of / together the successors and predecessors of
each node in NP . Then extract(/)
)g.
1 The extraction function extract satisfies Requirement
1.
As an example,
yields the following criterion
Here, the first three lines of the criterion are the [start-read.1]
node mentioned in the formula, along with its predecessor
and successor. The last three lines are the nodes where
WriterPresent is assigned a value.

Figure

8 presents the resulting slice. The slice is identical
to the original program except that the variable ErrorFlag
and the block raise-error disappear from the program.
Thus, slicing automatically detects what our abstracting
methodology yielded in the previous section: for the given
specification, only ErrorFlag is irrelevant. The previous
conditional jumps in stop-read and stop-write to raise-error
are replaced with unconditional jumps to check-req. In this
case, the slicing algorithm has detected that the nodes in the
raise-error block are irrelevant, and the conditional jumps
are replaced with unconditional jumps to the node where the
true and false paths leading out of the conditionals meet.
As a second example, consider the specification
3[check-reqs:1] ([check-reqs.1] is eventually executed). In
this case extract(/) yields the criterion C2 :? !
Here, the lines of the criterion are the [check-reqs.1] node
mentioned in the formula, along with its predecessor and
successors. Since there are no variable propositions in the
specification, no variables are specified as relevant in the
criterion.

Figure

9 presents the resulting slice. It is obvious that
the residual program is sufficient for verifying the reachability
of [check-req.1] as given in the specification. All
variables are eliminated except reqs which appears in the
test at [check-reqs.1]. Even though it not strictly necessary
for verifying the property, this conditional is retained
by the slicing algorithm since it is control-dependent upon
itself. In addition, the slicing criterion dictates that the node
[next-req.1] should be in the slice. However, since the assignment
at this node does not assign to a relevant variable,
the assignment can be replaced with skip. Finally, the jump
to check-reqs at node [next-req.3] in the residual program
is the result of chaining through a series of trivial goto's
during post-processing.
6 Future Work
The previous criteria have considered individual proposi-
tions. Many property specifications, however, describe states
using multiple propositions or state relationships between
states that are characterized by different propositions. In
this section, we give some informal suggestions about how
the structure of these complex specifications may be exploited
to produce refined slicing criterion.
init:
ActiveReaders := 0; [2]
WriterPresent := 0; [3]
goto check-reqs; [5]
check-reqs: end:
if (null? reqs) [1] return; [1]
then end
else next-req;
next-req:
reqs := (cdr reqs); [2]
goto attempt-start-read; [3]
attempt-start-read: start-read:
if (req=1 and WriterPresent=0) [1] ActiveReaders := ActiveReaders+1; [1]
then start-read goto check-reqs; [2]
else attempt-stop-read;
attempt-stop-read: stop-read:
if (req=2 and ActiveReaders?0) [1] ActiveReaders := ActiveReaders-1; [1]
then stop-read goto check-reqs; [2]
else attempt-start-write;
attempt-start-write: start-write:
if (req=3 and ActiveReaders=0 [1] WriterPresent :=
and WriterPresent=0) goto check-reqs; [2]
then start-write
else attempt-stop-write;
attempt-stop-write: stop-write:
if (req=4 and WriterPresent=1) [1] WriterPresent := 0; [1]
then stop-write else check-reqs; goto check-reqs; [2]

Figure

8: Slice of read-write control program with respect to C1
init:
goto check-reqs; [5]
check-reqs: end:
if (null? reqs) [1] return; [1]
then end
else next-req;
next-req:
reqs := (cdr reqs); [2]
goto check-reqs; [3]

Figure

9: Slice of read-write control program with respect to C2
not included in slice
not included in slice

Figure

10: Slicing abstracted programs
Consider a simple conjunction of propositions appearing
in an eventuality specification
Rather than slicing on the propositions separately, we can
use the semantics of - to refine the slicing criterion. For this
property, we are not interested in all assignments to x but
only those that can influence the value at [l:1]. Thus, our
slicing criterion would be: extract(/)
x)g. This
approach generalizes in any setting where the program point
proposition occurs positively with any number of variable
propositions as conjuncts.
Thus far, we have considered slicing as a prelude to
ABPS. Application of ABPS can, however, reveal semantic
information about variable values in statement syntax,
thereby making it available for use in slicing.

Figure

illustrates a sequence of assignments to x, on
the left, and the abstracted sequence assignments, in the
middle, resulting from binding of the classic signs AI [1]
to x during ABPS. In such a situation we can determine
transitions in the values of propositions related to x (e.g.,
syntactically.
Consider a response property [15] of the form
Our proposition slicing criterion would be based on solely
on /1 and /2 . As with the conjunctions above, we observe
two facts about the structure of this formula that can be
exploited.
1. Within the 2 is an implication, thus we need only
reason about statements that cause the value of /1
to become true (since false values will guarantee that
the entire formula is true).
2. Since the right-hand side of the ) is a 3, we need
only reason about the first statement, in a sequence of
statements, that causes /2 to become true.
The right column of Figure 10 illustrates the effect of
applying observation 1 to eliminate assignments that do not
cause a positive transition in from the sliced
program. Note that if a proposition involving x appears in
/2 then the slicing criterion may be expanded to include
additional statements.
In addition, a program point where /1 holds which is
post-dominated by a point at which /2 holds need not be
considered for the purpose of checking response, since the
existence of this relationship implies that the response holds
for this occurrence of /1 .
Observation 2 can be exploited using post-domination
information. A program point where /2 holds which is post-
dominated by another point where /2 holds does not need to
be included in the slice. This is because only one program
point at which /2 holds is required on any path for the
3 formula to become true. Thus, any post-dominated /2
nodes may be eliminated.
This refined slicing criteria defined above requires the
use of auxiliary information, such as post-domination infor-
mation, that needs to be available prior to slicing. While
the cost of gathering this information and processing it to
compute slicing criteria may be non-trivial, it will be dominated
by the very high cost of performing model checking
on the sliced system. In most cases, the cost of reducing the
the size of the system presented to the model checker will
be more than offset by reduced model check time.
We have discussed two refined criteria based on structural
properties of the formula being checked. Similar refinements
can be defined for a number of other classes of
specifications including precedence and chain properties [15].
These refinements use essentially the same information as
described above for response properties; precedence properties
require dominator rather than post-dominator information

We note that the refined response criteria is applicable
only when the property to be checked is of a very specific
even slight variations in the structure of the formula
may render the sliced program unsafe. A recent survey
of property specification for finite-state verification showed
that response and precedence properties of the form described
above occur quite frequently in practice [16]; 48% of
real-world specifications fell into these two categories.
For this reason, we believe that the effort to define a series
of special cases for extracting criteria based on formula
structure is justified despite its apparent narrowness.
7 Related Work
Program slicing was developed as a technique for simplifying
programs for debugging and for identifying parts of
programs that can execute in parallel [32]. Since its development
the concept of slicing has been applied to a wide
variety of problems including: program understanding, de-
bugging, differencing, integration, and testing [31]. In these
applications, it is crucial that the slice preserve the exact
execution semantics of the original program with respect to
the slicing criterion. In our work, we are interested only
preserving the ability to successfully model check properties
that are correct; this weakening allows for the refinement of
slicing criteria based on the property being checked.
Slicing has been generalized to other software artifacts
[30] including: attribute grammars, requirements models
[22] and formal specifications [4]. Cimitile et. al. [6] use Z
specifications to define slicing criteria for identifying reusable
code in legacy systems. In their work, they use a combination
of symbolic execution and theorem proving to process
the specifications and derive the slicing criteria. In con-
trast, we identify necessary conditions for sub-formula of
commonly occurring patterns of specifications and use those
conditions to guide safe refinement of our basic proposition
slicing criteria.
Our work touches on the relationship between program
specialization and slicing. We use slicing as a prelude to specialization
and suggest that abstraction-based specialization
may reveal semantic features in the residual program's syntax
that could be used by refined slicing criteria. Reps and
Turnidge [29] have studied this relationship from a different
perspective. They show that while similar the techniques
are not equivalent; not all slicing transformations can be
achieved with specialization and vice versa.
While slicing can be viewed as a state-space reduction
technique it has a number of important theoretical and practical
differences from other reduction techniques appearing
in the literature. State-space reduction, such as [17], preserve
correctness with respect to a specific class of correctness
properties. In contrast, our approach to slicing based
on criteria extracted from formulae yields compressed traces
that contain the state changes relevant to propositions contained
in the temporal logic formula. Our approach yields
programs that remain both sound and complete with respect
to property checking. This is in sharp contrast to the many
abstraction techniques developed in the literature (e.g.[7])
which sacrifice completeness for tractability. Finally, even
though significant progress has been made on developing
algorithms and data structures to reduce model checking
times, such as OBDDs [2], those techniques should be seen
as a complement to slicing. If slicing removes variables from
the system that do not influence the behavior to be checked
then the model checker will run faster regardless of the particular
implementation techniques it employs.
8 Conclusion
We have presented a variation of program slicing for a simple
imperative language. We have shown how slicing criteria can
be defined that guarantee the preservation of model check
semantics for LTL specifications in the sliced program. We
have implemented a prototype tool that performs this slicing
and experimented with a number of examples. Based on this
work we are scaling up the prototype to handle significantly
more complex features of programs including: structured
data, treatment of procedures, and multi-threaded programs
that communicate through shared data. While these extensions
are non-trivial they will build of the solid base laid out
in the work reported in this paper.

Acknowledgements

Thanks to James Corbett, Michael Huth, and David Schmidt
for several very illuminating discussions. Thanks also to
Hongjun Zheng for helpful comments on an earlier draft.



--R

Abstract Interpretation of Declarative Languages.
Symbolic model checking: 10 20 states and beyond.
Process control design using spin.

Model checking safety critical software with spin: an application to a railway interlocking system.
reusable functions using specification driven program slicing: A case study.
Model checking and abstraction.
Evaluating deadlock detection methods for concurrent software.
Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.
Abstract interpretation of reactive systems.
Using partial evaluation to enable verification of concurrent software.

Model checking generic container implementations.
Translating ada programs for model checking
Property specification patterns for finite-state verification
Patterns in property specifications for finite-state verification
Using partial orders for the efficient verification of deadlock freedom and safety properties.
Compiler generation by partial evaluation.
An introduction to partial evaluation using a simple flowchart language.
Staging static analysis using abstraction-based program specialization
Specializing configurable systems for finite-state verification
Reduction and slicing of hierarchical state machines.
The model checker spin.
Logic in Computer Science: Modelling and Reasoning about Systems.
Partial Evaluation and Automatic Program Generation.

The Temporal Logic of Reactive and Concurrent Systems: Specification.
Symbolic Model Checking.
Program specialization via program slicing.
Beyond traditional program slicing.
A survey of program slicing techniques.
Program slicing.
Supercompilers for Parallel and Vector Computers.
--TR
On the adequacy of program dependence graphs for representing programs
A Formal Model of Program Dependences and its Implications for Software Testing, Debugging, and Maintenance
The temporal logic of reactive and concurrent systems
Partial evaluation and automatic program generation
Incremental program testing using program dependence graphs
Static slicing in the presence of goto statements
Model checking and abstraction
Design patterns
Property preserving abstractions for the verification of concurrent systems
Beyond traditional program slicing
Abstract interpretation of reactive systems
The Model Checker SPIN
Reduction and slicing of hierarchical state machines
Filter-based model checking of partial systems
Using partial evaluation to enable verification of concurrent software
Patterns in property specifications for finite-state verification
Logic in computer science
Bandera
Abstract interpretation
Symbolic Model Checking
Evaluating Deadlock Detection Methods for Concurrent Software
Staging Static Analyses Using Abstraction-Based Program Specialization
The Semantics of Program Slicing and Program Integration
Program Slicing of Hardware Description Languages
Slicing Programs with Arbitrary Control-flow
A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives
Program Specialization via Program Slicing
Program Analysis as Model Checking of Abstract Interpretations
Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties
reusable functions using specification driven program slicing

--CTR
Heike Wehrheim, Slicing techniques for verification re-use, Theoretical Computer Science, v.343 n.3, p.509-528, 17 October 2005
Matthew B. Dwyer , John Hatcliff , Roby Joehanes , Shawn Laubach , Corina S. Psreanu , Hongjun Zheng , Willem Visser, Tool-supported program abstraction for finite-state verification, Proceedings of the 23rd International Conference on Software Engineering, p.177-187, May 12-19, 2001, Toronto, Ontario, Canada
James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Psreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland
Yunja Choi, From NuSMV to SPIN: Experiences with model checking flight guidance systems, Formal Methods in System Design, v.30 n.3, p.199-216, June      2007
Marieke Huisman , Kerry Trentelman, Factorising temporal specifications, Proceedings of the 2005 Australasian symposium on Theory of computing, p.87-96, January 01, 2005, Newcastle, Australia
Xianghua Deng , Matthew B. Dwyer , John Hatcliff , Masaaki Mizuno, Invariant-based specification, synthesis, and verification of synchronization in concurrent programs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida
G. J. Holzmann , M. H. Smith, An Automated Verification Method for Distributed Systems Software Based on Model Extraction, IEEE Transactions on Software Engineering, v.28 n.4, p.364-377, April 2002
Oksana Tkachuk , Sreeranga P. Rajan, Application of automated environment generation to commercial software, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
Antonella Santone , Gigliola Vaglini, A local approach for temporal model checking of java bytecode, Journal of Computer and System Sciences, v.70 n.2, p.258-281, March 2005
Yunja Choi , Sanjai Rayadurgam , Mats P.E. Heimdahl, Automatic abstraction for model checking software systems with interrelated numeric constraints, ACM SIGSOFT Software Engineering Notes, v.26 n.5, Sept. 2001
Matthew B. Dwyer , John Hatcliff , Robby , Venkatesh Prasad Ranganath, Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs, Formal Methods in System Design, v.25 n.2-3, p.199-240, September-November 2004
Ingo Brckner , Bjrn Metzler , Heike Wehrheim, Optimizing slicing of formal specifications by deductive verification, Nordic Journal of Computing, v.13 n.1, p.22-45, June 2006
Tool Support for Verifying UML Activity Diagrams, IEEE Transactions on Software Engineering, v.30 n.7, p.437-447, July 2004
Radu Iosif , Matthew B. Dwyer , John Hatcliff, Translating Java for Multiple Model Checkers: The Bandera Back-End, Formal Methods in System Design, v.26 n.2, p.137-180, March     2005
Baowen Xu , Ju Qian , Xiaofang Zhang , Zhongqiang Wu , Lin Chen, A brief survey of program slicing, ACM SIGSOFT Software Engineering Notes, v.30 n.2, March 2005
software verification;program slicing;state-space reduction;linear temporal logic;program dependence graph;model-checking