David L. Dill

Edit links
Source: Wikipedia, the free encyclopedia.
David L. Dill
Born (1957-01-08) January 8, 1957 (age 67)
Nationality United States
Alma materMassachusetts Institute of Technology
Awards
Scientific career
Doctoral advisorEdmund M. Clarke
Notable studentsRajeev Alur
Website[1]

David Lansing Dill (born January 8, 1957) is a

computational systems biology
.

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

Computer Science at Stanford University
.

Biography

Dill received an

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

Dill's interests include

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

In 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

Dill is a

Logic in Computer Science
conference in 2021.

References

  1. ^ a b "David L. Dill". Archived from the original on September 17, 2017. Retrieved September 12, 2017.
  2. ^ David L. Dill. 1989, Trace Theory for Automatic Hierarchical Verification of Speed Independent Circuits Archived 2019-05-25 at the Wayback Machine. MIT Press.
  3. ^ 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.
  4. ^ 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.
  5. ^ David L Dill, A Retrospective on Murphi, 25 Years of Model Checking, 2008. LNCS, Springer
  6. ^ Rajeev Alur, David L. Dill. 1994, A Theory of Timed Automata. Theoretical Computer Science, Volume 126, Issue 2, 183-235.
  7. ISBN 978-3-540-58179-6
    .
  8. ^ 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.
  9. S2CID 26802227
    .
  10. ISBN 978-3-540-73367-6
    .
  11. ^ 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.
  12. ^ "Resolution on Electronic Voting". Retrieved September 12, 2017.
  13. ^ "Verified Voting". Archived from the original on October 5, 2017. Retrieved September 12, 2017.

External links

Retrieved from "https://en.wikipedia.org/w/index.php?title=David_L._Dill&oldid=1211536686"