Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
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].
Tue 21 JanDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:30 | |||
11:00 18mTalk | Data Structure Abstraction and Incorrectness Separation Logic TPSA Andreas Lööw Imperial College London | ||
11:18 18mTalk | Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification TPSA Pre-print | ||
11:36 18mTalk | Partial Incorrectness Logic TPSA Lena Verscht RWTH Aachen University; Saarland University, Ānrán Wáng Saarland University, Benjamin Lucien Kaminski Saarland University; University College London | ||
11:54 18mTalk | Total Outcome Logic: Termination and Nontermination Proving for Effectful Branching TPSA James Li Cornell University, Noam Zilberstein Cornell University, Alexandra Silva Cornell University | ||
12:12 18mTalk | U-turn: Forward-driven backward analysis for incorrectness TPSA Flavio Ascari University of Pisa, Roberto Bruni University of Pisa, Roberta Gori Diaprtimento di Informatica, Universita' di Pisa, Italy, Azalea Raad Imperial College London | ||