Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Doing Business As Name:University of Vermont & State Agricultural College
  • David C Darais
  • (802) 656-3660
Award Date:08/21/2019
Estimated Total Award Amount: $ 599,440
Funds Obligated to Date: $ 599,440
  • FY 2019=$599,440
Start Date:10/01/2019
End Date:09/30/2023
Transaction Type:Grant
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:SHF: Medium: Collab Research: Synthesizing Verified Analyzers for Critical Software
Federal Award ID Number:1901278
DUNS ID:066811191
Parent DUNS ID:066811191
Program:Software & Hardware Foundation
Program Officer:
  • Nina Amla
  • (703) 292-7991

Awardee Location

Street:85 South Prospect Street
Awardee Cong. District:00

Primary Place of Performance

Organization Name:University of Vermont & State Agricultural College
Cong. District:00

Abstract at Time of Award

The reliability of a complete software system hinges on the reliability of each tool used to construct it. Among these tools are program analyzers which are automated tools for verifying the absence of specific classes of errors such as unsafe memory accesses. While used both for program optimization by compilers, and for eliminating software defects by software developers, program analyzers by themselves are not verified: their reliability is largely assumed and, in current practice, they inhabit a software's trusted computing base. This project develops (a) foundational theories for synthesizing program analyzers directly from their specifications; (b) practical implementations of program analyzers; and (c) rigorous evaluations of both foundational techniques as well as implementations via a mixture of formal methods, software development, and empirical case studies. Underlying these results is the potential for widespread adoption of these tools in practice thus leading to higher reliability of software more generally. The project's techniques and tools will enable the deductive synthesis of sound program analysers in proof assistants in an interactive, mostly-automated style, and using the calculational framework of abstract interpretation with Galois connections. The investigators evaluate this approach by first comparing to existing tools: Fiat, an existing tool for semi-automated deductive synthesis in the theorem prover Coq but which does not support Galois connections, and Constructive Galois Connections, an existing framework for embedding Galois connections in Agda language but which does not support automation. The investigators compare these results with existing on-paper derivations of correct-by-construction program analyzers, as well as existing information flow analyzers which were not derived using the abstract interpretation framework. 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.

For specific questions or comments about this information including the NSF Project Outcomes Report, contact us.