Lightweight Reasoning about Program Correctness.
Automated verification tools vary widely in the types of properties they are able to analyze, the complexity of their algorithms, and the amount of necessary user involvement. In this paper we propose a framework for step-wise automatic verification and describe a lightweight scalable program analysis tool that combines abstraction and model checking. The tool guarantees that its True and False answers are sound with respect to the original system. We also check the effectiveness of the tool on an implementation of the Safety-Injection System.
Introduction
Recent years have seen an increasing interest in computer-supported
techniques for analyzing correctness of software
artifacts. In particular, this interest is caused by the effectiveness
and potential of lightweight formal methods [18].
In this approach, verification consists of automated checking
of an artifact against some critical properties (e.g., deadlock-
security, fairness), often concentrating on debugging
instead of assurance. Most often lightweight methods
include model checking [5] - a technique for automatically
verifying properties of a system. Given a system and a prop-
erty, a model checker buildsthe reachability graph by exhaustively
exploring the state-space of the system. A number of
industrial model checkers have been developed, including
SPIN [15], SMV [22], and MurOE [10]. Althoughmodel checking
started as a technique for verifying hardware, it has been
effectively applied in a variety of software projects. For ex-
ample, SMV was used to verify correctness of mode logic
in A-7 aircraft [25] and TCAS specifications [4]; SPIN was
applied to the validation of the remote object invocation in
CORBAGIOP [20], checking Java programs [14], and many
others. Model checking became part of the routine V&V process
during the development of Lucent's new server product
[16], and has been applied to reasoning about user interfaces
[12] and business processes [19].
Model checking offers a potential for push-button verifi-
cation. However, this potential is not easily realizable, especially
for checking correctness of programs, as opposed to
specifications, protocols, or other software artifacts. First of
all, model checking is mostly limited to finite-state systems
(i.e., every variable in the system should have a finite domain).
Several model checkers allow reasoning about infinite-state
systems by "executing" all paths of the system up to a certain
depth [13, 15]. However, such systems cannot guarantee
that the system satisfies the desired property. To check pro-
grams, an analyst has to utilize abstractions, computed either
automatically or by hand [16]. And, although it is highly-
desirable that properties hold on the abstracted model if and
only if they hold in the original model [6], such assurance is
difficult to obtain: a different abstraction has to be built for
each class of properties under analysis [9].
Given a large number of available verification techniques
and a potential complexity and expense of their application
and interpretation of results, we propose a "layered" approach
to automatic verification, depicted in Figure 1. Given a system
S and a property P , we would like to know if P holds
in S. We would like to start at verification level 1, which
is fairly inexpensive, both in terms of the work required of
the user, and in terms of computing resources required. This
step will result in one of three conclusions: P is definitely
true or definitely false in S, at which point the verification
stops, or the analysis cannot yield any information. In the
latter case, the analyst will apply a technique on verification
property
is true
more expensive
analysis
property
is false verification step 2
verification step 1
step N
verification

Figure

