Cover Algorithms and their Combination
Abstract
This paper defines coverT(V,F) (also called the cover
of formula F with respect to a set of variables V in theory T
to be the strongest quantifier-free formula that is implied by
\exists(V): F in theory T. Cover exists for several useful
theories, including those that do not admit quantifier elimination.
This paper describes cover algorithms for the theories of
uninterpreted functions and linear arithmetic. In addition, the paper
provides a combination algorithm to combine the cover operations for
theories that satisfy some general condition. This paper motivates
the study of cover by describing its applications in program analysis
and verification techniques, like symbolic model checking and abstract
interpretation.