| dc.identifier.uri | http://hdl.handle.net/1951/55629 | |
| dc.identifier.uri | http://hdl.handle.net/11401/72673 | |
| dc.description.sponsorship | This work is sponsored by the Stony Brook University Graduate School in compliance with the requirements for completion of degree. | en_US |
| dc.format | Monograph | |
| dc.format.medium | Electronic Resource | en_US |
| dc.language.iso | en_US | |
| dc.publisher | The Graduate School, Stony Brook University: Stony Brook, NY. | |
| dc.type | Dissertation | |
| dcterms.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. | |
| dcterms.available | 2012-05-15T18:06:54Z | |
| dcterms.available | 2015-04-24T14:53:11Z | |
| dcterms.contributor | Stark, Eugene W. | en_US |
| dcterms.contributor | Scott D. Stoller | en_US |
| dcterms.contributor | Aarti Gupta. | en_US |
| dcterms.contributor | Grosu, Radu | en_US |
| dcterms.creator | Song, Wenxin | |
| dcterms.dateAccepted | 2012-05-15T18:06:54Z | |
| dcterms.dateAccepted | 2015-04-24T14:53:11Z | |
| dcterms.dateSubmitted | 2012-05-15T18:06:54Z | |
| dcterms.dateSubmitted | 2015-04-24T14:53:11Z | |
| dcterms.description | Department of Computer Science | en_US |
| dcterms.format | Monograph | |
| dcterms.format | Application/PDF | en_US |
| dcterms.identifier | Song_grad.sunysb_0771E_10260.pdf | en_US |
| dcterms.identifier | http://hdl.handle.net/1951/55629 | |
| dcterms.identifier | http://hdl.handle.net/11401/72673 | |
| dcterms.issued | 2010-08-01 | |
| dcterms.language | en_US | |
| dcterms.provenance | Made available in DSpace on 2012-05-15T18:06:54Z (GMT). No. of bitstreams: 1
Song_grad.sunysb_0771E_10260.pdf: 1367067 bytes, checksum: bfc0d2ea79709df74963198d61c6c76c (MD5)
Previous issue date: 1 | en |
| dcterms.provenance | Made available in DSpace on 2015-04-24T14:53:11Z (GMT). No. of bitstreams: 3
Song_grad.sunysb_0771E_10260.pdf.jpg: 1894 bytes, checksum: a6009c46e6ec8251b348085684cba80d (MD5)
Song_grad.sunysb_0771E_10260.pdf.txt: 254722 bytes, checksum: 483c02d0086a74e107ff2f3575757eb4 (MD5)
Song_grad.sunysb_0771E_10260.pdf: 1367067 bytes, checksum: bfc0d2ea79709df74963198d61c6c76c (MD5)
Previous issue date: 1 | en |
| dcterms.publisher | The Graduate School, Stony Brook University: Stony Brook, NY. | |
| dcterms.subject | automata, Binary Decision Diagrams, Horn clauses, program analysis, set-at-a-time evaluation | |
| dcterms.subject | Computer Science | |
| dcterms.title | Using Horn Clauses and Binary Decision Diagrams for Program Analysis | |
| dcterms.type | Dissertation | |
