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.