Type
Text
Type
Dissertation
Advisor
Stark, Eugene W. | Scott D. Stoller | Aarti Gupta. | Grosu, Radu
Date
2010-08-01
Keywords
Computer Science | automata, Binary Decision Diagrams, Horn clauses, program analysis, set-at-a-time evaluation
Department
Department of Computer Science
Language
en_US
Source
This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree.
Identifier
http://hdl.handle.net/11401/72673
Publisher
The Graduate School, Stony Brook University: Stony Brook, NY.
Format
application/pdf
Abstract
Logic programming languages have been widely used to express program analyses. In this dissertation, we present a framework of program analysis using Horn clauses and Binary Decision Diagrams (BDDs). In contrast to previous work of Whaley, et al. that used Datalog and BDDs for program analysis, we use Horn clauses (which can be viewed as an extension of Datalog) to express program analysis problems. Horn clauses are more expressive than Datalog by allowing functions as arguments of predicates. Many type-based program analysis problems involve type information in which the type is usually a recursively defined object consisting of subtypes. The use of function symbols makes it possible to specify a type in a natural way.BDDs are very popular tool in hardware verification and model checking. Recently, BDDs have also been used in program analysis to efficiently analyze large programs. Unlike Datalog, Horn clauses cannot be implemented by using ordinary BDDs due to the presence of functions. In this dissertation, we propose an automata-based approach that treats terms as strings reading from left to right and represents terms by automata. We devise various operations on automata to manipulate terms. Moreover, we show that such automata lend themselves readily to a representation using Multi-Terminal Binary Decision Diagrams (MTBDDs).We present a top-down set-at-a-time depth-first evaluation algorithm for Horn clauses in terms of sets of ground atoms. Such evaluation algorithm computes relevant results starting from the query in a top-down fashion, operates over a set of atoms at a time, and gains efficiency by taking the advantage of symbolic representation of sets of ground atoms in Horn clauses.The combination of the above ideas yields a framework for program analysis such that analysis queries are naturally expressed as Horn clauses and the evaluation of Horn clauses is efficiently implemented by MTBDDs. Such a framework is suitable for type-based program analysis, such as strictness analysis, binding-time analysis, secure information flow analysis, and so on.
Recommended Citation
Song, Wenxin, "Using Horn Clauses and Binary Decision Diagrams for Program Analysis" (2010). Stony Brook Theses and Dissertations Collection, 2006-2020 (closed to submissions). 1876.
https://commons.library.stonybrook.edu/stony-brook-theses-and-dissertations-collection/1876