Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Cover Algorithms and their Combination

Sumit Gulwani and Madanlal Musuvathi

Abstract

This paper defines the cover of formula φ with respect to a set of variables V in theory T to be the most precise quantifier-free formula that is implied by ∃Vφ in theory T. Cover exists for several useful theories, including those that do not admit quantifier elimination. This paper describes cover algorithms for theories of uninterpreted functions, linear arithmetic, lists, and arrays. 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.

Details

Publication typeTechReport
NumberMSR-TR-2006-09
Pages18
InstitutionMicrosoft Research
> Publications > Cover Algorithms and their Combination