David L. Dill
![Page d’aide sur l’homonymie](http://upload.wikimedia.org/wikipedia/commons/thumb/a/a9/Logo_disambig.svg/20px-Logo_disambig.svg.png)
Pour les articles homonymes, voir Dill.
![une illustration sous licence libre serait bienvenue](http://upload.wikimedia.org/wikipedia/commons/thumb/f/f7/Defaut_2.svg/langfr-260px-Defaut_2.svg.png)
Naissance | ![]() |
---|---|
Formation | |
Activités | Informaticien, universitaire, professeur d'université ![]() |
A travaillé pour | |
---|---|
Chaire | Donald E. Knuth Professorship (d) ![]() |
Membre de | |
Directeur de thèse | Edmund M. Clarke ![]() |
Élève | Rajeev Alur |
Site web | verify.stanford.edu/dill ![]() |
Distinctions | Liste détaillée |
modifier - modifier le code - modifier Wikidata
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 :
- 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.
Notes et références
- ↑ (en) « David L. Dill », sur le site du Mathematics Genealogy Project
- ↑ a et b « David L. Dill » (consulté le )
- ↑ Bio de David L. Dill sur sa page personnelle à Stanford
- ↑ David L. Dill, Trace Theory for Automatic Heirarchical Verification of Speed-independent Circuits (Thèse), MIT Press, (lire en ligne).
- ↑ 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.
- ↑ 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)
- ↑ 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
- ↑ 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).
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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.
- ↑ 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)
- ↑ Publications de David L. Dill sur sa page personnelle à Stanford
- ↑ « Resolution on Electronic Voting » (consulté le )
- ↑ « Verified Voting » (consulté le ).
Liens externes
- 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
:
- Digital Bibliography & Library Project
- Google Scholar
- Mathematics Genealogy Project
Portail de l’informatique
Portail de l'informatique théorique
Portail des États-Unis