• Jean-Marie Cadiou (Stanford University, 1972): Recursive Definitions of Partial Functions and their Computations
• Ashok Chandra (Stanford University, 1973): On the Properties and Applications of Program Schemas
• Jean Vuillemin (Stanford University, 1973): Proof Techniques for Recursive Programs
• Philippe Flajolet (Université de Paris, 1979)
• Laurent Cheno (Université Paris Orsay, 1981)
• Mireille Régnier (Université Paris Orsay, 1983)
• Claude Puech (Université Paris Orsay, 1984)
• Claire Kenyon (Université Paris Orsay, 1988)
• Nicolas Schabanel (École Normale Superière Lyon, 2000)
• Jérémy Barbay (Université Paris Orsay, 2002)
• Michel Pocchiola (Université Paris, 1990)
• Pierre Angelier (Université Paris VII, 2002)
• Éric Colin de Verdière (Université Paris VII, 2003)
• Alexis Lamouret (Université Joseph Fourier, 1995)
• Nicolas Holzschuch (Universite Joseph Fourier, 1996)
• Jean-Christophe Lombardo (Universite Joseph Fourier, 1996)
• Francois Faure (Universite Joseph Fourier, 1997)
• Frédéric Cazals (Universite Paris VII, 1997)
• Nicolas Tsingos (Universite Joseph Fourier, 1998)
• Fredo Durand (Universite Joseph Fourier, 1999)
• Eric Paquette (Universite de Montreal, 2002)
• Philippe Jacquet (Universite Paris Orsay, 1988)
• Michelle Soria (Universite Paris Orsay, 1990)
• Luc Albert (Universite Paris Orsay, 1990)
• Daniele Gardy (Université Paris Orsay, 1990)
• Paul Zimmermann (École Polytechnique, 1991)
• Francois Bertault (Universite Henry Poincare, Nancy, 1997)
• Bruno Salvy (École Polytechnique, 1991)
• Philippe Dumas (Université Bordeaux, 1993)
• Xavier Gourdon (École Polytechnique, 1996)
• Frédéric Chyzak (École Polytechnique, 1998)
• Julien Clement (Université Caen, 2000)
• Cyril Banderier (Université Paris VI, 2001)
• Marianne Durand (École Polytechnique, 2002)
• Louis Monier(Université Paris, 1980)
• Patrice Bertin(Université Paris VII, 1993)
• Laurent Moll (École Polytechnique, 1997)
• Shmuel Katz (Weizmann Institute, 1976): Invariants and the Logical Analysis of Programs
• Orna Grumberg (Technion, 1984)
• Limor Fix (Technion, 1992)
• Orna Kupferman (Technion, 1995)
• Karen Yorav (Technion, 2000)
• Doron Bustan(Technion, 2002)
• Gadi Taubenfeld (Technion, 1988)
• Doron Peled (Technion, 1991)
• Marcelo Glusman (Technion, 2003)
• Marcelo Sihman (Technion, 2003)
• Adi Shamir (Weizmann Institute, 1977): Fixedpoints of Recursive Programs
• Mira Balaban (Weizmann Institute, 1983)
• Amos Fiat (Weizmann Institute, 1987)
• Yuval Rabani (Tel Aviv University, 1994)
• Anna Moss (Technion, 2001)
• Yair Bartal (Tel Aviv University, 1997)
• Yiftach Ravid (Tel Aviv University, 1994)
• Moty Ricklin (Tel Aviv University, 1995)
• Adi Rosén (Tel Aviv University, 1995)
• Manor Mendel (Tel Aviv University, 2001)
• Ziv Soferman (Weizmann Institute, 1990)
• Avital Schrift (Weizmann Institute, 1991)
• Eli Biham (Weizmann Institute, 1992)
• Tal Mor (1997)
• Dan Kenigsberg (Technion, 2008)
• Orr Dunkelman (2006)
• Elad Barkan (2006)
• Uriel Feige (Weizmann Institute, 1992)
• Dror Lapidot (Weizmann Institute, 1993)
• Nachum Dershowitz (Weizmann Institute, 1978): Automatic Program Modification
• Jieh Hsiang (University of Illinois, 1982; unofficial)
• Michael Rusinowitch (Université de Nancy, 1987)
• Adel Bouhoula (Université de Nancy, 1994)
• Laurent Vigneron (Université de Nancy, 1994)
• Eric Monfroy (Université de Nancy, 1996)
• Narjes Berregeb (Université de Nancy, 1997)
• Sorin Stratulat (Université de Nancy, 2000)
• Eric Johnson (SUNY Stonybrook, 1990)
• Maria Paola Bonacina (SUNY Stonybrook, 1992)
• Hong Chen (SUNY Stonybrook, 1992)
• Hsieh-Chang Tu (National Taiwan University, 1999)
• Guan-Shieng Huang (National Taiwan University, 1999)
• Yuh-Pyng Shieh (National Taiwan University, 2000)
• Leo Bachmair (University of Illinois, 1986)
• Ta Chen (SUNY Stony Brook, 1995)
• Ashish Tiwari (SUNY Stony Brook, 2000)
• Yuh-jeng Lee (University of Illinois, 1987)
• G. Sivakumar (University of Illinois, 1988)
• S. Hanumantha Rao (IIT Bombay, 1998)
• Jyotsna Kamal (IIT Bombay, 1999)
• Krishnan Ramanathan (IIT Bombay, 1999)
• N. Alan Josephson (University of Illinois, 1989)
• Naomi Lindenstrauss (Hebrew University, 1991)
• Subrata Mitra (University of Illinois, 1994)
• Charles Hoot (University of Illinois, 1996)
• Mitch Harris (University of Illinois, 2002)
• Alexander Nadel ( Tel Aviv University, 2009)
• Udi Boker (Tel Aviv University, 2009)
• Iddo Tzameret ( Tel Aviv University, 2009)
• William Scherlis (Stanford University, 1980): Expression Procedures and Program Derivation
• Scott Dietzen (Carnegie-Mellon University, 1990)
• Rod Nord (Carnegie-Mellon University, 1991)
• Pierre Wolper (Stanford University, 1982): Synthesis of Communicating Processes from Temporal Logic Specifications
• Marie-Jeanne Toussaint (University of Liège, 1991)
• Froduald Kabanza (University of Liège, 1992)
• Patrice Godefroid (University of Liège, 1994)
• Bernard Boigelot (University of Liège, 1998)
• Ben Moszkowski (Stanford University, 1983): Reasoning about Digital Circuits
• Roger Hale (University of Cambridge, 1988)
• Arun Chakrapani Rao (De Montfort University, 2002)
• Jordan Dimitrov (De Montfort University, 2002)
• Yoni Malachi (Stanford University, 1985): Nonclausal Logic Programming
• Martín Abadi (Stanford University, 1986): Temporal Theorem Proving
• Marianne Baudinet (Stanford University, 1988): Logic Programming Semantics: Techniques and Applications
• Rajeev Alur (Stanford University, 1991): Techniques for Automatic Verification of Real-Time Systems
• Salvatore La Torre (University of Pennsylvania, 2001)
• Bow-Yaw Wang (University of Pennsylvania, 2001)
• Franjo Ivancic (University of Pennsylvania, 2003)
• Zijiang Yang (University of Pennsylvania, 2003)
• Michael McDouggall (University of Pennsylvania, 2005)
• Wonhong Nam (University of Pennsylvania, 2007)
• Sebastian Burkhardt (University of Pennsylvania, 2007)
• Swarat Chaudhuri (University of Pennsylvania, 2007)
• Mikhail Bernardsky (University of Pennsylvania, 2008)
• Tom Henzinger (Stanford University, 1991): The Temporal Specification and Verification of Real-Time Systems
• Pei-Hsin Ho (Cornell, 1995)
• Peter Kopke (Cornell, 1996)
• Shaz Qadeer (UC Berkeley, 1999)
• Sriram Rajamani (UC Berkeley, 1999)
• Freddy Mang (UC Berkeley, 2002)
• Rupak Majumdar (UC Berkeley, 2003)
• Ru-Gang Xu (UC Los Angeles, 2008)
• Jeffrey M. Fischer (UC Los Angeles, 2008)
• Benjamin Horowitz (UC Berkeley, 2003)
• Ranjit Jhala (UC Berkeley, 2004)
• Arindam Chakrabarti (UC Berkeley, 2007)
• Arkadeb Ghoshal (UC Berkeley, 2007)
• Krishnendu Chatterjee (UC Berkeley, 2007)
• Slobodan Matic (UC Berkeley, 2007)
• Vinayak Prabhu (UC Berkeley, 2007)
• Slobodan Matic (UC Berkeley, 2007)
• Eddie Chang (Stanford University, 1994): Compositional Verification of Reactive and Real-Time Systems
• Hugh McGuire (Stanford University, 1995): Two Methods for Checking Formulas of Temporal Logic
• Anuchit Anuchitanukul (Stanford University,1995): Synthesis of Reactive Programs
• Arjun Kapur (Stanford University, 1997): Interval and Point-Based Approaches to Hybrid System Verification
• Luca de Alfaro (Stanford University, 1998): Formal Verification of Probabilistic Systems
• Nikolaj S. Bjorner (Stanford University, 1998): Integrating Decision Procedures for Temporal Verification
• Tomás E. Uribe (Stanford University, 1998): Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems
• Henny B. Sipma (Stanford University, 1999): Diagram-Based Verification of Discrete, Real-Time and Hybrid Systems
• Bernd E. Finkbeiner (Stanford University, 2002): Verification Algorithms Based on Alternating Automata
• Sven Schewe (Univ. Saarbruecken, 2008)
• Michael Colón (Stanford University, 2003): Deductive Techniques for Program Analysis
• Calogero Zarba (Stanford University, 2004): The Combination Problem in Automated Reasoning
• Sriram Sankaranarayanan (Stanford University, 2005): Mathematical Analysis of Programs.
• Ting Zhang (Stanford University, 2006): Arithmetic Integration of Decision Procedures.
• Matteo Slanina (Stanford University, 2007): Deductive Verification of Alternating Systems.
• César Sánchez (Stanford University, 2007): Deadlock Avoidance for Distributed Real-Time and Embedded Systems.
• Aaron Bradley (Stanford University, 2007): Safety Analysis of Systems.

