David L. Dill

Professor of Computer Science. Played a key role in the development of today's industrial verification technology. Contributions include formal models, algorithms, and applications to the verification of real-world hardware and software systems. Created Murphi, a widely used explicit-state model checker. His formulation (with Alur) of timed automata created a model, now standard and suitable for verification by model checking, of systems operating under real-time constraints. Developed, with Burch, a technique for verifying the correctness of a pipelined microprocessor, showing that it produces the same results as an un-pipelined reference implantation, and spurring the development of automated decision procedures. Founded 0-in Design Automation and served as chief scientist guiding the company in the development of innovative approaches to inserting assertion-checking logic into circuit designs and using both simulation and formal verification to ensure the assertions hold. Helped make the security of electronic voting a national issue, and has been a leading advocate for ensuring that electronic voting systems produce verifiable results. Founded both the Verified Voting Foundation and VerifiedVoting.org.