Email Gateway (Aug 22 2022 at 16:39): Email Gateway (Aug 22 2022 at 16:39):From: "Thiemann, Rene" <Rene.Thiemann@uibk.ac.at>
Dear all,
today, I’d like to announce a new AFP entry on Hoare logics for time bounds.
Enjoy,
René
Hoare Logics for Time Bounds
by Maximilian P. L. Haslbeck and Tobias Nipkow
We study three different Hoare logics for reasoning about time bounds of
imperative programs and formalize them in Isabelle/HOL: a classical Hoare like
logic due to Nielson, a logic with potentials due to Carbonneaux et al. and a
separation logic following work by Atkey, Chaguérand and Pottier. These logics
are formally shown to be sound and complete. Verification condition generators
are developed and are shown sound and complete too. We also consider variants
of the systems where we abstract from multiplicative constants in the running
time bounds, thus supporting a big-O style of reasoning. Finally we compare
the expressive power of the three systems.
Last updated: Nov 21 2024 at 12:39 UTC