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

EAGER：协作研究：利用图形数据库进行增量和可扩展的 Web 应用程序符号分析和验证

• 批准号: 1549161
• 负责人: Corina Pasareanu
• 金额: $ 5万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-09-01 至 2019-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1549161&HistoricalAwards=false
• 关键词: EAGER; Collaborative; Research; Leveraging; Graph

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.

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