Yuri Gurevich

Last updated
Yuri Gurevich at ETH Zurich in May 2004, photograph by Bertrand Meyer. Yuri Gurevich ETH Zurich cropped.JPG
Yuri Gurevich at ETH Zurich in May 2004, photograph by Bertrand Meyer.

Yuri Gurevich, Professor Emeritus at the University of Michigan, is an American computer scientist and mathematician and the inventor of abstract state machines.

Gurevich was born and educated in the Soviet Union. [1] He taught mathematics there and then in Israel before moving to the United States in 1982. The best-known work of his Soviet period is on the classical decision problem. [2] In Israel, Gurevich worked with Saharon Shelah on monadic second-order theories. [3] The Forgetful Determinacy Theorem of Gurevich–Harrington is of that period as well. [4]

From 1982 to 1998, Gurevich taught computer science at the University of Michigan, where he started to work on various aspects of computational complexity theory [5] including average case complexity. [6] He became one of the founders of the emerging field of finite model theory. [7]

Most importantly, he became interested in the problem of what an algorithm is. This led him to the theory of abstract state machines (ASMs). The ASM Thesis says that, behaviorally, every algorithm is an ASM. [8] A few convincing axioms enabled derivation of the sequential ASM thesis [9] and the Church–Turing thesis. [10] The ASM thesis has also been proven for some other classes of algorithms. [11] [12]

From 1998 to 2018, Gurevich was with Microsoft Research where he founded a group on Foundations of Software Engineering. The group built Spec Explorer based on the theory of abstract state machines. The tool was adopted by the Windows team; a modified version of the tool helped Microsoft meet the European Union demands for high-level executable specifications. Later, Gurevich worked with different Microsoft groups on various efficiency, safety, and security issues, [13] including access control, [14] differential compression, [15] and privacy. [16]

Since 1988, Gurevich has managed the column on Logic in Computer Science in the Bulletin of the European Association for Theoretical Computer Science. [17] Since 2013 Gurevich has worked primarily on quantum computing, [18] while continuing research in his traditional areas.

Gurevich is a 2020 AAAS Fellow, [19] a 1997 ACM Fellow, [20] a 1995 Guggenheim Fellow, [21] an inaugural fellow of the European Association for Theoretical Computer Science, [22] a member of Academia Europaea, and Dr. Honoris Causa of Hasselt University in Belgium and of Ural State University in Russia.

Related Research Articles

<span class="mw-page-title-main">Algorithm</span> Sequence of operations for a task

In mathematics and computer science, an algorithm is a finite sequence of rigorous instructions, typically used to solve a class of specific problems or to perform a computation. Algorithms are used as specifications for performing calculations and data processing. More advanced algorithms can use conditionals to divert the code execution through various routes and deduce valid inferences, achieving automation eventually. Using human characteristics as descriptors of machines in metaphorical ways was already practiced by Alan Turing with terms such as "memory", "search" and "stimulus".

In computability theory, the Church–Turing thesis is a thesis about the nature of computable functions. It states that a function on the natural numbers can be calculated by an effective method if and only if it is computable by a Turing machine. The thesis is named after American mathematician Alonzo Church and the British mathematician Alan Turing. Before the precise definition of computable function, mathematicians often used the informal term effectively calculable to describe functions that are computable by paper-and-pencil methods. In the 1930s, several independent attempts were made to formalize the notion of computability:

In computer science, pseudocode is a description of the steps in an algorithm using a mix of conventions of programming languages with informal, usually self-explanatory, notation of actions and conditions. Although pseudocode shares features with regular programming languages, it is intended for human reading rather than machine control. Pseudocode typically omits details that are essential for machine implementation of the algorithm. The programming language is augmented with natural language description details, where convenient, or with compact mathematical notation. The purpose of using pseudocode is that it is easier for people to understand than conventional programming language code, and that it is an efficient and environment-independent description of the key principles of an algorithm. It is commonly used in textbooks and scientific publications to document algorithms and in planning of software and other algorithms.

