Portrait of Yuri Gurevich

Yuri Gurevich

Principal Researcher

About

Yuri Gurevich is an American computer scientist and mathematician and the inventor of abstract state machines. He is Principal Researcher at Microsoft Research, where he founded the Foundations of Software Engineering group, and he is professor emeritus at the University of Michigan.

Gurevich was educated in the Soviet Union, and taught in Israel before coming to the United States. The best known work of his Soviet period is on the classical decision problem. In Israel, Gurevich worked with Saharon Shelah on monadic second-order theories. The Forgetful Determinacy Theorem of Gurevich-Harrington is of that period as well. As far as his American period is concerned, Gurevich is best known for his work on finite model theory and the theory of abstract state machines. He has also contributed to average-case complexity theory.

Gurevich is an ACM Fellow, a Guggenheim Fellow, a member of Academia Europaea, and Dr. Honoris Causa of Hasselt University in Belgium and of Ural State University in Russia. In 2014 he became one of ten inaugural fellows of the European Association for Theoretical Computer Science.

Projects

Publications

Videos

Other

Some Recorded Talks

Axiomatic definition of sequential algorithms

Axiomatic definition of sequential algorithms

2011-03-30 Microsoft Channel 9 Lecture 3 on Algorithms

  • What are sequential algorithms?
  • Postulate 1 (Sequential Time)
  • Postulate 2 (Abstract State)
  • Postulate 3 (Bounded Exploration)
  • Axiomatic definition
  • Representation Theorem

What's an algorithm?

What’s an algorithm?

2011-02-07 Microsoft Channel 9 Lecture 2 on Algorithms

  • Is it possible to define algorithms?
  • What kind of entities are algorithms?
  • Why bother to define algorithms?
  • Algorithms = Turing machines?

Algorithms and computability

Algorithms and computability

2010-06-02 Microsoft Channel 9 Lecture 1 on Algorithms

  • Euclid’s algorithms and his time
  • One classification of algorithms
  • Turing’s analysis of symbolic algorithms
  • Computability and decidability
  • Limitations of the Turing machine model
  • On the verge of computational complexity

Interview from 2010

2010-02-02 Microsoft Channel 9 interview

  • The interview, conducted by Charles Torre of Channel 9, touched upon a number of topics.
  • Logic in Soviet Union.
  • A critique of functional programming and declarative specifications.
  • The analysis of algorithms that motivated the introduction of abstract state machines. The is by far the longest piece of the conversation.
  • A recent article When two algorithms are the same?
  • A quick motivation of a new Distributed Knowledge Authorization Language (DKAL).
  • The sequential character of human thought.

Lecture on Church-Turning thesis Google

2009-06-02 lecture on Church-Turing thesis at Google

  • It is the same lecture as the #1 but to a different audience with different questions.

Lecture on Church-Turning thesis Microsoft

2009-01-20 lecture on Church-Turing thesis at Microsoft

The lecture was organized by the Association for the Advancement of Artificial Intelligence of Greater Seattle

ABSTRACT:  The Church-Turing thesis is one of the foundations of computer science. The thesis heralded the dawn of the computer revolution by enabling the construct of the universal Turing machine which led the way, at least conceptually, to the von Neumann architecture and first electronic computers. One way to state the Church-Turing thesis is as follows: A Turing Machine computes every numerical function that is computable by means of a purely mechanical procedure.

It is that remarkable and a priori implausible characterization that underlies the ubiquitous applicability of digital computers. But why do we believe the thesis? Careful analysis shows that the existing arguments are insufficient. Kurt Godel surmised that it might be possible to state axioms which embody the generally accepted properties of computability, and to prove the thesis on that basis. That is exactly what we did in a recent paper with Nachum Dershowitz of Tel Aviv University.

Beyond our proof, the story of the Church-Turing thesis is fascinating and scattered in specialized and often obscure publications. We try to do justice to that intellectual drama.

Book Contributions

The Classical Decision Problem book

Egon Börger, Erich Grädel, Yuri Gurevich“Classical Decison Problem”Springer Verlag, Perspectives in Mathematical Logic, 1997Second printing, Springer Verlag, 2001

The classical decision problem is (in its modern meaning) the problem of classifying fragments of first-order logic with respect to the decidability and complexity of the satisfiability problem as well as the satisfiability problem over finite domains. The results and methods employed are used in logic, computer science and artificial intelligence. The book gives the most complete and comprehensive treatment of the classical decision problem to date, and includes an annotated biblography of 549 items. Much of the material is published for the first time in book form; this includes the classifiability theory, the classification of the so-called standard fragments, and the analysis of the reduction method. Many proofs have been simplified and there are many new results and proofs.

Books with multiple contributions of Yuri Gurevich

2004

Yuri Gurevich and guest authors “Logic in Computer Science” chapter (pages 95–311) in book

Current Trends in Theoretical Computer Science: The Challenge of the New Century Volume 2: Formal Models and Semantics eds. G. Paun, G. Rozenberg and A. Salomaa World Scientific, 2004

The chapter consists of articles published in the column on Logic in Computer Science in the Bulletin of European Association for Theoretical Computer Science from the October 2000 issue till the October 2003 issue.

2001

Yuri Gurevich and guest authors “Logic in Computer Science” chapter (pages 233–436) in book

Current Trends in Theoretical Computer Science: Entering the 21st Century eds. G. Paun, G. Rozenberg and A. Salomaa World Scientific, 2001

With one exception, the chapter consists of articles published in the column on Logic in Computer Science in the Bulletin of European Association for Theoretical Computer Science from the October 1992 issue till the February 2000 issue. The exception is the banquet talk published in the Bulletin outside the column.

1995

Specification and Validation Methods ed. E. Boerger, Oxford University Press, 1995

1993

Yuri Gurevich and guest authors “Logic in Computer Science” chapter (pages 223–394) in book

Current Trends in Theoretical Computer Science: Essays and Tutorials eds. G. Rozenberg and A. Salomaa World Scientific, 1993

With one exception, the chapter consists of the articles published in the column on Logic in Computer Science in the Bulletin of European Association for Theoretical Computer Science from the inception of the column in 1988 till the June 1992 issue. The exception is an updated version of the evolving algebra tutorial published in the Bulletin outside the column.