Most critical applications, such as airplane and rocket controllers, need correctness guarantees. Usually these correctness guarantees can be described as safety properties in the form of assertions. Verifying an assertion amounts to showing that the assertion holds true for all possible runs of an application. Abstract interpretation is a method to automatically verify a program by soundly abstracting the concrete executions of the program to elements in an abstract domain, and checking the correctness guarantees using the abstraction. However, traditional abstract domains treat the machine integers as mathematical integers. As a result, the conclusions drawn from such an abstract interpretation are, in general, unsound. In other words, the assertions shown to be true by traditional abstract interpretation approaches might actually be false because the underlying point space does not faithfully model bit-vector arithmetic.

This dissertation advances the field of abstract interpretation by providing sound abstraction techniques and abstract-domain frameworks that faithfully model bit-vector semantics. We focus on numerical abstract domains for bitvectors, which can provide equality and inequality invariants.

The first part of the dissertation focuses on abstract domains capable of expressing bit-vector-sound equality invariants. The performance and precision of two equality domains is compared, and sound inter-conversion methods are provided. Furthermore, we generalize one of the equality domains to develop a new abstract-domain framework that is capable of expressing a certain class of disjunctions over bit-vector-sound equality constraints. This framework can be instantiated with any relational or non-relational base abstract domain over bitvectors.

The second part of the dissertation focuses on abstract domains capable of expressing bit-vector-sound inequality invariants. We develop an abstract domain that is capable of expressing a certain class of bit-vector-sound inequalities over memory variables and registers. Furthermore, we develop an abstract-domain framework that takes an abstract domain that is sound with respect to mathematical integers, and creates an abstract domain whose operations and abstract transformers are sound with respect to machine integers.

(Click here to access the paper: PDF.)