Advertisement
Published in:
2006 | OriginalPaper | Chapter
Comparing Completeness Properties of Static Analyses and Their Logics
Author : David A. Schmidt
Published in: Programming Languages and Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.