This paper defines the cover of a formula φ with respect to a set of variables V in theory T to be the strongest quantifier-free formula that is implied by 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 combination algorithm can be used to compute the cover a formula in the combined theory of uninterpreted functions and linear arithmetic. This paper motivates the study of cover by describing its applications in program analysis and verification techniques, like symbolic model checking and abstract interpretation. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Gulwani, S., & Musuvathi, M. (2008). Cover algorithms and their combination. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4960 LNCS, pp. 193–207). https://doi.org/10.1007/978-3-540-78739-6_16
Mendeley helps you to discover research relevant for your work.