An efficient abstract domain for the approximation of machine integers

Software verification is essential for building reliable systems, but it requires well-crafted tools whose development is a non-trivial task. This thesis presents an abstract domain based on multi-intervals for the approximation of machine integers and arithmetic, logic and bitwise operations over them. The C++ implementation of the abstract domain has been carefully engineered for maximum efficiency, both in terms of memory occupation and of execution time. The applications of this abstract domain range from static analysis, to symbolic model-checking, to constraint-based generation of test cases