Computer science is the study of the theoretical foundations of information and computation and their implementation and application in computer systems. One well known subject classification system for computer science is the ACM Computing Classification System devised by the Association for Computing Machinery.

In computer science, interactive computation is a mathematical model for computation that involves input/output communication with the external world during computation.

<span class="mw-page-title-main">Martin Davis (mathematician)</span> American mathematician (1928–2023)

Martin David Davis was an American mathematician and computer scientist who contributed to the fields of computability theory and mathematical logic. His work on Hilbert's tenth problem led to the MRDP theorem. He also advanced the Post–Turing model and co-developed the Davis–Putnam–Logemann–Loveland (DPLL) algorithm, which is foundational for Boolean satisfiability solvers.

In computer science, and more specifically in computability theory and computational complexity theory, a model of computation is a model which describes how an output of a mathematical function is computed given an input. A model describes how units of computations, memories, and communications are organized. The computational complexity of an algorithm can be measured given a model of computation. Using a model allows studying the performance of algorithms independently of the variations that are specific to particular implementations and specific technology.

In computer science, an abstract state machine (ASM) is a state machine operating on states that are arbitrary data structures.

In computer science, unbounded nondeterminism or unbounded indeterminacy is a property of concurrency by which the amount of delay in servicing a request can become unbounded as a result of arbitration of contention for shared resources while still guaranteeing that the request will eventually be serviced. Unbounded nondeterminism became an important issue in the development of the denotational semantics of concurrency, and later became part of research into the theoretical concept of hypercomputation.

<span class="mw-page-title-main">Leslie Valiant</span> British American computer scientist

Leslie Gabriel Valiant is a British American computer scientist and computational theorist. He was born to a chemical engineer father and a translator mother. He is currently the T. Jefferson Coolidge Professor of Computer Science and Applied Mathematics at Harvard University. Valiant was awarded the Turing Award in 2010, having been described by the A.C.M. as a heroic figure in theoretical computer science and a role model for his courage and creativity in addressing some of the deepest unsolved problems in science; in particular for his "striking combination of depth and breadth".

In theoretical computer science, a pointer machine is an atomistic abstract computational machine whose storage structure is a graph. A pointer algorithm could also be an algorithm restricted to the pointer machine model.

The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

Algorithm characterizations are attempts to formalize the word algorithm. Algorithm does not have a generally accepted formal definition. Researchers are actively working on this problem. This article will present some of the "characterizations" of the notion of "algorithm" in more detail.

John Vivian Tucker is a British computer scientist and expert on computability theory, also known as recursion theory. Computability theory is about what can and cannot be computed by people and machines. His work has focused on generalising the classical theory to deal with all forms of discrete/digital and continuous/analogue data; and on using the generalisations as formal methods for system design; based on abstract data types and on the interface between algorithms and physical equipment.

<span class="mw-page-title-main">Andreas Blass</span> German-American mathematician

Andreas Raphael Blass is a mathematician, currently a professor at the University of Michigan. He works in mathematical logic, particularly set theory, and theoretical computer science.

In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi–Elgot–Trakhtenbrot theorem gives a logical characterization of the regular languages.

<span class="mw-page-title-main">Ronald Fagin</span> American mathematician and computer scientist

Ronald Fagin is an American mathematician and computer scientist, and IBM Fellow at the IBM Almaden Research Center. He is known for his work in database theory, finite model theory, and reasoning about knowledge.

Nachum Dershowitz is an Israeli computer scientist, known e.g. for the Dershowitz–Manna ordering and the multiset path ordering used to prove termination of term rewrite systems.

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power.

Benjamin E. Rossman is an American mathematician and theoretical computer scientist, specializing in computational complexity theory. He is currently an associate professor of computer science and mathematics at Duke University.

