Hoare Logics for Time Bounds
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, Chagueraud
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.
Open access DOI
Author pdf
Isabelle theories in the
Archive of Formal Proofs
BibTeX:
@inproceedings{HaslbeckN-TACAS18,
author={Maximilian Paul Louis Haslbeck and Tobias Nipkow},
title={Hoare Logics for Time Bounds},
booktitle={Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)},
editor={M. Huisman and D. Beyer},
publisher={Springer},series={LNCS},volume={10805},pages={155-171},year=2018}