CAREER: Gradual Verification: From Scripting to Proving

University Of Maryland, College Park, College Park MD

Investigators

Abstract

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.