Static analyses calculate abstract states, and their logics validate properties of the abstract states. We place into perspective the variety of forwards, backwards, functional, and logical completeness used in abstract-interpretation-based static analysis by giving examples and by proving equivalences, implications, and independences. We expose two fundamental Galois connections that underlie the logics for static analyses and reveal a new completeness variant, O-completeness. We also show that the key concept underlying logical completeness is covering, which we use to relate the various forms of completeness. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Schmidt, D. A. (2006). Comparing completeness properties of static analyses and their logics. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4279 LNCS, pp. 183–199). Springer Verlag. https://doi.org/10.1007/11924661_12
Mendeley helps you to discover research relevant for your work.