David L. Dill

Dill obtient un B. Sc. en informatique et électrotechnique au Massachusetts Institute of Technology en 1979, une M. Sc. en informatique à l'université Carnegie-Mellon en 1982, et un Ph. D. en informatique en 1987, également à l'université Carnegie-Mellon[1] sous la direction de Edmund M. Clarke, avec une thèse intitulée « Trace Theory for Automatic Heirarchical Verification of Speed-independent Circuits ». Il rejoint ensuite le département d'informatique de l'université Stanford[2]. Il devient professeur associé en 1994 et professeur titulaire en 2000. En 2016 il est le premier occupant due la chaire Donald Knuth, une chaire affectée à la Stanford University School of Engineering (en). De juillet 1995 à septembre 1996, il était chercheur scientifique en chef dans l'entreprise 0-In Design Automation (achetée par Mentor Graphics en 2004) et de 2016 à 2017, il était chercheur scientifique en chef dans l'entreprise LocusPoint Networks, LLC. Depuis son éméritat, il travaille pour Facebook sur les blockchains[3].

Les domaines de recherche de Dill comprennent la conception de circuits asynchrones, le logiciel et le matériel informatiques la vérification et validation, la démonstration automatique de théorèmes, la sécurité dans le vote électronique, et l'informatique de la biologie des systèmes. Sa thèse de Ph.D. sur la vérification de circuits asynchrones et a été publiée par MIT Press en 1989[4]. Il a contribué au développement de la vérification de modèles en améliorant la scalabilité de la technique[5]. Peu de temps après son arrivée à Stanford, Dill et ses étudiants développent le Murphi finite state verifier qui a servi ultérieurement au test de protocoles de cohérence de cache dans les multiprocesseurs les unités centrales de plusieurs constructeurs d'ordinateurs[6] - [7]. Dill et Rajeev Alur introduisent en théorie des automates le nouveau concept d'automate temporisé[8]. En 1994, Dill et Jerry Burch introduisent une technique de vérification de microprocesseurs[9]. Il aussi l'un des premiers contributeurs au domaine des satisfiability modulo theories (SMT), en supervisant le développement de plusieurs vérificateurs : le Stanford Validity Checker (SVC)[10], le Cooperating Validity Checker (CVC)[11], et le Simple Theorem Prover (STP)[12]. et il a contribué au développement de la méthode du Concolic testing (en)[13]. Plus récemment, il a publié sur l'informatique de la biologie des systèmes[14].

En janvier 2003, Dill publie une résolution intitulée Resolution on Electronic Voting[15] qui demande l'installation d'un dispositif produisant une trace de vote vérifiable sur papier (en) sur tous les équipements de votes. La résolution a été approuvée par des milliers de personnes, y compris des experts en informatique et en sécurité et par des représentants élus. En juillet de la même année, il a créé VerifiedVoting.org, et en février 2004, il a fondé la Verified Voting Foundation, où il continue à siéger dans le bureau.

En mai 2004, il intervient dans divers média y compris l'émission télévisuelle Lou Dobbs Tonight (en) et celle de Jim Lehrer. En avril 2005, il témoigne devant la Commission on Federal Election Reform (en) présidée par Jimmy Carter et James Baker, et en juin, il témoigne devant le Sénat des États-Unis[2] - [16].

Dill est fellow de l'ACM et de l'IEEE. Sa thèse a obtenu le prix ACM Distinguished Dissertation en 1988 ; la même année il est nommé Presidential Young Investigator (en). Il obtient le prix de la meilleure communication à la IEEE International Conference on Computer Design en 1991, et à la Design Automation Conference (en) en 1993 et en 1998. D'autres prix sont :

• 2004 : Electronic Frontier Foundation Pioneer Award « pour son rôle de fer de lance de soutien dans le mouvement populaire en faveur de l'intégrité et de la transparence dans le cadre d'élections modernes »
• 2008, Avec Rajeev Alur prix dee la conférence Computer Aided Verification « pour ses contributions fondamentales à la théorie de la vérification des systèmes temps réel ».
• 2010 : Test of time award du ACM-IEEE Symposium on Logic in Computer Science pour des articles publiés dans LICS en 1990, dont « Model checking for real-time systems » de la conférence LICS de 1990 (avec Rajeev Alur et Costas Courcoubetis).
• 2013 : Élu membre de l'Académie nationale d'ingénierie des États-Unis et de l'Académie américaine des arts et des sciences.
• 2016 : Avec Rajeev Alur, prix Alonzo Church décerné par l'ACM Special Interest Group for Logic and Computation (SIGLOG) (en), de l'European Association for Theoretical Computer Science (EATCS), de l'European Association for Computer Science Logic (EACSL) et de la Kurt Gödel Society (en) (KGS).
• 2016 également : Test of time award de la conférence ACM Computer and Communications Security.

• Page personnelle à Stanford University
• Liste de publications sur Google Scholar
• Liste de publications sur DBLP
• Notices d'autorité :

  • VIAF
  • ISNI
  • IdRef
  • LCCN
  • Israël
  • NUKAT
  • WorldCat
• Ressources relatives à la recherche :
  • Google Scholar
  • (en) Digital Bibliography & Library Project
  • (en) Mathematics Genealogy Project