David L. Dill

Page d’aide sur l’homonymie

Pour les articles homonymes, voir Dill.

David L. Dill
une illustration sous licence libre serait bienvenue
Biographie
Naissance
Voir et modifier les données sur Wikidata (68 ans)
Formation
Activités
Autres informations
A travaillé pour
Chaire
Donald E. Knuth Professorship (d)Voir et modifier les données sur Wikidata
Membre de
Directeur de thèse
Élève
Site web
Distinctions

modifier - modifier le code - modifier WikidataDocumentation du modèle

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 chair 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[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].

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[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].

Vote électronique

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].

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é 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 :

Notes et références

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « David L. Dill » (voir la liste des auteurs).
  1. ↑ (en) « David L. Dill », sur le site du Mathematics Genealogy Project
  2. ↑ a et b « David L. Dill » (consulté le )
  3. ↑ Bio de David L. Dill sur sa page personnelle à Stanford
  4. ↑ David L. Dill, Trace Theory for Automatic Heirarchical Verification of Speed-independent Circuits (Thèse), MIT Press, (lire en ligne).
  5. ↑ J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill et L. J. Hwang, « Symbolic Model Checking: 1020 States and Beyond », dans Proceedings of Logic in Computer Science (LICS '90), (lire en ligne), p. 428-439.
  6. ↑ David L. Dill, Andreas J. Drexler, Alan J. Hu et C. Han Yang, « Protocol verification as a hardware design aid », dans Computer Design: VLSI in Computers and Processors ICCD'92, (lire en ligne)
  7. ↑ David L. Dill, « A Retrospective on murφ », dans Orna Grumberg et Helmut Veith (éditeurs), 25 Years of Model Checking - History, Achievements, Perspectives, Springer, coll. « Lecture Notes in Computer Science » (no 5000),‎ (DOI 10.1007/978-3-540-69850-0_5, lire en ligne), p. 77-88
  8. ↑ Rajeev Alur et David L. Dill, « A theory of timed automata », Theoretical Computer Science, vol. 126, no 2,‎ , p. 183–235 (DOI 10.1016/0304-3975(94)90010-8).
  9. ↑ Jerry R. Burch et David L. Dill, « Automatic verification of pipelined microprocessor control », dans Computer Aided Verification, coll. « Lecture Notes in Computer Science » (no 818), (ISBN 978-3-540-58179-6, DOI 10.1007/3-540-58179-0_44), p. 68–80.
  10. ↑ C. Barrett, D. Dill et J. Levitt, « Validity Checking for Combinations of Theories with Equality », dans Proceedings of Formal Methods in Computer-Aided Design (FMCAD '96), (lire en ligne), p. 187-201.
  11. ↑ Aaron Stump, Clark W. Barrett et David L. Dill, « CVC: A Cooperating Validity Checker », dans Computer Aided Verification, coll. « Lecture Notes in Computer Science » (no 2404), (ISBN 978-3-540-43997-4, DOI 10.1007/3-540-45657-0_40, CiteSeerx 10.1.1.17.1530), p. 500–504.
  12. ↑ Vijay Ganesh et David L. Dill, « A Decision Procedure for Bit-Vectors and Arrays », dans Computer Aided Verification, coll. « Lecture Notes in Computer Science » (no 4590), (ISBN 978-3-540-73367-6, DOI 10.1007/978-3-540-73368-3_52, CiteSeerx 10.1.1.144.5247), p. 519–531.
  13. ↑ Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill et Dawson R. Engler, « EXE », ACM Transactions on Information and System Security, vol. 12, no 2,‎ , p. 1–38 (DOI 10.1145/1455518.1455522)
  14. ↑ Publications de David L. Dill sur sa page personnelle à Stanford
  15. ↑ « Resolution on Electronic Voting » (consulté le )
  16. ↑ « Verified Voting » (consulté le ).

Liens externes