Data Abstraction: Our presentation for data abstraction follows the abstract interpretation framework (Cousot and Cousot 1999). Abstract interpretation establishes a rigorous methodology for building data abstractions that are weakly preserving with respect to safety properties. In this framework, an abstraction maps the set of values of a program data type to an abstract domain and it maps the operations on that data type to functions over abstract values. Thus, the abstract program has a non-standard execution. Typically, the behaviors of the abstracted program are an over-approximation of the behaviors of the original program; each executable behavior in the original program is “covered” by a behavior in the abstract program. Thus, the abstraction is weakly preserving. When the abstract behaviors are checked with a model checker against a safety property (or a property written in LTL) and found to be in conformance, we can be sure that the true executable behaviors of the unabstracted program satisfy the property.