David Lansing Dill (né le ) est un informaticien et professeur américain connu pour des contributions à la vérification formelle, au vote électronique, et l'informatique de la biologie des systèmes. Il est professeur émérite sur la chaire Donald Knuth à la School of Engineering et professeur émérite d'informatique à l'université Stanford.

Biographie

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 sous la direction de Edmund M. Clarke, avec une thèse intitulée . Il rejoint ensuite le département d'informatique de l'université Stanford. 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 . De à , 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 blockchainsBio de David L. Dill sur sa page personnelle à Stanford.

Travaux

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.. Il a contribué au développement de la vérification de modèles en améliorant la scalabilité de la technique.. 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. Dill et Rajeev Alur introduisent en théorie des automates le nouveau concept d'automate temporisé.. En 1994, Dill et Jerry Burch introduisent une technique de vérification de microprocesseurs.. 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)., le Cooperating Validity Checker (CVC)., et le Simple Theorem Prover (STP).. et il a contribué au développement de la méthode du . Plus récemment, il a publié sur l'informatique de la biologie des systèmesPublications de David L. Dill sur sa page personnelle à Stanford.

Vote électronique En , Dill publie une résolution intitulée Resolution on Electronic Voting qui demande l'installation d'un dispositif produisant une 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 , il a fondé la Verified Voting Foundation, où il continue à siéger dans le bureau.

En , il intervient dans divers média y compris l'émission télévisuelle et celle de Jim Lehrer. En , il témoigne devant la présidée par Jimmy Carter et James Baker, et en juin, il témoigne devant le Sénat des États-Unis..

Honneurs et distinctions

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é . Il obtient le prix de la meilleure communication à la IEEE International Conference on Computer Design en 1991, et à la 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', de l'European Association for Theoretical Computer Science (EATCS), de l'European Association for Computer Science Logic (EACSL) et de la (KGS). 2016 : Test of time award de la conférence ACM Computer and Communications Security.

Notes et références

Liens externes

Catégorie:Naissance en janvier 1957 Catégorie:Personnalité américaine de l'informatique Catégorie:Professeur à l'université Stanford Catégorie:Étudiant du Massachusetts Institute of Technology Catégorie:Étudiant de l'université Carnegie-Mellon Catégorie:Membre de l'Académie américaine des arts et des sciences Catégorie:Personnalité en méthodes formelles