Memory demand optimization of fixpoint algorithm for PHP analysis
|Thesis title in Czech:||Optimalizace paměťové náročnosti fixpoint algoritmu pro analýzu PHP|
|Thesis title in English:||Memory demand optimization of fixpoint algorithm for PHP analysis|
|Academic year of topic announcement:||2017/2018|
|Type of assignment:||diploma thesis|
|Department:||Department of Distributed and Dependable Systems (32-KDSS)|
|Supervisor:||RNDr. Jan Kofroň, Ph.D.|
|Static analysis of programs is a common technique to verify software properties. It is can be tuned to be either fast or precise, but not both. Since the imprecision in terms of a high number of false-positive warnings makes it impossible to be used in the development process, the time and memory demands of the analyser have to be lowered by means of efficient algorithms and optimizations.
The goal of the thesis is to design and implement an optimization of the fixpoint computation exploiting the fact that it is sufficient to store the program state just for one program point for each cycle. The states of other cycle points can be computed on demand (when needed in subsequent phases of the analysis), which can even save some time. The implementation context is the PHP analysis framework .
| Framework pro analýzu PHP: http://d3s.mff.cuni.cz/projects/formal_methods/weverca/
 F. Nielson et al.: Principles of Program Analysis, Springer, 1999
 PHP: http://php.net