David Lansing Dill (born January 8, 1957) is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.
David L. Dill | |
|---|---|
| Born | January 8, 1957 |
| Nationality |  United States |
| Alma mater | Massachusetts Institute of Technology |
| Awards | |
| Scientific career | |
| Doctoral advisor | Edmund M. Clarke |
| Notable students | Rajeev Alur |
| Website | [1] |
In 2013, Dill was elected as a member into the National Academy of Engineering for the development of techniques to verify hardware, software, and electronic voting systems.
He is the Donald E. Knuth Professor, Emeritus, in the School of Engineering and Professor, Emeritus, of Computer Science at Stanford University.
Biography
editDill received an S.B. degree in Computer Science and Electrical Engineering from the Massachusetts Institute of Technology, Cambridge, MA, in 1979, an M.S. degree in Computer Science from Carnegie-Mellon University, Pittsburgh, PA, in 1982, and a Ph.D. degree in Computer Science in 1987, also from Carnegie-Mellon University. After receiving his Ph.D., he joined the faculty of the computer science department at Stanford University, Stanford, CA.[1] He became an associate professor in 1994 and a full professor in 2000. In 2016 he became the first recipient of the Donald E. Knuth Professorship, an endowed chair in the Stanford University School of Engineering. From July 1995 to September 1996, he was Chief Scientist at 0-In Design Automation (acquired by Mentor Graphics in 2004), and, from 2016 to 2017, he was Chief Scientist at LocusPoint Networks, LLC. He was at Meta from 2018 to 2023 as a lead researcher on the Libra/Diem blockchain project.
Work
editDill's interests include asynchronous circuit design, software and hardware verification, automatic theorem proving, electronic voting security, and computational systems biology. His Ph.D. dissertation was an important contribution to asynchronous circuit verification and was published by MIT Press in 1989. [2] He contributed to the development of symbolic model checking, helping to improve the scalability of the technique. [3] Soon after arriving at Stanford, Dill and his students developed the murphi finite state verifier, which was later used to check cache coherence protocols in multiprocessors and CPU's of several major computer manufacturers. [4] [5] He and Rajeev Alur extended classical automata theory with real-valued clocks, inventing timed automata. [6] In 1994, he and Jerry Burch published an influential paper on microprocessor verification, inventing a technique known as the Burch-Dill verification method. [7] He was also an early contributor to the research field known as satisfiability modulo theories (SMT), supervising the development of several early SMT solvers: the Stanford Validity Checker (SVC), [8] the Cooperating Validity Checker (CVC), [9] and the Simple Theorem Prover (STP). [10] And he contributed to the development of a key application of SMT solvers to software testing known as concolic testing. [11]
Electronic Voting
editIn January 2003, Dill authored the "Resolution on Electronic Voting",[12] which calls for a voter-verifiable audit trail on all voting equipment. The resolution has been endorsed by thousands of people, including computer and security experts and elected officials. In July of that year, he created VerifiedVoting.org, and in February 2004, he founded the Verified Voting Foundation, on whose board he remains. In May 2004, he did several media interviews on the topic, including with Lou Dobbs Tonight and Jim Lehrer. In April 2005, he testified before the Commission on Federal Election Reform, co-chaired by Jimmy Carter and James Baker, and in June, he testified before the United States Senate.[1][13]
Professional recognition
editDill is a fellow of the ACM and the IEEE. His dissertation won the ACM Distinguished Dissertation award in 1988, and in the same year, he was named a Presidential Young Investigator. He received best paper awards at the IEEE International Conference on Computer Design in 1991 and at the Design Automation Conference in both 1993 and 1998. He received the Electronic Frontier Foundation Pioneer Award in 2004 for spearheading and nurturing the popular movement for integrity and transparency in modern elections. In 2008, he and Rajeev Alur received the Computer Aided Verification award for fundamental contributions to the theory of real-time systems verification. In 2010, he received two test of time awards from the Logic in Computer Science conference (for papers published in LICS in 1990). In 2013, he was elected to the National Academy of Engineering and the American Academy of Arts and Sciences. In 2016, he and Rajeev Alur received the Alonzo Church Award for outstanding contributions to logic, from the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). Also in 2016, he received a test of time award from the ACM Conference on Computer and Communications Security. In 2021, he was one of a group of researchers receiving a Computer Aided Verification award for pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT). He and his co-authors also received a Test of Time award from the Logic in Computer Science conference in 2021. In 2024, he received a third Computer Aided Verification award with a group of researchers for the ReluPlex algorithm for verifying deep neural networks
References
edit- ^ a b "David L. Dill". Archived from the original on September 17, 2017. Retrieved September 12, 2017.
- ^ David L. Dill. 1989, Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits Archived 2019-05-25 at the Wayback Machine. MIT Press.
- ^ J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang. 1990, Symbolic Model Checking: 1020 States and Beyond. In Proceedings of Logic in Computer Science (LICS '90), 428-439.
- ^ David L Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang Protocol verification as a hardware design aid Archived 2015-09-19 at the Wayback Machine. Computer Design: VLSI in Computers and Processors, 1992. ICCD'92.
- ^ David L Dill, A Retrospective on Murphi, 25 Years of Model Checking, 2008. LNCS, Springer
- ^ Rajeev Alur, David L. Dill. 1994, A Theory of Timed Automata. Theoretical Computer Science, Volume 126, Issue 2, 183-235.
- ^ Burch, Jerry R.; Dill, David L. (1994). "Automatic verification of pipelined microprocessor control". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 818. pp. 68–80. doi:10.1007/3-540-58179-0_44. ISBN 978-3-540-58179-6.
- ^ C. Barrett, D. Dill, J. Levitt. 1996, Validity Checking for Combinations of Theories with Equality. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD '96), 187-201.
- ^ Stump, Aaron; Barrett, Clark W.; Dill, David L. (2002). "CVC: A Cooperating Validity Checker". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2404. pp. 500–504. CiteSeerX 10.1.1.17.1530. doi:10.1007/3-540-45657-0_40. ISBN 978-3-540-43997-4. S2CID 26802227.
- ^ Ganesh, Vijay; Dill, David L. (2007). "A Decision Procedure for Bit-Vectors and Arrays". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 4590. pp. 519–531. CiteSeerX 10.1.1.144.5247. doi:10.1007/978-3-540-73368-3_52. ISBN 978-3-540-73367-6.
- ^ C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. 2008, EXE: Automatically Generating Inputs of Death ACM Transactions on Information and System Security (TISSEC), Vol. 12, Issue 2, 10:1-10:38.
- ^ "Resolution on Electronic Voting". Retrieved September 12, 2017.
- ^ "Verified Voting". Archived from the original on October 5, 2017. Retrieved September 12, 2017.