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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Tiwari, A., & Gulwani, S. (2007). Logical interpretation: Static program analysis using theorem proving. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4603 LNAI, pp. 147–166). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_11
Mendeley helps you to discover research relevant for your work.