chklaev_nepomniaschy.pdf101.2 KB

The random-access machine invented by Aho, Hopcroft, and Ullman is one of the several known versions of abstract register machines, which are an important computation model. Using a formal framework developed for this architecture in our previous work, we consider a challenging example – a search program that computes the...

chkliaev.pdf195.55 KB

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...