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.