Logical Interpretation: Static Program Analysis Using Theorem Proving

Ashish Tiwari and Sumit Gulwani

Presented at CADE-21, July 2007.

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.

The first author was supported in part by the National Science Foundation under grant ITR-CCR-0326540.

pdf.

Slides

Slides of the presentation at CADE'07 may be put up here later ...

BibTeX Entry


@inproceedings{TTKLL07:AB,
	author = "A.~Tiwari and S. Gulwani",
	title = "Logical Interpretation: {S}tatic Program Analysis Using Theorem Proving",
	booktitle = "CADE-21",
    editor = "F. Pfenning",
    series = {LNAI},
    volume = 4603,
    pages = "147--166",
    year = 2007,
    publisher = "Springer",
}
Return to the Ashish's home page
Return to the Computer Science Laboratory home page