[Colloquium] Yuri Gurevich's talk next Friday, November 5th, 2004

[Margery Ishmael]

**UNIVERSITY OF CHICAGO LOGIC SEMINAR**

DATE: Friday, November 5, 2004

TIME: 1:30 p.m. (- 2:20 p.m.)

ROOM: Ryerson 251

TITLE:   Abstract State Machines: From Foundations to Microsoft Tools

SPEAKER:  YURI GUREVICH, Microsoft Research

ABSTRACT:

What is computer science about?  Largely about algorithms.
Programming languages, compilers, operating systems, communication
protocols, etc. are algorithms.  (More exactly, each of these gives
rise to a number of algorithms depending on the chosen abstraction
level.)  And what's an algorithm?  One may think that the question was
answered in full long ago by Church and Turing but it wasn't; there is
more to an algorithm than the function it computes.  (And what function
does an operating system compute?)

This line of research led to the definition of abstract state
machines and the ASM thesis: For every algorithm A, there is an ASM
that is behaviorally equivalent to A.  If A is sequential-time then
the ASM simulates A step for step.  International experimentation with
ASMs supports the thesis, and ever larger portions of the thesis have
been (and are being) proved from the first principles; see articles
141, 157, 166 and 170.

ASMs are a natural vehicle for executable specifications.  That caught
the attention of Microsoft Research and lead to the formation of a
group on Foundations of Software Engineering.  Some people think that
executable specification is a contradiction in terms.  We think that
executable specifications will change the way software is designed,
developed, tested and documented.  The specification languages AsmL
and Spec#, developed by the FSE group, make writing relatively large
ASMs practical.  Our tools allow the developers (more and more) to
experiment with their design, validate and enforce it.  The tools
empower numerous testers and enable them to be involved earlier in the
software development cycle.  We'll demonstrate SpecExplorer, our
latest tool.

BIOGRAPHICAL SKETCH:

Yuri Gurevich is a Sr. Researcher at Microsoft Research in Redmond,
WA.  He is also Professor Emeritus at the University of Michigan, an
ACM Fellow, a Guggenheim Fellow, and Dr. Honoris Causa of the Limburg
University in Belgium.

HOST:  ROBERT SOARE

*Refreshments will follow the talk in Ryerson 255*