Using the succinet solver to implement flow logic specifications of classical data flow analysis | Han Gao
| | Abstract | Program analysis is a long-history-studied field, which is used to determine properties of programs at compile time without actually executing them. Traditionally, program analysis has been developed and used to optimize compilers and programs in order to get better performance, but recent development shows a promising and much wider application area including validating security properties of Java programs and communication protocols.
A relatively new term in program analysis field is Flow Logic, which concerns about specifying which criteria an analysis estimate should satisfy in order to be acceptable for a program. More important, it separates the specification of an acceptable estimate from the actual computation of the analysis information.
In this thesis, we concern about using flow logic to solve some data flow questions. In particular, we show that data flow analysis can be expressed in term of flow logic. In order to be thoroughly, both bit-vector analyses and monotone analyses are considered. As a comparison, we implement bit-vector analyses in data flow approach, thus paving the way to evaluate the relative advantage of both approaches. This evaluation is based on the execution times of Succinct Solver running on constraints generated for certain scalable benchmarks. The result is encouraging that, flow logic approach is degrees of complexity polynomial better than data flow approach, as far as the analyses presented in this thesis are concerned. As a conclusion, we give some strategies for specifying flow logic specifications for classical data flow analyses. Furthermore, The correctness and expressiveness of Succinct Solver are examined as well. | | Keywords | Program analysis, Succinct Solver, Alternation-free Least Fixpoint Logic, Flow Logic, Data Flow Analysis, Framework | | Type | Master's thesis [Academic thesis] | | Year | 2004 | | Publisher | Informatics and Mathematical Modelling, Technical University of Denmark, DTU | | Address | Richard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby | | Series | IMM-Thesis-2004-53 | | Note | Supervised by Prof. Hanne Riis Nielson | | Electronic version(s) | [pdf] | | BibTeX data | [bibtex] | | IMM Group(s) | Computer Science & Engineering |
|