David L. Dill
David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and 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 Donald E. Knuth Professor, Emeritus, in the School of Engineering and Professor, Emeritus, of Computer Science at Stanford University.
Biography
Dill 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. 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, 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 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.
He contributed to the development of symbolic model checking, helping to improve the scalability of the technique.
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.
He and Rajeev Alur extended classical automata theory with real-valued clocks, inventing timed automata.
In 1994, he and Jerry Burch published an influential paper on microprocessor verification, inventing a technique known as the Burch-Dill verification method.
He was also an early contributor to the research field known as satisfiability modulo theories, supervising the development of several early SMT solvers: the Stanford Validity Checker,
the Cooperating Validity Checker,
and the Simple Theorem Prover.
And he contributed to the development of a key application of SMT solvers to software testing known as concolic testing.