| 研究実績の概要 |
The general objective of this research is to develop formal verification techniques and tools, based on especially model checking techniques, to ensure the safety and security of web applications.
In 2015, our main efforts are devoted to the following tasks:
1) Elaborate a sliding-window incremental algorithm for weighted pushdown systems (WPDSs), so as to enhance the practical efficiency of program analysis algorithms encoded based on WPDSs. We have implemented and evaluated the new algorithm with Java points-to analysis. Our empirical study shows that the sliding-window algorithm always outperforms the whole program analysis. The work is under submission, and we plan to make our tool open source to the community after publishing the work.
2) Elaborate a new backward/forward saturation algorithm for reachability problem of subclasses of conditional pushdown systems (CPDSs) that obey certain patterns. It gives rise to alternative solutions to reachability analysis of the existing applications using CPDSs, such as reachability analysis of HTML5 parser specifications, stack inspection, etc. We found that the backward saturation algorithm could be further optimized for the sake of practical scalability. We are looking into the optimization and planning an empirical study based on it.
|
