Thesis (Selection of subject)Thesis (Selection of subject)(version: 285)
Assignment details
   Login via CAS
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
Thesis language: angličtina
Department: Department of Distributed and Dependable Systems (32-KDSS)
Supervisor: RNDr. Jan Kofroň, Ph.D.
Author:
Guidelines
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 [1].
References
[1] Framework pro analýzu PHP: http://d3s.mff.cuni.cz/projects/formal_methods/weverca/
[2] F. Nielson et al.: Principles of Program Analysis, Springer, 1999
[3] PHP: http://php.net
 
Charles University | Information system of Charles University | http://www.cuni.cz/UKEN-329.html