EAGER: Collaborative Research: Leveraging Graph Databases for Incremental and Scalable Symbolic Analysis and Verification of Web Applications

现代人类社会对Web应用的依赖程度很高，并且深受其低可靠性的影响。不幸的是，无论在软件的验证和确认上投入多少努力，现有的技术本身都是有限的，软件发布时经常会出现错误和问题，这些缺陷和问题限制了软件的功能，并会极大地影响用户体验。这个项目研究了一种方法，该方法有可能显著提高符号程序分析和验证技术的可伸缩性和有效性，从而提高现代Web应用程序的可靠性。这个项目开发的技术和工具使用符号执行和基于自动机的验证技术来自动分析和验证Web应用程序，并将符号分析的结果存储在图形数据库中，以便有效地存储和检索。该方法使用增量和差异分析策略，利用图形数据库，以提高软件分析和验证的可扩展性和有效性。该项目培训研究生，并将向其他研究人员和教育工作者公开提供其文物。

Modern human society relies heavily on web applications and is deeply affected by their poor dependability. Unfortunately, no matter how much effort is put into verification and validation of software, existing techniques are inherently limited, and software is routinely released with bugs and issues that limit its functionality and can dramatically affect the user experience. This project investigates an approach that has the potential to significantly improve the scalability and effectiveness of symbolic program analysis and verification techniques, that will improve the dependability of modern web applications,. This project develops techniques and tools that use symbolic execution and automata-based verification techniques to automatically analyze and verify web applications, and store results of symbolic analyses in a graph database for efficient storage, and retrieval. The methods use incremental and differential analysis strategies that utilize the graph database in order to improve scalability and effectiveness of software analysis and verification. The project trains graduate students, and will make its artifacts publicly available to other researchers and educators.