2007 | OriginalPaper | Buchkapitel
Logical Interpretation: Static Program Analysis Using Theorem Proving
verfasst von : Ashish Tiwari, Sumit Gulwani
Erschienen in: Automated Deduction – CADE-21
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
This paper presents the foundations for using automated deduction technology in static program analysis. The central principle is the use of
logical lattices
– a class of lattices defined on logical formulas in a logical theory – in an abstract interpretation framework. Abstract interpretation over logical lattices, called
logical interpretation
, raises new challenges for theorem proving. We present an overview of some of the existing results in the field of logical interpretation and outline some requirements for building expressive and scalable logical interpreters.