James B. Saxe

James Benjamin Saxe est un informaticien théoricien américain, spécialiste en analyse des algorithmes, spécification et vérification, et qui a travaillé longtemps au Centre de recherche de DEC^[1] et ses successeurs, le centre de recherche de Compaq et le centre de recherche de Hewlett-Packard HP Labs (en), toujours situés à Palo Alto.

James B. Saxe

Biographie

Formation	Union College Université Carnegie-Mellon
Activité	Informaticien

Autres informations

Directeur de thèse	Jon Bentley

modifier - modifier le code - modifier Wikidata

Études

Lauréat des Olympiades mathématiques des États-Unis (en)^[2], Saxe participe, quand il est étudiant au Union College, à la William Lowell Putnam Mathematical Competition et, en tant que l'un des cinq premiers classés, il obtient une bourse Putnam^[3]. Il est diplômé due Union College en 1976^[2] et obtient un Ph. D. en 1985 à l'Université Carnegie-Mellon, sous la supervision de Jon Louis Bentley, avec une thèse intitulée « Decomposable Searching Problems and Circuit Optimization by Retiming: Two Studies in General Transformation on Computational Structures »^[4].

Travaux

Saxe est connu pour ses contribution en démonstration automatique de théorèmes^[5], complexité des circuits^[6], conception de circuits synchrones et retiming^[7], réseaux informatiques^[8], et static program analysis^[9]. Ses travaux théoriques se situent principalement dans la période 1980-2000. De cette époque date aussi l'article sur le Master theorem^[10] dont il est l'un des trois coauteurs, avec Jon Bentley et Dorothea Blostein.

L'article sur l'analyse statique de programme Java de 2002 au colloque PDLI (Programming Language Design and Implementation (en)) dont il ex coauteur a obtenu le prix de l’article le plus influent (Most Influential PLDI Paper Award) en 2012^[11].

Publications (sélection)

• Jon Louis Bentley, Dorothea Haken et James B. Saxe, « A general method for solving divide-and-conquer recurrences », ACM SIGACT News, vol. 12, n^o 3,‎ septembre 1980, p. 36–44 (DOI 10.1145/1008861.1008865)

• Merrick Furst, James B. Saxe et Michael Sipser, « Parity, circuits, and the polynomial-time hierarchy », Mathematical Systems Theory, vol. 17, n^o 1,‎ 1984, p. 13–27 (DOI 10.1007/BF01744431, MR 738749)

• Charles E. Leiserson et James B. Saxe, « Retiming synchronous circuitry », Algorithmica, vol. 6, n^o 1,‎ 1991, p. 5–35 (DOI 10.1007/BF01759032, MR 1079368)

• Thomas E. Anderson, Susan S. Owicki, James B. Saxe et Charles P. Thacker, « High-speed switch scheduling for local-area networks », ACM Transactions on Computer Systems, vol. 11, n^o 4,‎ novembre 1993, p. 319–352 (DOI 10.1145/161541.161736)

• Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe et Raymie Stata, « Extended static checking for Java », SIGPLAN Notices, vol. 37,‎ mai 2002, p. 234–245 (DOI 10.1145/543552.512558)

• David Detlefs, Greg Nelson et James B. Saxe, « Simplify: a theorem prover for program checking », Journal of the ACM, vol. 52, n^o 3,‎ 2005, p. 365–473 (DOI 10.1145/1066100.1066102, MR 2146512)