Logical Interpretation: Static Program Analysis Using Theorem Proving

Abstract. 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.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Ashish Tiwari, Sumit Gulwani
• Keywords: Automated Reasoning, CADE 2007, Logical Interpretation, Logical Lattices, Scalable Logical Interpreters