Abstract Hoare logic

In theoretical computer science, program logics are essential for verifying the correctness of software. Hoare logic provides a systematic way of reasoning about program correctness using preconditions and postconditions. This thesis explores the development and application of an abstract Hoare-like logic framework that generalizes the traditional Hoare program logic by using arbitrary elements of complete lattices as the assertion language, extrapolating what makes Hoare logic sound and complete. We also demonstrate the practical applications of this framework by systematically deriving a program logic for hyperproperties, thus highlighting versatility and benefits of our general framework. From the design of Abstract Hoare logic, we then define Reverse Abstract Hoare logic, which is used to develop a proof system for backward correctness reasoning on programs.