CAREER: Gradual Verification: From Scripting to Proving

该项目提供了理论、工具和教学框架，以缩小日常编程任务中广泛使用的编程语言与少数提供强大正确性保证的验证集成语言之间的差距。受到编程语言研究的两个重要趋势（即渐进类型和定理证明语言）的启发，这项工作综合了两者的各个方面，以实现从脚本语言到验证集成语言的每个点上验证编程的途径。研究人员开发了渐进验证的基础理论，设计和实现了集成渐进验证的通用语言，并设计了向新手程序员教授验证的教学方法。通过逐步使验证更易于使用，开发人员将更有可能利用这些技术，为更多程序员带来验证的已知好处。该项目开发了向初学者程序员教授逐步验证的方法，并在马里兰大学新的入门编程序列中对其进行评估。该研究支持在每个步骤中集成验证的软件开发实践，并消除强化编程的障碍。 技术方法的核心是渐进验证，这是一种利用运行时执行机制并通过抽象解释技术系统地将这些机制转化为静态验证方法的技术。此外，由于运行时强制的基础，验证变成了一个范围而不是二进制，因为无法静态验证的属性可以在运行时强制执行。这种方法使项目能够随着时间的推移沿着从较少到更多验证的梯度发展，并为许多有用的、具有强化性、高效性和通用性的编程工具提供了可能性。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力优点和更广泛的影响审查标准进行评估，被认为值得支持。

This project contributes theories, tools, and a pedagogical framework to close the gap between programming languages widely used in everyday programming tasks and the few verification-integrated languages that offer strong correctness guarantees. Inspired by two significant trends in programming language research, namely gradual types and theorem proving languages, this work synthesizes aspects of both to enable pathways to verified programming at every point along the spectrum from scripting languages to verification-integrated languages. The investigators develop a foundational theory of gradual verification, design and implement a general purpose language with integrated gradual verification, and devise pedagogical approaches to teaching verification to novice programmers. By making verification easier to use in a gradual way, developers will be more likely to make use of these techniques, bringing the known benefits of verification to more programmers. This project develops methods to teach gradual verification to beginner programmers and evaluates them in the new introductory programming sequence at University of Maryland.This research supports software development practices that integrate verification at each step and removes impediments to fortified programming. At the core of the technical approach is gradual verification, a technique that leverages run-time enforcement mechanisms and systematically turns these mechanisms in to static verification methods via abstract interpretation techniques. Moreover, due to the basis in run-time enforcement, verification becomes a spectrum rather than a binary, since properties that fail to statically validate can be enforced at run-time. This approach enables programs to evolve over time along a less- to more-verified gradient and opens up the possibility for a number of useful programming tools that are reinforcing, productive, and universal.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.