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

Conrad Zimmerman, Jenna DiVincenzo

Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is al…