Translation Validation: From Signal to C - Correct System Design: Recent Insights and Advances - page 239

variables (e.g. if there are n integer/float variables, then each of these variables

ranges over [1 ]). It is not dicult to see that this range is sucient for proving

the invalidity of a formula if it was originally not valid. The invalidity of the
formula implies that there is at least one assignment that makes the formula
false. Any assignment that preserves the partitioning of the variables in this
falsifying assignment will also falsify the formula (the absolute values are of no
importance). This is why the [1

::n

::n

] range, which allows all possible partitions, is
sucient regardless of the formula's structure.

5.2 Range Allocation

The size of the state-space imposed by the [1 ::n ] range as suggested in the pre-

n . For most industrial-size programs this state-space is far too
big to handle. But apparently there is a lot of redundancy in this range that
can be avoided. The [1

vious section is n

] range is given without any analysis of the formula's
structure. Note that our informal justication of the soundness of this method
is independent of the structure of the formula we try to validate, and thus the
range is sucient for all formulas with

::n

variables. This is probably the best we
can do when the only information we have about the formula is that it has

n

n
variables. However, a more detailed analysis of the structure of the formula we
wish to validate makes it possible to signicantly decrease the ranges, and con-
sequently the state space can be drastically reduced. This analysis is performed
by the 'Range Allocation' module, using the range allocation algorithm , which
signicantly reduces the range of each of these (now enumerated type) variables,
and enables the handling of larger programs. By applying the range-allocation
technique, CVT decreases the state space of the veried formulas typically by
orders of magnitude. We have many examples of formulas containing 150 integer
variables or more (which result in a state-space of 150 150

] range is
taken) which. after performing the range allocation algorithm, can be proved
with a state-space of less than 100, in less than a second.
The range allocation algorithm is somewhat complex and its full description
is beyond the scope of this paper. We refer the reader to [17] for more details,
and describe here only the general idea.
The algorithm attempts to solve a satisability (validity) problem eciently,
by determining a range allocation

if the [1 ::n

R : Vars ( ' ) 7! 2 N , mapping each integer

variable x i 2 ' into a small nite set of integers, such that ' is satisable

(valid) i it is satisable (respectively, valid) over some R -interpretation. After

each variable x i is encoded as an enumerated type over its nite domain R ( x i ),

we use a standard bdd package, such as the one in TLV (see Section 5.5), to

construct a B ' is not identical to 0.

Obviously, the success of our method depends on our ability to nd range
allocations with a small state-space.
In theory, there always exists a singleton range allocation

bdd B ' . Formula ' is satisable i

R , satisfying the

R allocates each variable a domain consisting of a above requirements, such that

jR j single integer, i.e., = 1. This is supported by the following trivial argument: