Execution Time Program Verification With Tight Bounds

Ana Carolina Silva, Manuel Barbosa, Mario Florido

This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: ap…