GOALI: SHF: Automated Verification and Validation for Quantum Software

This project focuses on improving how quantum computer programs are created, tested, and trusted. Quantum computing offers the potential to solve problems beyond the reach of today's classical computers, and its development is entering an era of realizing its benefits as many new investments bring it into the mainstream, but writing correct quantum programs remains extremely difficult. Current approaches require programmers to work at a very low level of detail and to understand hardware constraints, which creates significant barriers to broader adoption. In addition, many promising quantum algorithms exist only as mathematical descriptions and lack reliable implementations. This project addresses these challenges by developing AVQS (Automated Verification and Validation for Quantum Software), a framework that enables programmers to describe quantum programs at a higher level, automatically verify their behavior, and ensure correctness before execution. The project’s novelties are the integration of high-level program specification with automated validation and full correctness certification for quantum software. The project's impacts are enabling more reliable quantum applications, lowering barriers for non-experts to develop quantum programs, and accelerating progress toward practical, trustworthy quantum computing systems. The project develops AVQS as a comprehensive framework that unifies program abstractions, testing methodologies, and formal verification techniques for quantum software. Its core includes a validation infrastructure that combines symbolic execution with concrete testing strategies, such as property-based testing, to systematically explore program behaviors and identify errors. The framework also incorporates formal verification methods to provide end-to-end correctness guarantees for quantum programs derived from high-level specifications. Certified programs are then compiled into executable quantum circuits. To evaluate AVQS, the investigator uses existing benchmark suites and develops new, diverse benchmark sets that capture a wider range of quantum applications beyond platform-specific implementations. Expected advances include scalable techniques for analyzing quantum programs, new methods for adapting classical software engineering tools to quantum contexts, and improved programming language abstractions that bridge the gap between algorithm design and circuit realization. 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: 2551577 | Program: 01002627DB NSF RESEARCH & RELATED ACTIVIT | Principal Investigator: Liyi Li | Institution: Iowa State University, AMES, IA | Award Amount: $850,000 View on NSF Award Search: https://www.nsf.gov/awardsearch/show-award/?AWD_ID=2551577 View on Research.gov: https://www.research.gov/awardapi-service/v1/awards/2551577.html