Paper Info
Title
Hoare Logics for Time Bounds.
Abstract
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, Chaguerand 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.
Year
Venue
Field
2018
Archive of Formal Proofs
HOL,Separation logic,Programming language,Multiplicative function,Computer science,Hoare logic,Theoretical computer science,Expressive power
DocType
Volume
Citations 
Journal
2018
0
PageRank 
References 
Authors
0.34
10
2
Name
Order
Citations
PageRank
Maximilian Haslbeck123.09
Tobias Nipkow23056232.28