Yuri GurevichProfessor Emeritus of Computer ScienceUniversity of Michigan, Ann Arbor, MI, USA gurevich_at_umich.edu 
Recent employment

Selected honors

The order is chronological more or less. References [n] are to Annotated Works. See also the Trier Bibliography
Classical Decision Problem
By the time of ChurchTuring thesis, many standard fragments of pure predicate logic have been proved to be decidable or reduction classes. [6] completed this classiﬁcation. [13] extended it to firstorder logic with function symbols and explained why a complete classiﬁcations are possible in such cases, paving a way to a comprehensive
book.
Monadic secondorder theories, games and set theory
In a rare logic paper in Annals of Mathematics (Vol. 102 (1975)),
Saharon Shelah proved numerous results, including the undecidability of the
monadic theory of (linear) order, and posed a number of problems. [26] solved
some of those problems, which resulted in a decadelong collaboration with
Shelah. Much of this work is summarized in [64]. For example, [45] proved that
the monadic theory of ω_{2} cannot be proven decidable or undecidable in ZFC, even though the monadic theory of orinals < ω_{2} had been proved decidable by Büchi. [47] solved Rabin’s Uniformization problem. [64] also covered the GurevichHarrington Forgetful Determinacy Theorem [40] that pioneered the use of games in computer science.
Here is one somewhat paradoxical post[64] result. Even though Shelah interpreted Peano arithmetic in the monadic theory of order, [79] established that such interpretation is impossible in ZFC. A ﬁner analysis showed that Shelah interpreted Peano arithmetic from another settheoretic world.
Finite model theory
Here is a sample of our numerous contributions to finite model theory. [60]
argued that traditional mathematical logic, developed to confront the infinite, is ill suited to deal with finite structures, like databases; more appropriate logics should be tailored for computational complexity. [70] showed that the extensions of firstorder logic with monotone and with inflationary
(a.k.a. nonmonotone) inductions have the same expressive power on finite structures. [83] proved that every datalog query, expressible in firstorder logic, is bounded. [109] observed that ostensibly finite structures, like databases, have implicit infinite parts; it generalized finite model theory to metafinite model theory. [74] conjectured that no reasonable logic captures polynomial time on unordered structures. The conjecture is widely believed to hold, yet there are no polynomial time properties of unordered structures provably inexpressible in the logic of [150].
What is an algorithm?
The question, one might think, had been answered by Turing. But a Turingmachine implementation of an algorithm A is in general much different from A. The question
is not what function, if any, an algorithm computes, but what it is at its natural abstraction level. [103] defined abstract state machines (ASMs) in order to simulate arbitrary algorithms stepforstep on their natural abstraction levels. [141] axiomatized sequential algorithms and proved that sequential algorithms are behaviorally identical to sequential ASMs. In subsequent papers, these results were extended to parallel [157] and to interactive [176, 182] algorithms.
Software engineering
Abstract state machines (ASMs) mentioned above have been used by the ASM community to specify software and hardware architectures, compilers, databases, programming languages, various distributed systems, etc. At Microsoft, my group on Foundations
of Software Engineering built an ASMbased tool, called Spec Explorer, which helped Microsoft when the European Union demanded in early 2000s that Microsoft produce highlevel executable specifications of various communication protocols.
See this page in Google Patents.