A verifier and timing analyser for simple imperative programs

Abstract

A system will be described for analysing both qualitative and quantitative aspects of program behaviour. The input consists of commands (built from assignments, sequencing, conditionals and while-loops) that have been annotated with assertions about the values of variables. The output consists of theorems about the state-transitions made by the machine instructions obtained by compiling the annotated commands. These theorems consist of total correctness assertions together with worst-case time and space properties. The system is automatic on simple examples, but usually it generates verification conditions that need to be solved manually (using the HOL theorem prover). An example session with the system will be presented, followed by an explanation of the theoretical principles underlying it and their mechanization in HOL.