The problem of validation of standard mathematical functions and libraries is well-recognized by industrial and academic professional community but still is poorly understood by freshmen and inexperienced developers. The paper gives and discusses two examples (from the author's pedagogical experience) when formal specification and verification of standard functions do help...
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...
We consider the well-known Sliding Window Protocol (SWP) which provides reliable and efficient transmission of data over unreliable channels. It seems quite important to give a formal proof of correctness for the SWP, especially because the high degree of parallelism in this protocol creates a significant potential for errors. However...
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...