CAREER: Formal Specifications as a Foundation for Aligned and Automated Software Engineering

Modern software increasingly relies on autonomous AI-driven systems that generate, test, and revise code. Yet even the most advanced tools struggle with a simple question: does the software behave as intended? The answer depends on clear descriptions of expected behavior, known as formal specifications. In practice, such specifications are rare because they are difficult to write and maintain. This project studies how to make formal specifications practical, accessible, and central to software development. The project’s novelties are the creation of a large-scale resource that connects everyday language descriptions, precise behavioral rules, and real code; automated methods that derive and update these rules as software evolves; and tools that use them to guide intelligent AI-based coding systems. The project’s broader significance and importance are that reliable specifications enable safer AI-based autonomous systems, reduce costly failures, and increase public trust in critical software infrastructure, including applications in healthcare and finance. The project establishes a repository-level dataset linking natural language documentation, formal behavioral specifications, and code artifacts, accompanied by an automated evaluation pipeline for reproducible assessment of specification accuracy. It develops methods to infer specifications from documentation and program structure, propagate them across code dependencies, and maintain them under version changes to preserve semantic alignment. The project also advances specification-driven development tools that use these formal artifacts as semantic constraints to guide AI-based code generation and to detect behavioral inconsistencies early in the lifecycle. By integrating data infrastructure, inference algorithms, and alignment-oriented tooling, the research strengthens the theoretical and practical foundations of specification-centered software engineering. Its impact extends beyond computer science by enabling more dependable digital systems that society increasingly depends upon. 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. NSF Award ID: 2542053 | Program: 01003031DB NSF RESEARCH & RELATED ACTIVIT,01002627DB NSF RESEARCH & RELATED ACTIVIT,01002930DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Juan Zhai | Institution: University of Massachusetts Amherst, AMHERST, MA | Award Amount: $396,112 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2542053 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2542053.html