| Speaker: | Yuri GUREVICH, Microsoft Research, Redmond, WA, USA |
| Place: | Room B 216, Institute of Cybernetics, Akadeemia tee 21, Tallinn, Estonia |
| Time: | Monday, November 18, 2002, 14:00 |
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.