Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Internal and External Logics of Abstract Interpretations
verfasst von : David A. Schmidt
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We show that every abstract interpretation possesses an
internal logic
, whose proof theory is defined by the partial ordering on the abstract domain’s elements and whose model theory is defined by the domain’s concretization function. We explain how program validation and transformation depend on this logic.
Next, when a logic
external
to the abstract interpretation is imposed, we show how to synthesize a sound, underapproximating, set-based variant of the external logic and give conditions when the underapproximating logic can be embedded within the original abstract domain,
inverted
. We show how model-checking logics depend on this construction.
The intent of this paper is tutorial, to integrate little-publicized results into a standard framework that can be used by practitioners of static analysis.