SHF: Small: Collaborative Research: Online Verification-Validation

SHF：小型：协作研究：在线验证-确认

基本信息

批准号：
1619282
负责人：
Bor-Yuh Evan Chang
金额：
$ 31万
依托单位：
University of Colorado at Boulder
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2016
资助国家：
美国
起止时间：
2016-09-01 至 2020-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1619282&HistoricalAwards=false
关键词：
SHF Small Collaborative Research Online

项目摘要

Increasingly, modern software on the web is richly extensible, accelerating its evolution and dramatically reducing the time between development and deployment. The intellectual merit of this research consists of challenging the false choice between creating software that is extensible (easy to reuse and extend) and software that is correct (meets its specifications). The new approach advanced by this work, Incremental Verification-Validation, enables programmers to bring domain-specific safely disciplines to extensible systems, by providing a framework where these disciplines are communicated both precisely and usefully, as executable code. The project's broader significance and importance consist in changing the way programmers approach building correct extensible software for the web. The research targets ECMAScript (JavaScript), enabling this research to have a direct impact on the vast number of languages and systems that create and use JavaScript. Further, the project represents a new collaboration across the University of Colorado and University of Maryland, bringing together experts across verification, incremental computing, and runtime systems. Finally, this project benefits the graduate and undergraduate teaching mission at the participating universities, as aspects of the project enriches the program analysis and programming language courses.Incremental Verification-Validation encourages programmers to co-design their systems with executable specifications that check these systems dynamically, as they execute. Moreover, unlike typical assertions, which execute dynamically and non-incrementally, the proposed are subject to novel patterns that enhance their performance: In regressive validation, verification partially discharges some checks, dynamically rewriting the program with residual versions; in progressive verification, online verification occurs in passes that each cache and reuse work, to avoid from-scratch verification of facts that still hold from earlier passes. Finally, to avoid forcing analysis programmers to reason about incremental changes explicitly in each analysis that they create, the meta layer expresses incremental computations implicitly, using an implicitly-incremental meta language whose abstractions hide reasoning on a per-change basis.

网络上的现代软件越来越多，可以加速其演变，并大大减少开发和部署之间的时间。这项研究的智力优点包括在创建可扩展的软件（易于重复使用和扩展）和正确的软件（符合其规格）之间挑战错误的选择。这项工作提出的新方法是增量验证验证，使程序员能够通过提供一个框架来将这些学科精确且有用的框架作为可执行代码传达，从而将特定于领域的安全学科带到可扩展的系统中。该项目的更广泛的意义和重要性在于改变程序员接近为Web构建正确的可扩展软件的方式。该研究针对Ecmascript（JavaScript），使这项研究能够直接影响创建和使用JavaScript的大量语言和系统。此外，该项目代表了科罗拉多大学和马里兰州大学的新合作，将专家汇总到验证，增量计算和运行时系统中。最后，该项目使参与大学的研究生和本科教学任务受益，因为该项目的各个方面都丰富了程序分析和编程语言课程。进行验证验证鼓励程序员通过执行这些系统的可执行规范来协调他们的系统，从而在执行时会动态地检查这些系统。此外，与典型的断言（动态执行和非核心执行）不同，所提出的要受到增强其性能的新模式的约束：在回归验证中，验证部分放电一些检查，用残留版本动态地重写程序；在逐步验证中，在线验证发生在每个缓存和重用工作的通行证中，以避免从较早的通行证中遇到的事实进行从划痕验证。最后，为避免强迫分析程序员在他们创建的每个分析中明确推理增量变化，使用隐式元素的元语言，元层隐含地表达了增量计算，其抽象的抽象在每次变化的基础上隐藏了推理。