Yuri GurevichProfessor Emeritus of Computer Science
University of Michigan, Ann Arbor, MI, USA
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 Church-Turing thesis, many standard fragments of pure predicate logic have been proved to be decidable or reduction classes.  completed this classiﬁcation.  extended it to first-order logic with function symbols and explained why a complete classiﬁcations are possible in such cases, paving a way to a comprehensive book.
Monadic second-order 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.  solved some of those problems, which resulted in a decade-long collaboration with Shelah. Much of this work is summarized in . For example,  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.  solved Rabin’s Uniformization problem.  also covered the Gurevich-Harrington Forgetful Determinacy Theorem  that pioneered the use of games in computer science.
Here is one somewhat paradoxical post- result. Even though Shelah interpreted Peano arithmetic in the monadic theory of order,  established that such interpretation is impossible in ZFC. A ﬁner analysis showed that Shelah interpreted Peano arithmetic from another set-theoretic world.
Finite model theory
Here is a sample of our numerous contributions to finite model theory.  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.  showed that the extensions of first-order logic with monotone and with inflationary (a.k.a. nonmonotone) inductions have the same expressive power on finite structures.  proved that every datalog query, expressible in first-order logic, is bounded.  observed that ostensibly finite structures, like databases, have implicit infinite parts; it generalized finite model theory to metafinite model theory.  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 .
What is an algorithm?
The question, one might think, had been answered by Turing. But a Turing-machine 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.  defined abstract state machines (ASMs) in order to simulate arbitrary algorithms step-for-step on their natural abstraction levels.  axiomatized sequential algorithms and proved that sequential algorithms are behaviorally identical to sequential ASMs. In subsequent papers, these results were extended to parallel  and to interactive [176, 182] algorithms.
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 ASM-based tool, called Spec Explorer, which helped Microsoft when the European Union demanded in early 2000s that Microsoft produce high-level executable specifications of various communication protocols.
See this page in Google Patents.