Modeling and verification of web software based on theories symbolic computation

作为Web软件验证的案例，我们验证了WebEos的核心。利用Mathematica上的一些计算结果进行了有效的验证。针对基于字符串分析的验证，我们开发了精确分析正则表达式匹配的方法。通过引入对数据库通信的分析，我们实现了存储型XSS的检测。我们设计并实现了一种基于位置自动机的贪婪正则表达式匹配算法。

As a case study of Web software verification, we have verified the core of WebEos. The effective verification was conducted by utilizing some results of the computation conducted on Mathematica. With respect to the verification based on string analysis, we developed the method to precisely analyze regular expression matching. By introducing the analysis of communication to database, we enabled the detection of stored XSS. We designed and implemented an algorithm of greedy regular expression matching based on position automata.