David L. Dill

Last updated
David L. Dill
Born (1957-01-08) January 8, 1957 (age 67)
NationalityFlag of the United States (23px).png  United States
Alma mater Massachusetts Institute of Technology
Awards
Scientific career
Doctoral advisor Edmund M. Clarke
Notable students Rajeev Alur
Website

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.

Contents

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

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

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

In computational complexity theory, EXPSPACE is the set of all decision problems solvable by a deterministic Turing machine in exponential space, i.e., in space, where is a polynomial function of . Some authors restrict to be a linear function, but most authors instead call the resulting class ESPACE. If we use a nondeterministic machine instead, we get the class NEXPSPACE, which is equal to EXPSPACE by Savitch's theorem.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

SPIN is a general tool for verifying the correctness of concurrent software models in a rigorous and mostly automated fashion. It was written by Gerard J. Holzmann and others in the original Unix group of the Computing Sciences Research Center at Bell Labs, beginning in 1980. The software has been available freely since 1991, and continues to evolve to keep pace with new developments in the field.

In automata theory, a hybrid automaton is a mathematical model for precisely describing hybrid systems, for instance systems in which digital computational processes interact with analog physical processes. A hybrid automaton is a finite state machine with a finite set of continuous variables whose values are described by a set of ordinary differential equations. This combined specification of discrete and continuous behaviors enables dynamic systems that comprise both digital and analog components to be modeled and analyzed.

In theoretical computer science and formal language theory, a regular tree grammar is a formal grammar that describes a set of directed trees, or terms. A regular word grammar can be seen as a special kind of regular tree grammar, describing a set of single-path trees.

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.

<span class="mw-page-title-main">Moshe Vardi</span> Israeli mathematicien and computer scientist

Moshe Ya'akov Vardi is an Israeli mathematician and computer scientist. He is the Karen Ostrum George Distinguished Service Professor in Computational Engineering at Rice University, United States. and a faculty advisor for the Ken Kennedy Institute. His interests focus on applications of logic to computer science, including database theory, finite model theory, knowledge of multi-agent systems, computer-aided verification and reasoning, and teaching logic across the curriculum. He is an expert in model checking, constraint satisfaction and database theory, common knowledge (logic), and theoretical computer science.

<span class="mw-page-title-main">Rajeev Alur</span> American computer scientist

Rajeev Alur is an American professor of computer science at the University of Pennsylvania who has made contributions to formal methods, programming languages, and automata theory, including notably the introduction of timed automata and nested words.

In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi–Elgot–Trakhtenbrot theorem gives a logical characterization of the regular languages.

<span class="mw-page-title-main">Mihalis Yannakakis</span> Greek-American computer scientist

Mihalis Yannakakis is professor of computer science at Columbia University. He is noted for his work in computational complexity, databases, and other related fields. He won the Donald E. Knuth Prize in 2005.

<span class="mw-page-title-main">E. Allen Emerson</span> American computer scientist

Ernest Allen Emerson II, better known as E. Allen Emerson, is an American computer scientist and winner of the 2007 Turing Award. He is Professor and Regents Chair Emeritus at the University of Texas at Austin, United States.

ACM SIGLOG or SIGLOG is the Association for Computing Machinery Special Interest Group on Logic and Computation. It publishes a news magazine, and has the annual ACM-IEEE Symposium on Logic in Computer Science (LICS) as its flagship conference. In addition, it publishes an online newsletter, the SIGLOG Monthly Bulletin, and "maintains close ties" with the related academic journal ACM Transactions on Computational Logic.

In model checking, a subfield of computer science, a timed word is an extension of the notion of words, in a formal language, in which each letter is associated with a positive time tag. The sequence of time tags must be non-decreasing, which intuitively means that letters are received. For example, a system receiving a word over a network may associate to each letter the time at which the letter is received. The non-decreasing condition here means that the letters are received in the correct order.

In computer science, DPLL(T) is a framework for determining the satisfiability of SMT problems. The algorithm extends the original SAT-solving DPLL algorithm with the ability to reason about an arbitrary theory T. At a high level, the algorithm works by transforming an SMT problem into a SAT formula where atoms are replaced with Boolean variables. The algorithm repeatedly finds a satisfying valuation for the SAT problem, consults a theory solver to check consistency under the domain-specific theory, and then (if a contradiction is found) refines the SAT formula with this information.

Murφ is an explicit-state model checker developed at Stanford University, and widely used for formal verification of cache-coherence protocols.

<span class="mw-page-title-main">Kenneth L. McMillan</span> American computer scientist

Kenneth L. McMillan is an American computer scientist working in the area of formal methods, logic, and programming languages. He is a professor in the computer science department at the University of Texas at Austin, where he holds the Admiral B.R. Inman Centennial Chair in Computing Theory.

In computer science and mathematical logic, Cooperating Validity Checker (CVC) is a family of satisfiability modulo theories (SMT) solvers. The latest major versions of CVC are CVC4 and CVC5 ; earlier versions include CVC, CVC Lite, and CVC3. Both CVC4 and cvc5 support the SMT-LIB and TPTP input formats for solving SMT problems, and the SyGuS-IF format for program synthesis. Both CVC4 and cvc5 can output proofs that can be independently checked in the LFSC format, cvc5 additionally supports the Alethe and Lean 4 formats. cvc5 has bindings for C++, Python, and Java.

References

  1. 1 2 "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. ↑ 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.
  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. ↑ 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.
  10. ↑ 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.
  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.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.