The other direction:

Zohar Manna (Carnegie-Mellon University, 1968)

Robert W. Floyd

Alan J. Perlis (Massachusetts Institute of Technology, 1950)

Philip Franklin (Princeton University, 1921)

Oswald Veblen (University of Chicago, 1903)

Eliakim Hastings Moore (Yale University, 1885)

Hubert Anson Newton (Yale University, 1850)

Michel Chasles (École Polytechnique, 1814)

Siméon-Denis Poisson (École Polytechnique, 1798)

Joseph-Louis Lagrange [Giuseppe Lodovico Lagrangia] (unofficial; 1764)

Leonhard Euler (Universität Basel, 1726)

Johann Bernoulli (Universität Basel, 1694)

Jakob [Jaques] Bernoulli (Universität Basel, 1684)

Gottfried Willhelm Leibniz (Universität Altdorf, 1666)

Erhard Weigel (Universität Leipzig, 1650)

Christiaan Huygens (Universiteit Leiden / Université d'Angers 1647, 1655)

Frans van Schooten, Jr. (Universiteit Leiden, 1635)

Jacobus Golius (Universiteit Leiden, 1612, 1621)

Willebrord [Snel van Royen] Snellius (Universiteit Leiden, 1607)

Ludolph van Ceulen

Rudolph [Snel van Royen] Snellius (Universität zu Köln / Ruprecht-Karls-Universität Heidelberg, 1572)

Valentine Naibod (Martin-Luther-Universität Halle-Wittenberg / Universitat Erfurt)

Erasmus Reinhold (Martin-Luther-Universität Halle-Wittenberg, 1535)

Jakob Milich (Albert-Ludwigs-Universität Freiburg im Breisgau / Universität Wien, 1520, 1524)

Desiderius Erasmus (Collège de Montaigu, 1497)

Jan Standonck (Collège Sainte-Barbe / Collège de Montaigu, 1474, 1490)

Alexander Hegius von Heek

Ulrich Zasius (Albert-Ludwigs-Universität Freiburg im Breisgau, 1501)

Immanuel Tremellius

Thomas Erpenius

Marin Mersenne (Université Paris IV-Sorbonne, 1611)

Jan Jansz Stampioen, Jr.