| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 8, 2021 |
| Latest Amendment Date: | July 25, 2022 |
| Award Number: | 2107169 |
| Award Instrument: | Continuing Grant |
| Program Manager: |
Anindya Banerjee
abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | July 15, 2021 |
| End Date: | June 30, 2024 (Estimated) |
| Total Intended Award Amount: | $399,995.00 |
| Total Awarded Amount to Date: | $399,995.00 |
| Funds Obligated to Date: |
FY 2022 = $150,240.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
ONE CASTLE POINT ON HUDSON HOBOKEN NJ US 07030-5906 (201)216-8762 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
NJ US 07030-5991 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
01002223DB NSF RESEARCH & RELATED ACTIVIT 01002324DB NSF RESEARCH & RELATED ACTIVIT |
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Reactive/interactive systems such as web applications and servers, real-time video streaming software, and IoT platforms are deeply embedded into all aspects of the modern world. Many program-analysis techniques and tools have been created to analyze important temporal properties of these systems that span both safety ("nothing bad will happen") and liveness ("something good eventually happens"). Unfortunately, modern static analyses are still limited in handling complex program semantics that often appear in many real-world applications: they support only simple properties, produce false positives, or do not scale to large programs. Recent dynamic or "data-driven" approaches address several shortcomings of static analyses to analyze more complex program properties more efficiently, yet sometimes yield incorrect results. The project's novelties are the theoretical and practical integration of static and dynamic approaches to analyze, localize, and repair temporal aspects of reactive/interactive systems. The project's impacts are the development of new theories and algorithms, giving rise to advanced methods for ensuring the safety/liveness of today's reactive/interactive software.
Today's software involves complex non-linear behavior, heap manipulations, and higher-order features. The project's use of dynamic analysis enables inference of expressive properties of these programs, while the use of static verification allows for validation of those inferred properties. Furthermore, static verification and dynamic learning mutually inform and bolster the power of each other, allowing for safety/liveness analyses, and even for the localization of faults and synthesis of repairs for temporal defects. The methods being developed are embodied in a growing collection of automated tools to be released publicly. The results of the research are used to develop new courses, senior design projects, and an interactive Jupyter book in programming languages and software engineering. The project broadens participation through several initiatives, aimed at middle/high school students and undergraduate students from underrepresented groups in the investigators' local communities.
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.
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.
PROJECT OUTCOMES REPORT
Disclaimer
This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.
Software is now pervasive and impacts many crucial aspects of modern life, ranging from human implant devices to autonomous vehicles to air traffic control systems. In these contexts it is essential that software operate reliably and researchers have thus sought methods for mathematically proving the correctness of computer code. Despite decades of progress, these techniques are still limited in applicability and impact. One reason is that existing techniques have focused on only what can be learned through analysis of the program (so-called "static analysis"), and have not incorporated what can be learned from example executions of the program ("dynamic" analysis).
This project studied how static and dynamic analyses can complement and inform each other to create novel algorithms for program analysis. By combining the strengths of the two approaches, the research improved verification and reliability of software systems in domains such as termination, temporal properties of programs, heap-manipulating programs, higher-order constructs, fault localization, and automated program repair. The project has also advanced the use of dynamic learning for inferring complex program properties, including numerical invariants and recurrent relations for reasoning program complexity. These techniques and results have been applied to diverse domains, including verifying safety properties in neural networks, optimizing cryptographic protocols, and improving automated program repair.
The project has produced publicly available open-source tools, benchmark suites and conference publications describing the research results. The project also impacted educational and outreach activities. Interactive learning materials were developed to encourage students to explore formal methods. Research results and materials were integrated into a summer program to encourage underrepresented students to pursue STEM studies. Finally, female and underrepresented minority students at both undergraduate and graduate levels were mentored and contributed to the project.
Last Modified: 02/06/2025
Modified by: Eric Koskinen
Please report errors in award information by writing to: awardsearch@nsf.gov.
