zbMATH — the first resource for mathematics

Comparing completeness properties of static analyses and their logics. (English) Zbl 1168.68364
Kobayashi, Naoki (ed.), Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8–10, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48937-5/pbk). Lecture Notes in Computer Science 4279, 183-199 (2006).
Summary: 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.
For the entire collection see [Zbl 1133.68007].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
Full Text: DOI