SHF: Medium: Gradual Verification

软件对社会来说变得越来越重要，然而我们使用的应用程序仍然受到错误（bug）的困扰，从不方便到严重的安全威胁。验证是一种很有前途的消除软件缺陷的新技术。但是验证也是非常昂贵的——它的成本可能是常规软件开发的10倍，使得验证太昂贵而无法完全应用于所有软件。这个项目的新奇之处是建立在逐步验证的基础上的，这样它就可以应用于软件系统的一部分，而不是全部。项目的影响是基于允许工程师将验证工作集中在应用程序最重要的部分，以及消除导致最大问题的错误。这可以以相对较小的成本增加来消除软件应用中最严重的漏洞。该项目还将通过为学生提供学习这一主题的更顺畅的途径来加强核查教学，并将采取具体步骤扩大代表性不足的群体对计算的参与。该项目的技术方法建立在最近关于抽象渐进类型的工作之上：一种原则性的方法，它应用抽象解释的思想，系统地将静态类型系统调整为允许静态类型和动态类型混合的系统。我们建议调整这种方法，使验证渐进式。在渐进式验证设置中，开发人员可以选择为程序中的关键功能指定可能的部分前置和后置条件规范，而不指定其他功能和属性。渐进式验证者将使用抽象解释来静态地识别规范和代码之间的不一致，但不会因为规范缺失或不完整而触发错误警告。它还将插入最小的运行时检查，这些检查是强制执行静态验证器无法保证的任何属性所必需的。目前正在通过形成性质的研究、形式化和证明、原型实施和绩效评价、总结性用户研究和案例研究来验证这种方法。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Software is becoming ever more essential to society, yet the apps we use continue to be plagued by errors (bugs) that range from inconveniences to severe security threats. Verification is a promising new technology for eliminating bugs from software. But verification is also very expensive--it may cost 10 times the amount of regular software development, making verification way too expensive to fully apply to all software. The project's novelties are based on making verification gradual, so that it can be applied to just part of a software system, not all of it. The project's impacts are based on allowing engineers to focus verification efforts on the most important parts of applications, and on eliminating the bugs that cause the biggest problems. This could eliminate the most severe bugs from software apps with a relatively small increase in cost. The project will also enhance the teaching of verification by providing students with a smoother path to learning the topic, and will take specific steps towards broadening the participation of underrepresented groups in computing. The project's technical approach builds on recent work on abstracting gradual typing: a principled approach that that applies ideas from abstract interpretation to systematically adapt a static type system into one that allows static and dynamic types to be mixed. We proposed to adapt this approach to make verification gradual. In the gradual verification setting, developers can choose to specify possibly partial pre- and post-condition specifications for the critical functions in a program, while leaving other functions and properties unspecified. The gradual verifier will use abstract interpretation to statically identify inconsistencies between specifications and code, but without triggering false warnings due to specifications that are missing or incomplete. It will also insert the minimum run-time checks that are necessary in order to enforce any properties that the static verifier cannot assure. The approach is being validated through a combination of formative qualitative studies, formalization and proof, prototype implementation and performance evaluation, and summative user studies and case studies.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.