David L. Dill

David L. Dill is a computer scientist and Professor Emeritus at Stanford University, best known for his foundational work on the formal verification of real-time and asynchronous systems. With Rajeev Alur, Dill developed the theory of timed automata in the early 1990s, providing the first decidable framework for verifying systems with quantitative timing constraints. The region construction — the key technical device that makes timed automata decidable — was developed in their collaboration.

Dill's broader contributions include work on asynchronous circuit verification, the development of the Murphi verification system, and research on electronic voting security. He has been a prominent advocate for verifiable voting systems, arguing that the integrity of democratic elections depends on the ability to verify the correctness of the systems that count votes.

Dill received his Ph.D. from Carnegie Mellon University and was a faculty member at Stanford from 1988 to 2016. He is a Fellow of the ACM and the IEEE.