A framework for combining analysis and verification.
We present a general framework for combining program verification and program analysis. This framework enhances program analysis because it takes advantage of user assertions, and it enhances program verification because assertions can be refined using automatic program analysis. Both enhancements in general produce a better way of reasoning about programs than using verification techniques alone or analysis techniques alone. More importantly, the combination is better than simply running the verification and analysis in isolation and then combining the results at the last step. In other words, our framework explores synergistic interaction between verification and analysis. In this paper, we start with a representation of a program, user assertions, and a given analyzer for the program. The framework we describe induces an algorithm which exploits the assertions and the analyzer to produce a generally more accurate analysis. Further, it has some important features:  it is flexible: any number of assertions can be used anywhere; it is open: it can employ an arbitrary analyzer; it is modular: we reason with conditional correctness of assertions; it is incremental: it can be tuned for the accuracy/efficiency tradeoff.
Introduction
abstraction [9] is a successful method of abstract
interpretation. The abstract domain, constructed from
a given finite set of predicates over program variables, is
intuitive and easily, though not necessarily efficiently, computable
within a traversal method of the program's control
flow structure. More recently, the success of predicate abstraction
has been enhanced by a process of discovery of the
[copyright notice will appear here]
abstract domain, generally known as CEGAR or "counterex-
ample guided abstraction refinement".
One major disadvantage of predicate abstraction, as is
true for many other realizations of abstract interpretation, is
that in principle, the process of abstraction is performed at
every step of the traversal phase. Indeed, the survey section
in [19] states that "abstractions are often defined over small
parts of the program", and that "abstractions for model-checking
often over-approximate".
While it is generally easy to optimize somewhat by performing
abstraction here and there (eg: several consecutive
asignments may be compressed and abstraction performed
according one composite assignment, such as in the BLAST
system [11]), there has not been a systematic way of doing
this. Another disadvantage, arising partly because the abstract
description is limited to a fixed number of variables,
is that this ad-hoc method would not be compositional. For
example, [2] required an elaborate extension of predicate abstraction
which essentially considers a second set of variables
(called "symbolic constants"), in order to describe the
behaviour of a function, in the language of predicate abstrac-
tion. This provided a limited form of compositionality.
In this paper, we present a general proof method of program
reasoning based on predicate abstraction in which the
process of abstraction is intermittent, that is, approximation
is performed only at selected program points, if at all. There
is no restriction of when abstraction is performed, even
though termination issues will usually restrict the choices.
The key advantages are that (a) the abstract domain required
to ensure convergence of the algorithm can be minimized,
and (b) the cost of performing abstractions, now being inter-
mittent, is reduced.
For example, to reason that executing x :=
one needs to know that
the final assignment. Also, consider proving for the
following program snippet:
#1# while (i < n) do
A textbook Hoare-style loop invariant for the loop is
2i. Having this proposition in predicate abstraction would,
however, not suffice; one in fact needs to know that
holds in between the two increments to c. Thus in general, a
proper loop invariant is useful only if we could propagate its
information exactly.
A main challenge to having exact propagation is that reasoning
will be required about the strongest-postcondition operator
associated with an arbitrarily long program fragment.
This essentially means dealing with constraints over an unbounded
number of variables describing the states between
the start and end of the program fragment at hand. The advantages
in terms of efficiency, however, are significant: less
predicates needed in the abstract domain, and also, less frequent
execution of the abstraction operation.
An important additional feature of our proof method is
that it is compositional. We represent a proof as a Hoare-style
triple which, for a given program fragment, relates the
input values of the variables to the output values. This is represented
as a formula, and in general, such a formula must
contain auxiliary variables in addition to the program vari-
ables. This is because it is generally impossible to represent
the projection of a formula using a predefined set of vari-
ables, or equivalently, it is not possible to perform quantifier
elimination. Consequently, in order to have unrestricted
composition of such proofs, it is (again) necessary to deal
with an unbounded number of variables.
The latter part of this paper will introduce the technology
of Constraint Logic Programming (CLP) as a basis for efficient
implementation. Briefly, the advantages of CLP are (a)
handles terms containing anonynous primary variables and
constraints on these variables and also an arbitrary number
of auxiliary variables, (b) efficiently represents the projection
of such terms, and (c) handles backtracking.
In summary, we show that our method provides a flexible
combination of abstraction and Hoare-style reasoning with
predicate transformers and loop-invariants, that is composi-
tional, and that its practical implementation is feasible.
1.1 Further Related Work
An important category of tools that use program verification
technology have been developed within the framework of
the Java Modelling Language (JML) project. JML allows
to specify a Java method's pre- and post-conditions, and
class invariants. Examples of such program verification tools
are: Jack [4], ESC/Java2 [7], and Krakatoa [15]. All these
tools employ weakest precondition/strongest postcondition
calculi to generate proof obligations which reflect whether
the given post-conditions and class invariants hold at the
end of a method, whenever the corresponding pre-conditions
are valid at the procedure's entry point. The resulting proof
obligations are subsequently discharged by theorem provers
such as Simplify [7], Coq [3], PVS [17], or HOL light [10].
While these systems perform exact propagation, they depend
on user-provided loop invariants, as opposed to an abstract
domain.
Recently there have emerged systems based on abstract
interpretation, and in particular, on predicate abstraction.
Some examples are BLAST [11], SLAM [1], MAGIC [5],
and Murphi- [8], amongst others. While abstract interpretation
is central, these systems employ a further technique of
automatically determining the abstract domain needed for
a given assertion. This technique is called CEGAR, see eg.
the description in [6], based on an iteratively refining the abstract
domain from the failure of the abstract domain in the
previous iteration. These systems do not perform exact propagation
in a systematic way.
2. Preliminaries
Apart from a program counter k, whose values are program
points, let there be n system variables -
domains respectively. In this paper, we shall
use just two example domains, that of integers, and that of
integer arrays. We assume the number of system variables is
larger than the number of variables required by any program
fragment or procedure.
DEFINITION 1 (States and Transitions). A system state (or
simply state) is of the form (k,d 1 , - , d n ) where pc is a
program point and d i # D i , 1 # i # n, are values for the
system variables. A transition is a pair of states.
In what follows, we define a language of first-order for-
mulas. Let V denote an infinite set of variables, each of
which has a type in D 1 , - , D n , let S denote a set of func-
tors, and P denote a set of constraint symbols. A term
is either a constant (0-ary functor) in S or of the form
and each t i is a term,
primitive constraint is of the form f(t 1 , -
where f is a m-ary constraint symbol and each t i is a term,
A constraint is constructed from primitive constraints
using logical connectives in the usual manner. Where Y is a
constraint, we write Y( -
X) to denote that Y possibly refers to
variables in -
X , and we write -
X) to denote the existential
closure of Y( -
away from -
X .
An substitution is a mapping which simultaneously replaces
each variable in a term or constraint into some ex-
pression. Where e is a term or constraint, we write eq to
denote the result of applying q to e. A special kind of substitution
is a renaming, which maps each variable in a given
sequence, say -
into the corresponding variable in another
given sequence, say -
Y . We write [ -
Y ] to denote such a
mapping.
Another special kind of substitution is a grounding of an
this maps each variable in the expression into a
value in its respective domain. Thus the effect of applying a
grounding substitution q to an expression e is to obtain a set
eq of its ground instances under q. We write to denote
the set of all possible groundings of e.
3. Constraint Transition Systems
A key concept is that a program fragment p operates on a
sequence of anonymous variables, each corresponding to a
system variable at various points in the computation of p.
In particular, we consider two sequences -
n of anonymous variables to denote the system
values before executing p and at the "target" point(s) of p,
respectively. Typically, but not always, the target point is the
terminal point of p. Our proof obligation or assertion is then
of the form
where Y and Y 1 are constraints over the said variables, and
possibly including new variables. Like the Hoare-triple, this
states that if p is executed in a state satisfying Y, then all
states at the target points (if any) satisfy Y 1 . Note that, unlike
the Hoare-triple, p may be nonterminating and Y 1 may refer
to the states of a point that is reached infinitely often. We
will formalize all this below.
For example, let there be just one system variable x, let
p be <0> x let the target point be <1>.
meaning p is the successor
function on x. Similarly, if p were the (perpetual) program
<0> while (true) x
if <1> were the target point, then {true}p{x
that is, any state (1,x) at point <1> satisfies #z(x
This shows, amongst other things, that the parity of x always
remains unchanged.
Our proof method accomodates concurrent programs of a
fixed number of processes. Where we have n processes, we
shall use as a program point, a sequence of n program points
so that the i th program point is one which comes from the i th
process,
We next represent the program fragment p as a transition
system which can be executed symbolically. The following
definition serves two main purposes. First, it is a high
level representation of the operational semantics of p, and in
fact, it represents the exact trace semantics of p. Second, it
is an executable specification against which an assertion can
be checked.
DEFINITION 2 (Constraint Transition System). A constraint
transition of p is a formula
where k and k 1 are variables over program points, each of
x and -
x 1 is a sequence of variables representing a system
even(5,
even(5,

Figure

1. Even counts
Process 1:
while (true) do
Process 2:
while (true) do

Figure

2. Two Process Bakery

Figure

3. CTS of Two Process Bakery
state, and Y is a constraint over -
x and -
possibly some
additional auxiliary variables.
A constraint transition system (CTS) of p is a finite set of
constraint transitions of p.
Consider for example the program in Section 1; call it
even.

Figure

1 contains a CTS for even.
Consider another example: the Bakery algorithm with
two processes in Figure 2. A CTS for this program, call it
bak, is given in Figure 3. Note that we use the first and
second arguments of the term bub to denote the program
points of the first and second process respectively.
Clearly the variables in a constraint transition may be re-named
freely because their scope is local to the transition.
We thus say that a constraint transition is a variant of another
if one is identical to the other when a renaming subsitution is
performed. Further, we may simplify a constraint transition
by renaming any one of its variables x by an expression y
provided that all groundings of the constraint tran-
sition. For example, we may simply state the last constraint
transition in Figure 3 into
by replacing the variable y 1 in the original transition with 0.
The above formulation of program transitions is familiar
in the literature for the purpose of defining a set of transi-
tions. What is new, however, is how we use a CTS to define
a symbolic transition sequences, and thereon, the notion of a
proof.
By similarity with logic programming, we use the term
goal to deonote a literal that can be subjected to an unfolding
process in order to infer a logical consequence.
DEFINITION 3 (Goal). A query or goal of a CTS is of the
where k is a program point, Y is a sequence of variables
over system states, and Y is a constraint over some or all
of the variables -
x, and possibly some additional variables.
The variables -
x are called the primary variables of this goal,
while any additional variable in Y is called an auxiliary
variable of the goal.
Thus a goal is just like the conclusion of a constraint
transition. We say the goal is a start goal if k is the start
program point. Similarly, a goal is a target goal is k is the
target program point. Running a start goal is tantamount to
asking the question: which values of -
x which satisfy -
will lead to a goal at the target point(s)? The idea is that we
successively reduce one goal to another until the resulting
goal is at a target point, and then inspect the results.
Next we define it means for a CTS to prove a goal.
DEFINITION 4 (Proof Step, Sequence and Tree). Let there
be a CTS for p, and let
x),Y be a goal for this. A
proof step from G is obtained via a variant p(k, -
of a transition in the CTS in which all the variables are fresh.
The result is a goal G # of the form
y, Y 1
providing the constraints Y, -
y, Y 1 are satisfiable.
A proof sequence is a finite or infinite sequence of proof
steps. A proof tree is defined from proof sequences in the
obvious way. A tree is complete if every internal node representing
a goal G is succeeded by nodes representing every
goal obtainable in a proof step from G .

Figure

5. Proof Tree of Even Counts Program
Consider again the CTS in Figure 1, and we wish to prove
There is in fact only one proof sequence
from the start goal
or equivalently, even(0, i, 1,0). This proof sequence is shown
in

Figure

5, and note that the counter,represented in the last
goal by the variable c 2 , has the value 2.
Hereafter we shall consider that a program and its CTS
are synonymous. Given a program p, we say that
x are the
start variables of p to denote that -
x are the variables in the
first constraint transition of p.
DEFINITION 5 (Assertion). Let p be a program with start
variables -
x, and let Y be a constraint. Let -
x t denotes a sequence
of variables representing system states not appearing
in p or Y. (These represent the target values of the system
An assertion for p wrt to -
x t is of the form
In particular, when k is the start program point, we may
abberviate the assertion using the notation:
It is intuitively clear what it means for an assertion to
hold. That is, execution from every instance q of p(k, -
cannot lead to a target state where the property Y 1 ( -
violated.
In the example above, we could prove the assertion
it is understood that the final
variable c t corresponds to the start variable c. Note that the
last occurrence of n in the assertion means that we are comparing
c t with the initial and not final value of n (though in
this example, the two are in fact the same).
We now state the essential property of proof sequences:
THEOREM 1. Let a CTS for p have the start point k and target
x and -
x 1 each be sequences of variables

Figure

4. Proof Tree of 2-Process Bakery Algorithm (Partially Shown)
over system states. The assertion {Y( -
holds if for any goal of the form p(k t , -
appearing
in a proof sequence from the goal p(k, -
x), the following
holds:
The above theorem provides the basis of a search method,
and what remains is to provide a means to ensure termination
of the search. Toward this end, we next define the concepts
of subsumption and coinduction and which allow the
(successful) termination of proof sequences. However, these
are generally insufficient. In the next section, we present our
version of abstraction whose purpose is to transform a proof
sequence so that it is applicable to the termination criteria of
subsumption and coinduction.
3.1 Subsumption
Consider a finite and complete proof tree from some start
goal. A goal G in the tree is subsumed if there is a different
path in the tree containing a goal G # such that [[G
The principle here is simply memoization: one may terminate
the expansion of a proof sequence while constructing
a proof tree when encountering a subsumed goal.
3.2 Coinduction
The principle here is that, within one proof sequence, the
proof obligation associated with the final goal may assume
that the proof obligation of an ancestor goal has already
been met. This can be formally explained as a principle of
coinduction (see eg: Appendix B of [16]). Importantly, this
simple form of coinduction does not require a base case nor
a well-founded ordering.
We shall simply demonstrate this principle by example.
Suppose we had the transition p(0,x) # p(0,x #
and we wished to prove the assertion p(0,x) |= even(x t
-x),
that is, the difference between x and its final value is even.
Consider the derivation step:
We may use, in the latter goal, the fact that the earlier goal
satisfies the assertion. That is, we may reduce the obligaton
of the latter goal to
It is now a simple matter of inferring whether this formula
holds.
In general practice, the application of coinduction testing
is largely equivalent to testing if one goal is simply an instance
of another.
3.3 Compostionality
It is intuitively clear that since our proof obligation relates
the start and final values of a program, or equivalently, it
obeys the "assume-guarantee" paradigm [18], that the proof
method is sequentially compositional. We thus omit a formal
treatment of CTS where programs directly invoke other
programs. Instead, in the next section, we provide a simple
example.
4. Abstraction
In the literature on predicate abstraction, the abstract description
is a specialized data structure (monomial?), and
the abstraction operation serves to propagate such a structure
though a small program fragment (a contiguous group
of assignments, or a test), and then obtaining another struc-
ture. The strength of this method is in the simplicity of using
a finite set of predicates over the fixed number of program
variables as a basis for the abstract description.
We choose to follow this method. However, our abstract
description shall not be a distinguished data structure. In
our abstract description of a goal is itself a goal.
DEFINITION 6 (Abstraction). An abstraction A is applied
to a goal. It is specified by a program point pc(A), a sequence
of variables var(A) corresponding to a subset of
the system variables, and finally, a finite set of constraints
pred(A) over var(A), called the "predicates" of A .
Let A be an abstraction and G be a goal p(k, -
x),Y where
x denote the subsequence of -
x corresponding
to the system variables var(A). Let -
x denote the remaining
subsequence of -
x. Without losing generality, we assume
that -
x 1 is an initial subsequence of -
x, that is, -
x.
Then the abstraction A(G) of G by A is:
Z is a sequence of fresh variables renaming -
Y 2 is the finite set of constraints
For example, let A be such that
and That is, the first variable
is to be abstracted into a negative or a nonnegative value.
Let G be p(0, [x 1 , x 2 , x 3 ]), x 1. Then the abstraction
A(G) is a goal of the form p(0, [Z,x 2 , x 3 ]), x
which can be simplified into p(0, [Z,x 2 , x 3 ]), x
Note that the orginal goal had ground instances
p(0, [1, 1,n]) for all n, while the abstracted goal has the instances
p(0, [m,1,n]) for all n and all nonnegative m. Note
that the second variable x 2 has not been abstracted even
though it is tightly constrained to the first variable x 1 . Note
further that the value of x 3 is unchanged, that is, the abstraction
would allow any constraint on x 3 , had the example goal
contained such a constraint, to be propagated.
LEMMA 1. Let A be an abstraction and G a goal.
The critical point is that the abstraction of a goal has the
same format as the goal itself. Thus an abstract goal has the
expressive power of a regular goal, while yet containing a
notion of abstraction that is sufficient to produce a finite-state
effect. Once again, this is facilitated by the ability to
reason about an unbounded number of variables.
Consider the "Bubble" program and its CTS in Figures
7 and 8, which is a simplified skeleton of the bubble sort
algorithm (without arrays). Consider the subprogram corresponding
to start point 2 and whose target point is 6, that is,
we are considering the inner loop. Further suppose that the
following assertion had already been proven:
bub(2, i, j, t, n) |=
that is, the subprogram increments t by n - preserving
both i and n, but not j. Consider now a proof sequence
for the goal bub(0, i, j, t, n),n # 0, where we want to
prove that at program point #8#,
n)/2. The proof
tree is depicted in Figure 6. The proof shows a combination
of the use of intermittent abstraction and compositional
proof:
. At point (A), we abstract the goal bub(2,
using the predicates i <
i)/2. Call this abstraction A . Here the set
of variables is hence both the variables
correspond respectively to system variables
#1# while (i < n-1) do
#3# while (j < n-i-1) do

Figure

7. Program "Bubble"
bub(0, i, j, t, n) # bub(1,
bub(1, i, j, t, n) # bub(8, i, j, t, n), i # n-1.
bub(1, i, j, t, n) # bub(2, i, j, t, n), i < n-1.
bub(2, i, j, t, n) # bub(3,
bub(3, i, j, t, n) # bub(6, i, j, t, n), j # n- i -1.
bub(3, i, j, t, n) # bub(4, i, j, t, n), j < n- i -1.
bub(4, i, j, t, n) # bub(5,
bub(5, i, j, t, n) # bub(6, i, j, t, n), j # n- i -1.
bub(5, i, j, t, n) # bub(4, i, j, t, n), j < n- i -1.
bub(6, i, j, t, n) # bub(7,
bub(7, i, j, t, n) # bub(8, i, j, t, n), i # n-1.
bub(7, i, j, t, n) # bub(2, i, j, t, n), i < n-1.

Figure

8. CTS of "Bubble"
and t are renamed to fresh variables i 2 , and t 2 . Mean-
while, the variables j and n retain their original values.
. After performing the above abstraction, we reuse the
proof of the inner loop above. Here we immediately move
to program point #6#, incrementing t with
updating j to an unknown value. However, i and n retain
their original values at #2#.
. As the result of the intermittent abstraction above, we
obtain a coinductive proof at (B).
5. The Whole Algorithm
We now summarize our proof method for an assertion
Suppose the start program point of p is k and the start
variables of p are -
x. Then consider the start goal p(k, -
and incrementally build a search tree. For each path in the
tree constructed so far leading to a goal G :
. if G is either subsumed or is coinductive, then consider
this path closed, ie: not to be expanded further;
. if G is a goal on which an abstraction A is defined,
replace G by A(G);
. if G is a target goal, and if the constraints on the primary
variables -
x 1 in G do not satisfy Yq, where q renames the
target variables in Y into -
Coinduction using (A)
Satisfies
Satisfies
Proof composition
Intermittent abstraction
bub(0, i, j, t, n),n # 0

Figure

6. Compositional Proof
THEOREM 2. If the above algorithm, applied to the assertion
then the asertion holds.
6. CLP Technology
It is almost immediate that CTS is implementable in CLP.
Given a CTS for p, we build a CLP program in the following
way: (a) for every transition of the form (k, -
we use the CLP rule the clause p(k, -
ing that Y is in the constraint domain of the CLP implementation
at hand); (b) for every terminal program point k, we
use the CLP fact p(k, , . , , ), where the number of anonymous
variables is the same as the number of variables in -
x.
We see later that the key implementation challenge for
a CLP system is the incremental satisfiability problem.
Roughly stated, this is the problem of successively determining
that a monotonically increasing sequence of constraints
(interpreted as a conjunction) is satisfiable.
6.1 Exact Propagation is "CLP-Hard"
Here we informally demonstrate that the incremental satisfiability
problem is reducible to the problem of analyzing
a straight line path in a program. We will consider here
constraints in the form of linear diophantine equations, i.e.,
multivariate polynomials over the integers. Without loss of
generality, we assume each constraint is written in the form
is an integer.
Suppose we already have a sequence of constraints
corresponding path in the program's control
flow.
Suppose we add a new constraint Y
Then, if one of these variables, say Y , is new, we add the
assignment y := x - z where y is a new variable created to
correspond to y. The remaining variables x and z are each
either new, or are the corresponding variable to x and Z. If
however all of x,Y and Z are not new, then add the statement
if are the program
variables corresponding to x, y, z respectively. Hereafter we
pursue the then branch of this if statement.
Similarly, suppose the new constraint were of the form
y correspond to Y , and y is possibly new. Again,
if x is new, we simply add the assignment x := n # y where
x is newly created to correspond to x. Otherwise, add the
statement if . to the path, and again, we
now pursue the then branch of this if statement.
Clearly an exact analysis of the path we have constructed
leading to a successful traversal required, incrementally, the
solving of the constraint sequence Y 0 , - , Y n .
6.2 Key Elements of CLP Systems
A CLP system attempts to find answers to an initial goal G
by searching for valid substitutions of its variables. Depth-first
search is used. Each path in the search tree in fact
involves the solving of an incremental satisfiability problem.
Along the way, unsatisfiability of the constraints at hand
would entail backtracking.
The key issue in CLP is the incremental satisfiability
problem, as mentioned above. A standard approach is as
follows. Given that the sequence of constraints Y 0 , . , Y i
has been determined to be satisfiable, represent this fact
in a solved form. Essentially, this means that when a new
constraint Y i+1 is encountered, the solved form is efficiently
combinable with Y i+1 in order to determine the satisfiability
of the new conjunction of constraints.
This method essentially requires a representation of the
projection of a set of constraints onto certain variables. Con-
sider, for example, the set x
Assuming that the new constraint would
only involve the variable x i (and this happens vastly of-
ten), we desire a representation of x projection
problem is well studied in CLP systems [13]. In the system
CLP(R ) [14] for example, various adaptations of the
Fourier-Motzkin algorithm were implemented for projection
in Herbrand and linear arithmetic constraints.
We finally mention another important optimization in
CLP: tail recursion. This technique uses the same space in
the procedure call stack for recursive calls. Amongst other
bebefits, this technique allows for a potentially unbounded
number of recursive calls. Tail recursion is particurly relevant
in our context because the recursive calls arising from
the CTS of programs are often tail-recursive.
The CLP(R ) system that we use to implement our prototype
has been engineered to handle constraints and auxiliary
variables efficiently using the above techniques.
7. Experiments
We performed two kinds of experiments: the first set performs
exact propagation. We then look at comparable abstract
runs in the BLAST system, and (exact) runs in the
system. These results are presented in Section
7.1.
In the second set of experiments, presented in Section 7.2,
we compare intermittent predicate abstraction with normal
predicate abstraction, again against the BLAST system.
We used a Pentium 4 2.8 GHz system with 512 MBRAM
running GNU/Linux 2.4.22.
7.1 Exact Runs
We start with an experiment which shows that concrete execution
can potentially be less costly than abstract execution,
we simply compare the timing of concrete execution using
our CLP-based implementation and a predicate abstraction-based
model checker. We also run a simple looping program,
whose C code is shown in Figure 9. We first have BLAST
generate all the 100 predicates it requires. We then re-run
BLAST by providing these predicates. BLAST took 22.06
seconds to explore the state space. On the same machine, and
without any abstraction, our verification engine took only
seconds. For comparison, SPIN model checker [12] executes
the same program written in PROMELA in less than
seconds.
Now consider the synthetic program consisting of an initial
assignment x := 0 followed by 1000 increments to x,
with the objective of proving that 1000 at the end. Consider
also another version where the program contains only
a single loop which increments is counter x 1000 times. We
input these two programs to our program verifier, without
using abstraction, and to ESC/Java 2 as well. The results are
shown in Table 1. For both our verifier and ESC/Java 2 we
run both with x initialized to 0 and not initialized, hopefully
forcing symbolic execution.

Table

1 shows that our verifier runs faster for the non-looping
version. However, there is a noticeable slowdown in
int main()
{ int i=0, j, x=0;
while (i<7) {
while (j<7) { x++; j++; }
{ ERROR: }

Figure

9. Program with Loop
Time (in Seconds)
CLP with Tabling ESC/Java 2
Non-Looping 2.45 2.47 9.89 9.68
Looping 22.05 21.95 1.00 1.00

Table

1. Timing Comparison with ESC/Java 2
the looping version for our implementation. This is caused
by the fact that in our implementation of coinductive tabling,
subsumption check is done based on similarity of program
point. Therefore, when a program point inside a loop is visited
for the i-th time, there are i - 1 subsumption checks to
be performed. This results in a total of about 500,000 subsumption
checks for the looping program. In comparison,
the non-looping version requires only 1,000 subsumption
checks. However, our implementation is currently at a prototype
stage and our tabling mechanism is not implemented in
the most efficient way. For the looping version, ESC/Java 2
employs a weakest precondition propagation calculus; since
the program is very small, with a straightforward invariant
(just the loop condition), the computation is very fast. Table
also shows that there is almost no difference between
having x initialized to 0 or not.
7.2 Experiments Using Abstraction
Next we show an example that demonstrates that the intermittent
approach requires fewer predicates. Let us consider
a second looping program written in C, shown in Figure 10.
The program's postcondition can be proven by providing an
invariant x=i # i<50 exactly before the first statement of
the loop body of the outer while loop. We specify as an abstraction
domain the following predicates x=i, i<50, and respectively
their negations x#=i, i#50 for that program point
to our verifier. Using this information, the proof process finishes
in less than 0.01 seconds. If we do not provide an abstract
domain, the verification process finishes in 20.34 sec-
onds. Here intermittent predicate abstraction requires fewer
predicates: We also run the same program with BLAST and
provide the predicates x=i and i<50 (BLAST would auto-
int main()
{ int i=0, j, x=0;
while (i<50) {
while (j<10) { x++; j++; }
while (x>i) { x-; }
{ ERROR: }

Figure

10. Second Program with Loop
while (true) do

Figure

11. Bakery Algorithm Peudocode for Process i
matically also consider their negations). BLAST finishes in
1.33 seconds, and in addition, it also produces 23 other predicates
through refinements. Running it again with all these
predicates given, BLAST finishes in 0.28 seconds.
Further, we also tried our proof method on a version
of bakery mutual exclusion algorithm. We need abstraction
since the bakery algorithm is an infinite-state program. The
pseudocode for process i is shown in Figure 11. Here we
would like to verify mutual exclusion, that is, no two processes
are in the critical section (program point #2#) at the
same time. Our version of bakery algorithm is a concurrent
program with asynchronous composition of processes. It can
be encoded as a sequential program with nondeterministic
choice.
We first encode the algorithm for 2, 3 and 4 processes
in BLAST. Nondeterministic choice can be implemented in
BLAST using the special variable BLAST NONDET which
has a nondeterministic value. We show the BLAST code for
2-process bakery algorithm in Figure 12. Within the code,
we use program point annotations #pc# which should be considered
as comments. Notice that the program points of the
concurrent version are encoded using the integer variables
pc1 and pc2.
Further, we translate the BLAST sequential versions of
the algorithm for 2, 3 and 4 processes into the CTS version
shown in Figure 13 and also its corresponding CLP code, as
an input to our prototype verifier.
In our experiments, we attempt to verify mutual exclusion
property, that is, no two processes can be in the critical section
at the same time. Here we perform 3 sets of runs, each
consisting of runs with 2, 3 and 4 processes. In all 3 sets,
we use a basic set of predicates: x i =0, x i #0, pc i =0, pc i =1,
int main()
{
#0# int pc1=0, pc2=0;
unsigned int x1=0, x2=0;
#1# while (1) {
#2# if (pc1==1 || pc2==1) {
#3# /* Abstraction point 1 */; }
#4# if (pc1==0 || pc2==0) {
#5# /* Abstraction point 2 */;
else if (pc1==2 && pc2==2) {#6# ERROR: }
#7# if ( BLAST NONDET) {
#8# if (pc1==0) {
else if (pc1==1 &&
{
else if (pc1==2) {
} else {
#12# if (pc2==0) {
else if (pc2==1 &&
{
else if (pc2==2) {

Figure

12. Sequential 2-Process Bakery
and N the number of processes,
and also their negations.
. Set 1: Use of predicate abstraction at every state with
full predicate set. Here using our prototype system we
perform ordinary predicate abstraction where we abstract
at every state encountered during search. Here, in addition
to the basic predicates, we also require the predicates
shown in Table 2 (and their negations) to avoid producing
spurious counterexample.
. Set 2: Intermittent predicate abstraction with full
predicate set. In the second set we use intermittent abstraction
technique on our prototype implementation. We
abstract only when for some process i, pc i =1 holds. In

Figure

12, this abstraction point is marked with the comment
"Abstraction point 1." The set of predicates that we
use here is the same as the predicates that we use in the
first experiment above, otherwise spurious counterexample
will be generated.
. Set 3: Intermittent predicate abstraction with reduced
predicate set. For the third set we also use intermittent
abstraction technique on our tabled CLP system.
Here we only abstract whenever there are N-1 processes
at program point 0, which in the 2-process sequential version
is the condition where either pc1=0 or pc2=0. This is
bak(3, pc1, pc2,x1,x2) # bak(4, pc1, pc2,x1,x2).
bak(5, pc1, pc2,x1,x2) # bak(7, pc1, pc2,x1,x2).
2.
bak(6, pc1, pc2,x1,x2) # bak(7, pc1, pc2,x1,x2).
bak(7, pc1, pc2,x1,x2) # bak(8, pc1, pc2,x1,x2).
bak(7, pc1, pc2,x1,x2) # bak(12, pc1, pc2,x1,x2).
2.
2.
2.
2.

Figure

13. CTS of Sequential 2-Process Bakery
Bakery-2 x1<x2
Bakery-3 x1<x2, x1<x3, x2<x3
Bakery-4 x1<x2, x1<x3, x1<x4
x2<x3, x2<x4, x3<x4

Table

2. Additional Predicates
Time (in Seconds)
CLP with Tabling BLAST
Bakery-3 0.83 0.14 0.09 2.38
Bakery-4 131.11 8.85 5.02 78.47

Table

3. Timing Comparison with BLAST
marked with the comment "Astraction point 2" in Figure
12.
For each bakery algorithm with N processes, here we
only need the basic predicates and their negations without
the additional predicates shown in Table 2.
We have also compared our results with BLAST. We supplied
the same set of predicates that we used in the first and
second sets to BLAST. Again, in BLAST we do not have to
specify their negations explicitly. Interestingly, for 4-process
bakery algortihm BLAST requires even more predicates to
avoid refinement, which are x1=x3+1, x2=x3+1, x1=x2+1,
1#x4, x1#x3, x2#x3 and x1#x2. We suspect this is due to
the fact that precision in predicate abstraction-based state-space
traversal depends on the power of the underlying theorem
prover. We have BLAST generate these additional predicates
it needs in a pre-run, and then run BLAST using them.
Here since we do not run BLAST with refinement, lazy abstraction
technique [11] has no effect, and BLAST uses all
the supplied predicates to represent any abstract state.
For these problems, using our intermittent abstraction
with CLP tabling is also markedly faster than both full predicate
abstraction with CLP and BLAST. We show our timing
results in Table 3 (smallest recorded time of 3 runs each).
The first set and BLAST both run with abstraction at
every visited state. The timing difference between them and
second and third sets shows that performing abstraction at
every visited state is expensive. The third set shows further
gain over the second when we understand some intricacies
of the system.

Acknowledgement

We thank Ranjit Jhala for his help with BLAST.



--R

Automatic predicate abstraction of C programs.
Polymorphic predicate abstraction.
The Coq proof assistant reference manual-version v6
Java applet correctness: A developer-oriented approach
Modular verification of software components in C.

ESC/Java2: Uniting ESC/Java and JML.
Experience with predicate abstraction.
Construction of abstract state graphs of infinite systems with PVS.
HOL light: A tutorial introduction.
Lazy ab- straction
The SPIN Model Checker: Primer and Reference Manual.
Projecting CLP(R
The CLP(R
The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML.
Principles of Program Analysis.
PVS: A prototype verification system.
A proof technique for rely/guarantee properties.
Model checking programs.
--TR
Constraint logic programming
Methods and logics for proving programs
based program analysis
Modern compiler implementation in ML
Simplification by Cooperating Decision Procedures
Abstract interpretation
Systematic design of program analysis frameworks
A flexible approach to interprocedural data flow analysis and programs with recursive data structures
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
Program Analysis Using Mixed Term and Set Constraints
Experiments in Theorem Proving and Model Checking for Protocol Verification
Powerful Techniques for the Automatic Generation of Invariants
Verifying Invariants Using theorem Proving
PVS
program analysis;program verification;abstract interpretation