Beta 1

Title Using the succinet solver to implement flow logic specifications of classical data flow analysis
Author Gao, Han (Computer Science and Engineering, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Master's thesis
Year 2004
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.
Note Supervised by Prof. Hanne Riis Nielson
Keywords Program analysis; Succinct Solver; Alternation-free Least Fixpoint Logic; Flow Logic; Data Flow Analysis; Framework
Original PDF imm3258.pdf (0.60 MB)
Admin Creation date: 2006-06-22    Update date: 2007-09-11    Source: dtu    ID: 154751    Original MXD