karelklic
commented
11 years ago Efficient chaotic iteration
Canal is a static analysis tool designed to analyze behaviour of application programs written in C. It is based on the theoretical framework of abstract interpretation, with focus on the scalability to large programs and proper handling of real-world source code.
Currently, Canal implements a basic chaotic iteration to compute the program analysis: the iterative strategy is used to compute the fixed point and head of every program basic block is used as a widening point. The iterative strategy causes unnecessary abstract operations to be performed in already-stabilized parts of the program, and this significantly extends the time of the analysis. Using the head of every basic block as a widening point causes large memory requirements as the abstract state is stored at every widening point.
The goal of this thesis is to implement a recursive strategy of chaotic iteration, based on components created by a weak topological ordering of the program dependency graph. Heads of components should be used as the widening points to reduce the memory requirement of the analysis.
Our current algorithm is slow and takes much more memory than needed. This is an interesting topic for a bachelor or master thesis.