RI: Formal Verification of Answer Set Programs

Modern society increasingly depends on software to make important decisions in areas such as logistics, transportation, manufacturing, and scientific research. Ensuring that this software behaves correctly is essential because errors can have significant societal and economic consequences. This project will strengthen the reliability of software developed using answer set programming, a widely used artificial intelligence (AI) technology for solving complex planning and reasoning problems. By creating methods that enable software developers to demonstrate that their programs are mathematically correct, the project will improve confidence in systems used in critical applications. The project will also contribute to the education of undergraduate and graduate students in AI, and help prepare a workforce with expertise in developing dependable planning and reasoning software systems that benefit science, industry, and society. The project will develop a methodology and supporting software tools for proving the correctness of answer set programs. Research activities include extending formal foundations for modern answer set programming language features, establishing and streamlining formal verification techniques for this prominent knowledge representation and reasoning paradigm. Within the project scope, the team will develop methods that exploit program modularity to simplify correctness proofs and integrate these advances into an interactive proof environment that assists developers throughout the verification process. The resulting framework will combine automated reasoning with user-guided proof construction to make formal verification practical for real world answer set programming applications. By providing rigorous verification techniques together with usable software tools, the project is expected to advance the state of the art in knowledge representation and reasoning, enable the development of more reliable AI software, and broaden the adoption of formally verified answer set programming-based systems in scientific and engineering applications. 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.