Monday, 18 November 2002, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B216
Abstract: One may think that the title problem was solved long ago by Church and Turing but it wasn't; there is more to an algorithm that the function it computes. (Besides, what function does an operating system compute?) The interest to the problem is not only theoretical; applications include specification, validation and verification of software and hardware systems.
In the first part of the talk, we formalize sequential algorithms, define sequential Abstract State Machines (ASMs) and sketch a proof of the following theorem: for every sequential algorithm A, there exists an ASM that is behaviorally identical to A and in particular simulates A step-for-step. The full proof of the theorem is found in ACM Transactions on Computational Logic, v 1, n 1, 2000.
In the second part of the talk, we discuss the Blass-Gurevich generalization of the theorem to parallel algorithms (to appear in the same journal), and ASM applications in Microsoft.
Tarmo Uustalu