Formal verification of programs for abstract register machines

Abstract register machines are an important formal model of computation widely used for the modeling of many classes of computational algorithms and the analysis of their complexity. Despite the significance of this model, formal verification of general-purpose programs for abstract register machines has not been properly covered in the existing literature. To fill this gap, we provide a formal specification for one version of abstract register machines – the random-access machine invented by Aho, Hopcroft and Ullman. Executions of this machine are formalized by a transition system in the language of the verification system PVS. We also specify in PVS a simple search program for this architecture and its correctness property. The property is proved using the interactive proof checker of PVS. We were able to prove not only the functional correctness of the program, but also its time complexity, which shows the novelty of our approach.