Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Awardee:BOARD OF REGENTS OF THE UNIVERSITY OF NEBRASKA
Doing Business As Name:University of Nebraska-Lincoln
PD/PI:
  • Hamid Bagheri
  • (402) 472-5087
  • bagheri@unl.edu
Award Date:08/31/2021
Estimated Total Award Amount: $ 198,944
Funds Obligated to Date: $ 198,944
  • FY 2021=$198,944
Start Date:09/01/2021
End Date:08/31/2023
Transaction Type:Grant
Agency:NSF
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:EAGER: CCF: SHF: Scalable Software Verification through Automated Derivation of Domain-Specific Optimization Tactics
Federal Award ID Number:2139845
DUNS ID:555456995
Parent DUNS ID:068662618
Program:Software & Hardware Foundation
Program Officer:
  • Sol Greenspan
  • (703) 292-7841
  • sgreensp@nsf.gov

Awardee Location

Street:151 Prem S. Paul Research Center
City:Lincoln
State:NE
ZIP:68503-1435
County:Lincoln
Country:US
Awardee Cong. District:01

Primary Place of Performance

Organization Name:University of Nebraska-Lincoln
Street:
City:
State:NE
ZIP:68503-1435
County:Lincoln
Country:US
Cong. District:01

Abstract at Time of Award

The ever-growing reliance of society on software-intensive systems drives a continued demand for increased software dependability, making it more important than ever. Formal-verification techniques provide the highest degree of software assurance, with their strengths residing in their automated yet rigorous analysis capabilities. Performing such formal analyses is, however, an expensive endeavor, facing scalability issues. This challenge is exacerbated when considering the evolving nature of complex systems. The high cost of formal verification is thus prohibitive for rapidly evolving large-scale systems, despite the benefits it can offer for reliability, safety, and security. This research seeks to develop techniques for automating the development of optimizations for software-verification techniques with the aim that each system of interest can have verification tailored to its specific characteristics, thereby significantly reducing the verification cost. This, in turn, allows software engineers to continuously analyze evolving systems online, rather than the current practice of performing expensive, long-running formal analysis once, if at all, during the entire development process. In addition to graduate students, this project will attempt to involve undergraduate, female, and underrepresented minority students. This research project explores the possibility of driving the automated discovery of domain-specific optimizations for software-verification techniques. Historically, such optimizations have arisen from the insights of a few dozen experts in software verification worldwide. This research is taking a different approach. The project seeks to automatically infer domain-specific, sound optimizations to trim the verification bounds without requiring any prior domain expertise on the part of the analyzer, promising to make software verification significantly more scalable and cost-effective. The intellectual merit of this research is a novel, speculative analysis, underpinned by established, proven model-finding technologies to automatically recognize opportunities for the derivation of sound optimizations, without requiring domain expertise or excessive overhead, thereby significantly diminishing the analysis cost. This research promises to advance the state-of-the-art by rendering bounded formal verification more tractable, thereby expanding the areas that can practically benefit from formal verification techniques. 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.