David L. Dill

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.

Dill's interests include asynchronous circuit design, software and hardware verification, automatic theorem proving, electronic voting security, and computational systems biology.

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

[8] 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), [9] the Cooperating Validity Checker (CVC), [10] and the Simple Theorem Prover (STP).

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 2010, he received two test of time awards from the Logic in Computer Science conference (for papers published in LICS in 1990).

In 2024, he received a third Computer Aided Verification award with a group of researchers for the ReluPlex algorithm for verifying deep neural networks