Van Horn Receives NSF Award For Gradual Verification Project

Published February 5, 2019

A University of Maryland expert in programming languages has won a National Science Foundation (NSF) award to develop next-generation programming languages that integrate strong correctness guarantees and verification technology with the aim of elevating the quality and reliability of software.

David Van Horn, an assistant professor of computer science with an appointment in the University of Maryland Institute for Advanced Computer Studies (UMIACS), is principal investigator of an NSF Faculty Early Career Development (CAREER) award, expected to total $573,376 over five years.

He will use the funding to develop theories, tools and a teachable framework on verification programs. His research will support software development practices that integrate verification at each step and make it easier for programmers to routinely incorporate.

Program verification, despite its major accomplishments, is considered a rarefied concern to most professional programmers. It is still widely seen as a niche skill, reserved only for those with advanced degrees and training in verification. The prevailing view is that program verification is expensive, time-consuming, and the benefits are limited outside of critical software.

Van Horn’s project draws from aspects of two significant trends in programming language research—gradual types and theorem proving languages—to enable pathways to verified programming at every point, from scripting languages to verification-integrated languages.

At the core of the technical approach is gradual verification. This technique leverages run-time enforcement mechanisms, and systematically turns these mechanisms into ways that guarantee a software program works correctly ahead of time. Gradual typing has been adopted by major software companies such as Microsoft’s TypeScript, Google’s Dart, and Facebook’s Flow.

Van Horn will develop a foundational theory of gradual verification, then design and implement a general purpose language with integrated gradual verification. He will also devise educational approaches to teaching verification to novice programmers.

By making verification easier to use in a gradual way, Van Horn hopes developers will be more likely to make use of these techniques, bringing the known benefits of verification to more programmers.

***

“Gradual Verification: From Scripting to Proving” is supported by NSF grant #1846350 from the NSF’s Division of Computing and Communication Foundations.

PI: David Van Horn, assistant professor of computer science with an appointment UMIACS.

About the CAREER award: The Faculty Early Career Development (CAREER) Program is an NSF activity that offers the foundation’s most prestigious awards in support of junior faculty who exemplify the role of teacher-scholars through outstanding research, excellent education and the integration of education and research within the context of the mission of their organization.