There has been a surge of progress in automated verification methods based
on state exploration. In areas like hardware design, these technologies are
rapidly augmenting key phases of testing and validation. To date, one of t
he most successful of these methods has been symbolic model-checking, in wh
ich large finite-state machines are encoded into compact data structures su
ch as Binary Decision Diagrams (BDDs), and are then checked for safety and
liveness properties. However, these techniques have not realized the same s
uccess on software systems. One Limitation is their inability to deal with
infinite-state programs, even those with a single unbounded integer. A seco
nd problem is that of finding efficient representations for various variabl
e types. We recently proposed a model-checker for integer-based systems tha
t uses arithmetic constraints as the underlying state representation. While
this approach easily verified some subtle, infinite-state concurrency prob
lems, it proved inefficient in its treatment of boolean and (unordered) enu
merated types-which are not efficiently representable using arithmetic cons
traints. In this article we present a new technique that combines the stren
gths of both BDD and arithmetic constraint representations. Our composite m
odel merges multiple type-specific symbolic representations in a single mod
el-checker. A system's transitions and fixpoint computations are encoded us
ing both BDD (for boolean and enumerated types) and arithmetic constraint (
for integers) representations, where the choice depends on the variable typ
es. Our composite model-checking strategy can be extended to other symbolic
representations provided that they support operations such as intersection
, union, complement, equivalence checking, and relational image computation
. We also present conservative approximation techniques for composite repre
sentations to address the undecidability of model-checking on infinite-stat
e systems. We demonstrate the effectiveness of our approach by analyzing tw
o example software specifications which include a mixture of booleans, inte
gers, and enumerated types. One of them is a requirements specification for
the control software of a nuclear reactor's cooling system, and the other
one is a transport protocol specification.