1: Framework for automatic verification.
level 2. This technique is more expensive than that of verification
level 1, but may help in determining whether or not
holds. If it does not, the analyst proceeds in applying more
and more complex and expensive techniques until 1) P is definitely
proved or definitely disproved or 2) all levels are exhausted
or all resources are exhausted. Note that no precision
is lost at each level. All properties that have not been
concluded to definitely hold or definitely not hold on S during
the verification level have to proceed to level k.
What is the benefit of the step-wise verification frame-work
outlinedabove? It allows us to categorize existing tools
based on their effectiveness in verifying properties and the
complexity of application (this complexity metric includes
the effort needed by a human and the effort needed by a com-
puter). This also allows one to utilize verification efforts more
effectively.
In this paper, we discuss verification of sequential programs
against fairly complex properties, involving temporal
logic and arithmetic on values of variables, e.g. "a is never
less than b", "immediately after 2a will be true".
However, our approach is to build a "level 1" verifier. First,
we compute the abstraction of behaviors of the program under
analysis using abstract interpretation. This abstraction
is not dependent on a choice of properties to verify and is
computed automatically, even though the program may not
be finite-state. Then we model check the abstracted system.
If our analysis yields True, the property holds in the original
system; if it yields False, the property does not hold, and if
it yields Maybe, the analysis is inconclusive. For such cases,
properties can be verified using more expensive techniques.
The idea of verification with the presence of abstraction
has been explored by several researchers. In particular, Jackson
[17] proposed a model checking method to analyze infinite
specifications expressed in Z or VDM. His approach defines
an abstract state space where each abstract state represents
a (possibly infinite) equivalence class of concrete states.
Dams [9] demonstrated how to abstract reactive systems, so
that the abstracted transition systems preserves certain forms
of combined safety/liveness properties. Pardo [24] built the
abstract and the concrete models of the system and conservatively
verified properties expressed in -calculus on the abstracted
model. If the formula is proved false, related states
are then successively refined, until the given formula is verified
or computational resources are exhausted.
The rest of this paper is organized as follows: Section 2
gives an overview of model checking and abstract interpre-
tation. Section 3 discusses the theoretical goals of this work
and introduces new algorithms for our program verification
system. Proofs of correctness of some of these algorithms are
given in the Appendix. The design of this system is described
in Section 4. Section 5 demonstrates the results of using our
abstract model checker to analyze the Safety-Injection Sys-
tem. We conclude the paper with the summary of this work
and the outline of future research directions.
Background
In this section we recall the basic definitions of abstract interpretation
and model checking.
2.1

Abstract

Interpretation
Abstract interpretation [8, 9] is a way of symbolically executing
programs using abstract instead of concrete domain. Familiar
data-flow analysis algorithms, e.g., constant propagation
or live variables, are examples of abstract interpretation.
Let D c and D a be the concrete and the abstract domains, re-
spectively. The abstraction function ff : 2 D c ! D a maps a
set of concrete values into an abstract value. ff has an inverse,
the concretization function . An abstraction
is valid if the pair of functions (ff, fl) forms a Galois connection

For example, we can perform a "sign analysis" by replacing
a set of integers (D signs ((\Gamma), (+), or (0)).
Here, . We can execute
the program on the abstract values. For example,
(f\Gamma1345g \Theta f17g) ff
However, the abstract values cannot always be determined
exactly. Consider the following example:
(f\Gamma1345g \Theta f17g
can be represented as a set f(\Gamma); (+); (0)g with the interpretation
that the result can be any of these values. When
the abstract domain is finite, the abstract interpretor acts as
a data-flow analyzer. However, we may also want to use abstract
interpretationto reason about infinite-domain variables.
In order to achieve tractability, we need to ensure that the abstraction
is converging:
1. we have a finite representation of the infinite set of val-
ues. One way is to abstract from a set to an interval by
taking the minimum (maximum) value from the set as
the left (right) bound of the interval. For example,
2. we ensure convergence in a finite number of steps. With
a finite-domain abstraction, convergence is guaranteed.
To achieve convergence for the infinite-domain abstrac-
tion, [8] introduced an abstract binary operator widen-
ing, denoted as r, which represents a "jump". For any
abstract values i 0 and ri 1 . [8] defined
widening as follows:
For example,
2.2 Model Checking
In this paper we will concern ourselves withCTL model checking
- an automatic technique for verifyingproperties expressed
in a propositionalbranching-time temporal logic called Computational
Tree Logic (CTL) [5]. The system is defined by
a Kripke structure, and properties are evaluated on a tree of
infinite computations produced by the model of the system.
The standard notation M; s indicates that a formula f
holds in a state s of a model M . If a formula holds in the
initial state, it is considered to hold in the model.
A Kripke structure consists of a set of states S, a transition
relation R ' S \Theta S, a set of initial states I, a set of atomic
propositions P , and a labeling function L
must be a total function, i.e, 8s 2
If a state s n has no successors, we add a self-loop to it, so
that Intuitively, for each s 2 S, the labeling
function provides a list of atomic propositionswhich are True
in this state.
We use CTL on boolean expressions that include variables
and arithmetic operations on them. The set P of atomic propositions
is defined as follows:
If P 1 and P 2 are terms, then
are
atomic propositions.
Terms are defined recursively as
1. Every identifier and every constant is a term.
2. If t is a term, so is (t).
3. If t 1 and t 2 are terms, so are t 1
mod and exp are the mod and the exponentiation functions,
respectively. For example, the following are some atomic
propositions in this version of CTL:
CTL is then defined as follows:
1. Every atomic proposition
2. If ' and are CTL formulas, then so are :', ' - ,
The logic connectives :, - and - have their usual meanings.
The existential (universal) quantifier E (A) is used to quantify
over paths. The operator X means "at the next step", F
represents "sometime in the future", and U is "until". There-
fore, EX' (AX') means that ' holds in some (every) immediate
successor of the current program state; EF' (AF')
means that ' holds in the future along some (every) path emanating
from the current state; E['U ] (A['U ]) means that
for some (every) computation path starting from the current
state, ' continuously holds until becomes true. Formally,
exists some path s
Note that AF (') j A[True U ']; and EF (') j E[True U '],
that is, we are using a "strong until". We also use the abbreviations
EG(') and AG(') to represent the property that '
holds at every state for some (every) path emanating from s 0 .
EG and AG are defined as:
3 Lightweight Model Checking
The goal of this work is to use abstract interpretation to alleviate
the state explosion problem of model checking while
ensuring that the properties verified on the abstract system
can be properly interpreted in the original system. This goal
is achieved by constructing an abstract model checker on our
three-valued logic that returns values True, False and Maybe,
such that the analysis that results in True and in False is sound.
Using static analysis, we build the abstract system by associating
each line of the program with an abstraction of the set
of values that program variables can attain when the control
reaches this point along any execution path. This abstraction,
which reduces the state-space for finite-state and for infinite-
state systems, is computed completely automatically.
In this section we introduce the language for constructing
programs, describe the process of building the labeled transition
machine, and present a model checking algorithm on
the three-valued logic.
3.1 The Input Language
Our input language, called C-, is a sequential language with
the syntax similar to C. The language includes the following
constructs: booleanandinteger types; conditionalcon-
trol structures (if, else); loops (while); input and output
(print, fprint, scan, fscan); assignments; functions
and procedures. Dynamic features such as recursion or
pointers are not provided in this language. It also does not
allow any user-defined (compound) data structures. A complete
grammar of the language is available in [11]. Figure 2
gives an example program written in C-.
3.2 Construction of a Labeled Transition System
Here, we describe the transformation of the program representation
into a labeled transition system.
We start with a (infinite-state) program
is a (infinite) set of states, s 0 2 W is
the initial state, R ' W \Theta W is the total accessibility rela-
tion, and LT and LF are truth and falsity labeling functions,
mapping each state to the set of propositionsthat are True and
False, respectively, in this state (L T
In C-, as in C, there is no one-to-one correspondence between
assignments to variables and lines of code. In fact, before
attempting to verify programs expressed in C-, we need
to give it a well-defined formal semantics, i.e., describe the
way in which each construct transforms the "program state"
[23]. We define a state to be the mapping between the set
of global variables and their values, and thus a state change
occurs when at least one of the global variables changes its
value.
Our goal is to construct an abstract finite Kripke structure,
in which every edge represents a state change in the program.
In order to do that, we define a set of variables V and let Vw '
V be the set of variables which are accessible in the lexical
scope associated with a state w 2 W , and G ' V be the set
of variables which are accessible at every point of the pro-
gram. Thus, G is the set of global variables. Each state w in
the program is an n+1-tuple,
(v )), in which ln corresponds to the line number of the
state in the program, and
here d i is a subset of D i - the values of the concrete domain
of v i . CTL properties about such programs can be expressed
only in terms of global variables.
We start the analysis by parsing the program and building
an

Abstract

