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.