Assertion Checking over Combined Abstraction of Linear Arithmetic and Uninterpreted Functions
This paper presents results on the problem of checking equality assertions in
programs whose expressions have been abstracted using combination
of linear arithmetic and uninterpreted functions, and whose
conditionals are treated as non-deterministic.
We first show that the problem of assertion checking for this combined abstraction is
coNP-hard, even for loop-free programs. This result is quite
surprising since assertion checking for the individual
abstractions of linear arithmetic and uninterpreted functions
can be performed efficiently in polynomial time.
Next, we give an assertion checking algorithm for this combined
abstraction, thereby proving decidability of this problem despite the
underlying lattice having infinite height. Our algorithm is based on an important connection
between unification theory and program analysis.
we show that
weakest preconditions can be strengthened by replacing equalities
by their unifiers, without losing any precision, during backward analysis