Скачать или смотреть APLAS-ATVA 2024 Keynote: High-Order Fixpoint Logic for Automated Program Verification

Title: High-Order Fixpoint Logic for Automated Program Verification

Speaker: Naoki Kobayashi (University of Tokyo)

Abstract: We present an overview of our recent project on automated program verification based on higher-order fixpoint logic HFL(Z), a higher-order logic equipped with fixpoint operators and integer arithmetic. Various problems for higher-order program verification can naturally be reduced to the validity checking problem for HFL(Z) formulas. Thus, an HFL(Z) validity checker can serve as a common backend for automated verification tools for higher-order programs. We explain why the HFL(Z) approach is preferable to other representative approaches to automated higher-order program verification, such as the one based on the model checking of higher-order recursion schemes. We also outline how an automated HFL(Z) validity checker can be constructed, and discuss the remaining challenges and future directions.