Award Abstract #1619282
SHF: Small: Collaborative Research: Online Verification-Validation

NSF Org:	CCF Division of Computing and Communication Foundations
Initial Amendment Date:	May 13, 2016
Latest Amendment Date:	March 15, 2019
Award Number:	1619282
Award Instrument:	Standard Grant
Program Manager:	Anindya Banerjee CCF Division of Computing and Communication Foundations CSE Direct For Computer & Info Scie & Enginr
Start Date:	September 1, 2016
End Date:	August 31, 2019 (Estimated)
Awarded Amount to Date:	$309,990.00
Investigator(s):	Bor-Yuh Evan Chang evan.chang@colorado.edu (Principal Investigator) Matthew Hammer (Former Principal Investigator) Bor-Yuh Evan Chang (Former Co-Principal Investigator)
Sponsor:	University of Colorado at Boulder 3100 Marine Street, Room 481 Boulder, CO 80303-1058 (303)492-6221
NSF Program(s):	SOFTWARE & HARDWARE FOUNDATION
Program Reference Code(s):	7923, 7943
Program Element Code(s):	7798

ABSTRACT

Increasingly, modern software on the web is richly extensible, accelerating its evolution and dramatically reducing the time between development and deployment. The intellectual merit of this research consists of challenging the false choice between creating software that is extensible (easy to reuse and extend) and software that is correct (meets its specifications). The new approach advanced by this work, Incremental Verification-Validation, enables programmers to bring domain-specific safely disciplines to extensible systems, by providing a framework where these disciplines are communicated both precisely and usefully, as executable code. The project's broader significance and importance consist in changing the way programmers approach building correct extensible software for the web. The research targets ECMAScript (JavaScript), enabling this research to have a direct impact on the vast number of languages and systems that create and use JavaScript. Further, the project represents a new collaboration across the University of Colorado and University of Maryland, bringing together experts across verification, incremental computing, and runtime systems. Finally, this project benefits the graduate and undergraduate teaching mission at the participating universities, as aspects of the project enriches the program analysis and programming language courses.

Incremental Verification-Validation encourages programmers to co-design their systems with executable specifications that check these systems dynamically, as they execute. Moreover, unlike typical assertions, which execute dynamically and non-incrementally, the proposed are subject to novel patterns that enhance their performance: In regressive validation, verification partially discharges some checks, dynamically rewriting the program with residual versions; in progressive verification, online verification occurs in passes that each cache and reuse work, to avoid from-scratch verification of facts that still hold from earlier passes. Finally, to avoid forcing analysis programmers to reason about incremental changes explicitly in each analysis that they create, the meta layer expresses incremental computations implicitly, using an implicitly-incremental meta language whose abstractions hide reasoning on a per-change basis.

PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH

Note:  When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

Matthew A. Hammer, Bor-Yuh Evan Chang, David Van Horn. "A Vision for Online Verification-Validation," Proceedings of the 2016 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, 2016.

Please report errors in award information by writing to: awardsearch@nsf.gov.