Syntax Tree (AST). AST is an intermediate representation
for the structure of the program under interpreta-
tion. Next, we propagate information for all variables (global
and local) in the current scope throughout the AST, until we
reach a fixpoint. Abstractions are formed by mapping a concrete
state w onto an abstract state w ff (w
each d i 2 2 D i is mapped onto an abstract value D ff i . The result
is an abstract state space W ff , in which each w ff 2 W ff is
an n+1-tuple w
Notice that line numbers and the set of variables are the same
in the concrete and the abstract state space. ff is chosen so
that W ff is finite, and an abstract state w ff can represent one
or more or even an infinite number of concrete states due to
the abstraction. Moreover, there is only one state associated
with each line of code. Let R ff be a transition relation over
the abstract state space, R ff ' W ff \Theta W ff . R ff is constructed
as follows: (s
Our labeling functions then become
In the concrete domain, 8w 2 W ,
Under the assumptions of
the Galois connection framework, an abstract system has at
least as many behaviors as the corresponding concrete one.
Typically, verification on abstracted systems is done either
conservatively or optimistically. The former case provides
"reliable negative" answers, with L ff T ' LT , and L ff F '
LF . The latter case provides "reliable positive" answers, with
In either case, one side of
the answer cannot be trusted. The goal of our work is to ensure
that we get "reliable positive" and "reliable negative"
answers, i.e., L ff T ' LT and L ff F ' LF . So, in our case,
. The resulting abstract
finite-state program is PG
In order to construct an abstract Kripke structure in which
every transition corresponds to a change to a global variable,
we define a "global variable changed" predicate p on a state
such that p(y) is True iff 9x; (x; y) 2 R ff , 9g 2 G, s.t.
g's abstract value in state x (y). Now we construct
an abstract aggregate state space S ff in which every element
contains one state w ff which involves a change to
a global variable, and other states that do not involve changes
to global variables and can be reached from w ff via the transitive
closure of R ff (denoted R ff  ). s ff is defined recursively
as follows:
ffl if p(w ff ) is true, then w ff 2 s ff .
1: int b; 12:
2: int xy; 13: else
3: int main ( ) { 14:
4: int a; 15: if ( (a !=
5: int c; 16: if ( (a != 2) && (a !=
7:
8: print("xy is ", xy);
9: while { 20: print("b is ", b);

Figure

2: A program fragment.
Note that values of global variables within s ff are the same.
We will refer to L ff
T and L ff
F as labeling functions that map
each s ff 2 S ff to a set of atomic propositions on global variables
that are true (false) in that state. Finally, the transitions
between states in S ff , E ff ' S ff \Theta S ff , are thus defined as:
Our abstract Kripke structure K
ready.
3.3 Model Checking Algorithm
We now present the algorithm that receives a Kripke structure
K ff constructed above and a correctness propertyexpressed
in the version of CTL described in Section 2, and determines
whether or not the property holds in the system. As mentioned
in the previous section, we want to ensure that our analysis
yields "reliable positive" and "reliable negative" answers,
i.e., if the analysis concluded that a property is True, then it
holds in the original system, and if the analysis concluded
that a property is False, then it does not hold in the original
system. In order to do so, we introduce a third logical
value Maybe. Thus, if the analysis concluded that a property
Maybe holds in the system, then it is unknown whether or not
the property holds in the concrete system.
The algorithm recursively goes through the structure of
the property under analysis, associating each subproperty '
with a pair of sets of states (Yes('), No(')). Yes(') ' S ff
is a set of states in which ' is True, or, more formally, s ff 2
which represents a set of
states in which ' is False, is defined similarly. We also define
a predecessor function pred : 2 S ff
which, given a set
of states Q, returns all the states that can reach some state in
Q in one transition:
The algorithm, inspired by Bultan'ssymbolic model checker
for infinite-state systems [3], is given in Figure 3. For exam-
ple, a property p - q holds in state s ff if s ff is in Yes sets of
both p and q. The same property does not hold in state s ff if
s ff is in the No set of either p or q. When verifying EXp, we
note that if p holds in some immediate successor of state s ff ,
then EXp holds in s ff ; any immediate successor in which p
may hold (S ff \Gamma No(p)) should be excluded from No(EXp).
A[pUq] is computed recursively as follows: A[pUq] is True
in all states S 0 in which q holds; it is also True in predecessors
of S 0 in which p holds and all of which successors are
in S 0 . A[pUq] is False in a state s ff iff q does not hold in s ff
and either p does not hold in s ff or one of its successors does
not lead to q.
Implementation

Figure

4: Architecture of the Abstract Model Checker.
We have implemented our Abstract Model Checker (AMC)
as a 26,000-line C program. Figure 4 shows the architecture
Procedure CHECK(')
2.
Until
3. Return (Qm ,
2.
Until
3. Return (Qm ,

Figure

3: Model checking algorithm.
of our software. The CTL formulas and the input language
have been described in Sections 2 and 3, respectively. The

Abstract

Interpretor (AI) receives the program under analysis
and builds the Kripke structure K
using the process described in Section 3. This
structure, together with a set of CTL formulas, becomes the
input to the Model Checker which checks each property and
returns True if the formula holds in the program, False if the
formula does not hold, or Maybe if the validity of the formula
cannot be established. In the latter two cases, the model
checker also returns a counter-example. At the moment, the
counter-example facility includes just the line number and
the variable-value mappings of the states where the formula
is not True.
The AI receives a program and "interprets" it by starting
with an input context that consists of a set of values that variables
have before a program statement, executing the state-
ment, and producing an output context. The output context is
then stored as part of the state. The abstract values of finite-
domain variables (boolean or enumerated types) consist of
sets of (concrete) values these variables can attain, or UNDEF
(undefined) 1 . However, values of infinite-domain variables
such as integers should be abstracted further. In Section
2, we have briefly discussed how an abstraction function
ff can be applied to a set to get an interval. However, for bet-
1 For brevity, we do not discuss the treatment of UNDEF here. For details, please
refer to [11]
ter precision, we will associate each infinite-domain variable
with a (finite) set of intervals, with the following interpreta-
tion
In the current implementation of AI, each set can consist of
up to 5 intervals. We define ff
[ (union on the set of intervals)
below. Let a be intervals and assume, without a loss of
generality, that m - n:
fag
ff
fag
ff
ff
ff
ng
fag ff
When we encounter two sets, each containing more than one
interval, we first union elements of the set with less intervals
(in this case, fa 1 ; :::; amg) into one interval, and then union
the result with each interval of the other set. Interval operations
unionand difference have their usual meaning, and widening
on intervals is defined in Section 2. Other operations on
sets of intervals, ff
ff
r (widening) are similar.
Additional operations, including comparison and arithmetic,
are defined formally in [11].
The algorithm used in our AI for analyzing conditional
statements is depicted in Figure 5. Given an input abstract
statements to
execute when iexpr is True or False (stmt t and stmt f , respec-
tively), we either execute stmt t (stmt f ) based on S i and then
return the resulting abstract state, or call the Omega calculator
to get abstract states that correspond to taking the If and
the Else part (S i
t and S i
f , respectively), execute the state-
ments, and compute the union of the resulting output con-
texts. The Omega calculator is a set of C++ classes [21] for
manipulating integer tuple relations and sets described by Presburger
formulas. We use it for symbolically executing conditional
expressions involving intervals.
Procedure EVAL-IF
Evaluate iexpr
IF iexpr is True
Execute stmt t starting with S i to get S
Return S
ELSE IF iexpr is False
Execute stmt f starting with S i to get S
Return S
ELSE IF iexpr is Maybe
Call Omega calculator to get S i
f
Execute stmt t starting with S i t to get S
Execute stmt f starting with S i
f to get S
f
Return S
f

Figure

5: Algorithm for analyzing conditional statements.
For example, suppose we are running our AI on the program
fragment depicted in Figure 2 (Figure 6 shows the control-flow
graph for this fragment, with each state associated with
the program line number). Let the input context before executing
state 11 be ((xy; f[\Gamma20; 52]g); (a; f[\Gamma5; 8]g); (b; f[13;
2]g)). The condition xy == 0 evaluates to
Maybe; therefore, we call the Omega calculator to determine
that the value of xy in input contexts for states 12 and 14
should be f[0; 0]gand f[\Gamma20; \Gamma1]; [1; 52]g, respectively. The
values of b in output contexts of these states are f[5; 5]g and
f[26; 26]g; these are unioned to obtain f[5; 25]g in the input
context to state 15. The values of a after executing state 15
and state 16 are f[\Gamma3; \Gamma1]; [1; 8]gand f[\Gamma3; \Gamma1]; [1; 1]; [3; 3];
respectively. At this point, a has reached its
limit of five intervals, and further splitting cannot be done;
instead, we union a's intervals to get f[\Gamma3; 8]g and proceed
with the execution. This introduces a loss of information and
precision, but it is strictly conservative [11]. The outputvalue
for a after state 17 is f[\Gamma3; \Gamma3]; [\Gamma1; 8]g.
Loops are executed until a fixpoint on values of all variables
has been achieved. In order to ensure that this fixpoint
occurs in a finite number of steps, we change values of variables
in each loop at most 20 times, keeping track of whether
they decrease or increase between iterations. If a fixpoint was
not achieved, we widen values of non-converged variables,
with the increase and the decrease leading to the values of
+1 and \Gamma1, respectively. Afterwards, we proceed executing
the loop again to ensure that dependencies between the
variables are adequately captured. Table 1 lists several values
that variables b and xy attain in the input context to state
9 as we execute the main while loop of the program in Figure
2. At the first iteration, these values are f[13; 13]g and
\Gamma20]g, respectively. In the following19 iterations we
note that the maximum values b and xy can attain are in-
creasing, whereas their minimum values stay the same. Thus,
the widening which occurs on the 20th iteration changes only
the maximum values of these variables. The 21th iteration
does not bring any further changes, thus achieving a fixpoint.

Figure

7 shows the final Kripke structure built from the
control-flow graph of Figure 6. Each state is associated with
a line number of the statement that changes a global variable
in the original program, and withthe abstract values that global
variables have after the execution of this state. For example,
state 10 of Figure 7 is an aggregation of states 10 and 11 of

Figure

6.
int xy
int b
8:
10:
True 11:
xy == 0
14:
False
15:
a!=-2
True True
19:
print xy
int a
int c
7:
9:12:
20:
print b
True
False
False
False
3:
MAIN
END
True
False

Figure

Control-flow graph of the program in Figure 2.
iteration b xy

Table

1: Execution of the while loop of the program in Figure
2.
The resulting Kripke structure becomes input to the model
checker whose algorithm is described in Section 3. For ex-
Figure

7: Kripke structure K ff built from the program fragment
in Figure 2.
ample, we can model check the structure depicted in Figure 7
against CTL properties
and EF (b = 12). AMC returns False for the first property
because it is violated in state corresponding to line 12 of the
program. The second property is determined to be True because
it is satisfied in the state corresponding to line 12. The
third property is determined to be Maybe: it Maybe holds in
the state corresponding to line 14 and does not definitely hold
in any state.
4.1 Performance
Given a programPG, let jV j be the total number of variables,
global and local, and n be the number of statements in PG.
The worst case of the AI algorithm occurs when the program
has jV j loops, and each loop widens exactly one variable.
We go through each loop at most 20 times; therefore, each
statement in PG can be changed at most 20 \Theta jV j times, and
there are n \Theta 20 \Theta jV j changes altogether. Furthermore, every
state has at most predecessors. For each change of
state, we union abstract values of variables of all the prede-
cessors, which takes (n steps (m is a constant
proportional to the number of intervals associated with each
variable). Therefore, the entire computation of the abstract
interpretor takes 20 \Theta jV j \Theta n \Theta m \Theta (n \Gamma 1) \Theta jV j steps,
which is O(jV
To compute the performance of our model checker, we let
jP j be the length of a property P . Among all the CTL for-
mulas, A['U/] is the most complex. For this algorithm, Q i
can change value at most n times before a fixpoint is reached,
and it takes steps to compute Q i 's predecessors each
time. Verification of this property takes O(n \Theta (n \Gamma 1)) steps.
Therefore, the total running time for our model checker to
check a formula P is O(jP j \Theta n 2 ).
5 Case Study
To determine the effectiveness of our abstract model checker,
we analyzed the simplified version of a Safety-Injection System
[7]. Safety-Injection is an embedded system that monitors
the water pressure and injects the coolant into the reactor
core when the pressure falls below a certain threshold. There
is a manual control that the operator can use to prevent the
system from injecting the coolant, which causes the system to
be overridden. A reset switch prevents the system from being
overridden. The system inputs the value of the water pressure
and outputs a boolean condition signifying whether to
inject the coolant. In addition, it maintains the internal state
reflecting the water pressure. If the water pressure falls below
a threshold Low, the system's pressure level becomes too
low; if the water pressure raises above Permit, the system's
pressure level becomes high; otherwise, this level is "within
the permitted range".
We have implemented the Safety-Injectionsystem as a 200-
line C- program with 8 global variables closely reflecting those
of the specification: WaterPres of type integer, Block
and Reset of type boolean, Injection of type boolean,
Overridden of type boolean, constants Low, Permit,
TooLow, Permitted and High and Pressure of type
integer (our system does not allow enumerated types, and the
last three constants are used to indicate symbolic values of
Pressure). The implementation also includes 7 functions
and 8 local variables.
The specification language of our system is expressive enough
to capture complex properties of the Safety-Injectionsys-
tem, such as
1. AG((Reset - Pressure
2. AG((Reset -
3. AG((Block - :Reset - Pressure 6= High)
4. Permitted - WaterPres - Permit)
AX(WaterPres - Permit
For example, Property 2 states that the system will inject the
coolant if the pressure is too lowand the reset button is pressed,
whereas Property 4 states that whenever the pressure is permitted
and the water pressure raises above the allowed thresh-
old, then the system will eventually transit into a state where
the pressure is high.
We verified the above properties on Sun UltraSPARC-II
with 4 400 MHz processors and 4 GB of RAM. The entire
verification effort, includingbuildingthe abstract Kripke structure
and checking all the properties, took 3.92 seconds (user),
6.20 seconds (system). Our model-checker yielded True for
each of the four properties. The final Kripke structure consisted
of only abstract states.
Safety-Injection has been verified by two other research
groups. Bultan [2] built an infinite-state symbolic model checker
that uses binary decision diagrams (BDDs) and a system
of linear constraints to reason about models with Presburger
arithmetic. This model checker also uses the Omega
library together with abstract interpretation to achieve finite-time
convergence of the analysis, but the properties are verified
optimistically, allowing false positives. In addition, this
procedure is partial, with the convergence dependent on the
structure of the program and the formula to be verified. This
approach does not utilize abstraction for state-space reduc-
tion. Bultan verified Properties 1 and 2, and we were not able
to determine the exact size of his models. Bharadwaj and
Heitmeyer [1] analyzed SCR specifications using the SPIN
[15] model checker. Their technique only allows finite-domain
variables, including integer subranges and enumerated types.
The size of the concrete state space is reduced by two meth-
ods: eliminating variables which are not relevant to the property
being verified (SCR ensures that dependencies between
variables form a partial order), and by replacing input variables
by predicates. The latter approach makes the verification
conservative, allowing false negatives. The unabstracted
system for Properties 1 and 2 (SPIN performs on-the-fly ver-
ification, without building a complete state space) consists of
over 1.7 million states, whereas the combination of the above
abstractions brings the state space down to 650 states.
6 Summary and Future Work
In this paper we proposed a framework for step-wise automatic
verification and described an implementation of a very
cheap and not particularly precise model checker. This model
checker verifies infinite-state sequential programs written in
a subset of C against CTL formulas containing arithmetic op-
erations. It applies property-independent abstract interpretation
to create an abstract Kripke structure, and then uses
this extremely compact structure to verify properties in low-order
polynomial time. No user-created abstractions are nec-
essary. The verification always converges and is guaranteed
to be sound: if the model checker yields True, the property
holds in the concrete system, and if it yields False, the property
does not hold. This approach is not limited to the analysis
of programs; it can be applied to finite-state and infinite-
state specifications equally well. We also believe that tightening
up the code of our model checker and making the state
encoding symbolic will further improve its running time.
However, the results of our work are limited in several
ways:
(1) The implementation of the tool cannot handle complex
constructs of the input language. These include recur-
sion, user-defined data types, dynamic memory allocation,
pointers, etc. We also currently limit our verification to sequential
programs.
(2) Our tool interacts with the Omega library, which can
only handle operations on integer-valued variables. Thus, reasoning
about floating-pointnumbers is currently not supported.
(3) There is only one built-inlevel of abstraction provided
in our system.
(4) The input language, being a subset of C, does not have
formal semantics; in particular, the notion of a state transition
is poorly-defined. We chose to associate a state with values
of global variables, and a state transition with changes of
values of global variables. Perhaps a more flexible way to
determine the granularity of state transitions is more appropriate

(5) Our model checker returns Maybe if it cannot determine
whether a property holds in the system. We believe we
can reduce the number of cases for which the verification is
inconclusive by improving the reasoning about abstract values
and/or by choosing property-specific abstractions.
In short-term future work we hope to extend our model-checker
to reasoning about CTL   [5] which combines branching-time
and linear-time operations and is strictly more expressive
than CTL. We would also like to address the issue
of state granularity. We can do so by either asking users to
specify which global variables constitute a "state" or to add
language constructs for explicitly stating the beginning and
the end of each state, either via begin-state/end-state or via
adding the notion of time (time-tick), where each state occurs
between consecutive time-ticks.

Acknowledgments

We would like to thank Ric Hehner and Radu Iosif for reading
earlier versions of this paper, and Mark Pichora, Albert
Yu and Daniel House for many interesting discussions. We
acknowledge the financial support of NSERC Postgraduate
Scholarship.


Appendix


In this section, we give proofs of correctness of algorithms
for checking A['U/]. See [11] for proofs of correctness of
other algorithms. Let (AM
s ff )) indicate that our model checker returns True (False) when
checking a formula OE in state s ff of the abstract model M ff .
Assume:
where M , s are the model and the state of the concrete pro-
gram, respectively. The above expressions state that our model
checker is sound with respect to Yes and No answers for ' and
/. Prove:
1.
2. (AM
1.
The proof is by induction on the length of the path from
s ff to a state in which / holds.
IH: Let T be the set of states from which can be reached
in ! n steps. Assume 8t ff
PROVE: The formula holds for paths of length - n.
We will not consider the case where AM
because it is covered by the base case.
2. (AM
A['U/] does not hold in state s ff if either (1) / does not occur
on some path emanating from s ff , or (2) on some path
emanating from s ff , before the first occurrence of /, there is
a state in which ' does not hold.
The algorithm can be expanded as follows:
Case (1):
Until
Case
Case (1) starts from the set of states where :/ is true and recursively
intersects it with those states that have successors in
which :/ holds. The result is the set of states that can never
reach /, i.e. M; s
(2) results in the set of states in which neither ' nor / hold,
i.e. M; s



--R

"Model Checking Complete Requirements Specifications Using Abstrac- tion"
"Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach"
"Symbolic Model Checking of Infinite State Programs Using Presburger Arithmetic"
"Decoupling Synchronization from Local Control for Efficient Symbolic Model Checking of StateCharts"
"Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications"
"Model Checkingand Abstraction"
"Documentation for Safety Critical Software"
"Static Determination of Dynamic Properties of Programs"
"Abstract Interpretation of Reactive Systems"
"The MurOE Verification System"
Analyzing infinite-state programs with abstract interpretation
"Model Checking Graphical User Interfaces Using Abstractions"
"VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software"
"Model Checking Java Programs Using Java Pathfinder"
"The Model Checker SPIN"
"A Practical Method for Verifying Event-Driven Software"
"Abstract Model Checking of Infinite Spec- ifications"
"Lightweight Formal Meth- ods"
"Model Checking for Managers"
"Validation of Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin"
"The Omega Calculator and Library"
Symbolic Model Checking.
"An Abstract Dynamic Semantics for C"
"Automatic Abstraction techniques for Propositional -calculus Model Check- ing"
"Feasibility of Model Checking Software Requirements: A Case Study"
--TR

--CTR
Steve Easterbrook , Marsha Chechik , Benet Devereux , Arie Gurfinkel , Albert Lai , Victor Petrovykh , Anya Tafliovich , Christopher Thompson-Walsh, Chek: a model checker for multi-valued reasoning, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Marsha Chechik , Benet Devereux , Steve Easterbrook , Arie Gurfinkel, Multi-valued symbolic model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.12 n.4, p.371-408, October
program analysis;CTL;abstract interpretation;model checking