References

  1. ↑ Blass, Andreas; Dershowitz, Nachum; Reisig, Wolfgang (2010), Blass, Andreas; Dershowitz, Nachum; Reisig, Wolfgang (eds.), "Yuri, Logic, and Computer Science", Fields of Logic and Computation, Lecture Notes in Computer Science, Berlin, Heidelberg: Springer Berlin Heidelberg, vol. 6300, pp. 1–48, doi:10.1007/978-3-642-15025-8_1, ISBN   978-3-642-15024-1 , retrieved 2023-07-05
  2. ↑ E. Börger, E. Grädel, and Y. Gurevich. The Classical Decision Problem. Springer, 1997.
  3. ↑ Y. Gurevich. Monadic second-order theories. In J. Barwise and S. Feferman (eds.), Model-Theoretic Logics, Springer, 1985, 479-506.
  4. ↑ Y. Gurevich and L. Harrington. Automata, Trees, and Games. STOC '82: Proceedings of the Fourteenth annual ACM Symposium on Theory of Computing, 1982, 60-65.
  5. ↑ Y. Gurevich and S. Shelah. Expected computation time for Hamiltonian Path Problem. SIAM Journal on Computing 16:3, 1987, 486-502.
  6. ↑ Y. Gurevich. Average case completeness. Journal of Computer and System Sciences 42:3, 1991, 346-398.
  7. ↑ Y. Gurevich. Toward logic tailored for computational complexity. In M Richter et al. (eds.), Computation and Proof Theory. Springer Lecture Notes in Mathematics 1104, 1984, 175-216.
  8. ↑ Y. Gurevich. Evolving Algebra 1993: Lipari Guide. In E. Börger (ed.), Specification and Validation Methods, Oxford University Press, 1995, 9–36. https://arxiv.org/abs/1808.06255
  9. ↑ Y. Gurevich. Sequential Abstract State Machines capture sequential algorithms. ACM Transactions on Computational Logic 1(1), 2000.
  10. ↑ N. Dershowitz and Y. Gurevich. A natural axiomatization of computability and proof of Church’s Thesis. Bulletin of Symbolic Logic 14:3, 2008, 299-350.
  11. ↑ A. Blass and Y. Gurevich. Abstract State Machines Capture Parallel Algorithms. ACM Transactions on Computational Logic 4(4), 2003, 578–651, and 9(3), 2008, article 19.
  12. ↑ A. Blass, Y. Gurevich, D. Rosenzweig, and B. Rossman. Interactive Small-Step Algorithms II: Abstract State Machines and the Characterization Theorem. Logical Methods in Computer Science 3(4), 2007, paper 4.
  13. ↑ "Google Patents".
  14. ↑ A. Blass, Y. Gurevich, M. Moskal, and I. Neeman. Evidential authorization. In S. Nanz (ed), The Future of Software Engineering, Springer 2011, 77–99.
  15. ↑ N. Bjørner, A. Blass, and Y. Gurevich. Content-dependent chunking for differential compression: The local maximum approach. Journal of Computer Systems Science 76(3-4), 2010, 154-203.
  16. ↑ Y. Gurevich, E. Hudis, and J.M. Wing. Inverse privacy. Communications of the ACM 59(7), 2016, 38-42.
  17. ↑ https://eatcs.org/index.php/eatcs-bulletin
  18. ↑ A. Bocharov, Y. Gurevich, and K.M. Svore. Efficient decomposition of single-qubit gates into V basis circuits. Physical Review A 88:1, 2013.
  19. ↑ AAAS Fellows, retrieved on Jan 11, 2021.
  20. ↑ ACM Fellows, Association for Computing Machinery. Accessed February 16, 2010.
  21. ↑ Fellows List, Archived June 22, 2011, at the Wayback Machine John Simon Guggenheim Memorial Foundation. Accessed February 16, 2010.
  22. ↑ "EATCS names 2014 fellows", Milestones: Computer Science Awards, Appointments, Communications of the ACM , 58 (1): 24, January 2015, doi:10.1145/2686734, S2CID   11485095
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.