Members
University of Nebraska Omaha (UNO)
|
Collaborators
|
Table of Contents
Project Summary
This project encompasses a number of research ventures falling under the umbrella topic of formal verification of answer set programs. These can be roughly divided into three interrelated categories. The first is the task of developing semantics for advanced ASP language constructs (aggregates and conditional literals) that do not refer to grounding. This allows ASP practitioners to reason formally about the correctness of their programs without reference to a particular input. The second category seeks to enhance modularity in Answer Set programs. From a formal verification perspective, it is desirable to reason about program components in isolation. This allows proofs of correctness for sub-programs to be recycled, and simplifies the task of verifying extended programs. Finally, the ability to automatically verify programs will make widespread adoption of formal methods for ASP development much more palatable. Details of our progress in this direction can be found on the Anthem-P2P software system linked below.
This work was partially supported by the Research Development Program (Fall 2020) from the Office of Research and Creative Activity (UNO).
Software
Publications
- External Behavior of a Logic Program and Verification of Refactoring - Jorge Fandinno, Zachary Hansen, Yuliya Lierler, Vladimir Lifschitz, and Nathan Temple - ICLP - 2023
- Arguing Correctness of ASP Programs with Aggregates - Jorge Fandinno, Zachary Hansen and Yuliya Lierler - LPNMR - 2022
- Semantics for Conditional Literals via the SM Operator - Zachary Hansen and Yuliya Lierler - LPNMR - 2022
- Axiomatization of Aggregates in Answer Set Programming - Jorge Fandinno, Zach Hansen and Yuliya Lierler - AAAI - 2022
Presentations
- Semantics for Conditional Literals via the SM Operator - Zach Hansen - LPNMR - 2022
- Arguing Correctness of ASP Programs with Aggregates - Zach Hansen - LPNMR - 2022
- Tools and Methodologies for Verifying Answer Set Programs - Zach Hansen - ICLP - 2022
- Axiomatization of Aggregates In Answer Set Programs - Zach Hansen - AAAI - 2022