Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification

TL;DR

This paper introduces gradual exact logic, unifying overapproximating and underapproximating logics like Hoare and incorrectness logic, to enhance verification and bug-finding techniques through gradual verification principles.

Contribution

It presents a novel definition of gradual verification and a new gradualization of exact logic, establishing a unified framework connecting Hoare logic, incorrectness logic, and gradual verification.

Findings

Unified framework for Hoare and incorrectness logic

Potential for applying exact logic techniques to verification and bug-finding

New gradualization approach for exact logic

Abstract

Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic [Maksimovic et al. 2023] which we call gradual exact logic. Further, we show that Hoare logic, incorrectness logic, and gradual verification can be defined in terms of gradual exact logic. We hope that this connection can be used to develop tools and techniques that apply to both gradual verification and bug-finding. For example, we envision that techniques defined in terms of exact logic can be directly applied to verification, bug-finding, and gradual verification, using the principles of gradual typing [Garcia et al. 2016].