David L. Dill


David Lansing Dill (nacido el 8 de enero de 1957) es un científico informático y académico destacado por sus contribuciones a la verificación formal , la seguridad del voto electrónico y la biología de sistemas computacionales .

En 2013, Dill fue elegido miembro de la Academia Nacional de Ingeniería para el desarrollo de técnicas para verificar hardware, software y sistemas de votación electrónica.

Es profesor emérito de Donald E. Knuth en la Escuela de Ingeniería y profesor emérito de Ciencias de la Computación en la Universidad de Stanford .

Dill recibió una SB grado en Ciencias de la Computación e Ingeniería Eléctrica del Instituto de Tecnología de Massachusetts , Cambridge, MA , en 1979, un MS grado en Ciencias de la Computación de la Universidad Carnegie-Mellon , Pittsburgh, PA , en 1982, y un Ph.D. Licenciado en Ciencias de la Computación en 1987, también de la Universidad Carnegie-Mellon . Después de recibir su doctorado, se unió a la facultad del departamento de informática de la Universidad de Stanford , Stanford, California . [1] Se convirtió en profesor asociado en 1994 y profesor titular en 2000. En 2016 se convirtió en el primer receptor de la cátedra Donald E. Knuth , una cátedra en la Escuela de Ingeniería de la Universidad de Stanford . De julio de 1995 a septiembre de 1996, fue Científico Jefe en 0-In Design Automation (adquirido por Mentor Graphics en 2004) y, de 2016 a 2017, fue Científico Jefe en LocusPoint Networks, LLC. .

Los intereses de Dill incluyen el diseño de circuitos asincrónicos , la verificación de software y hardware , la demostración automática de teoremas , la seguridad del voto electrónico y la biología de sistemas computacionales . Su Ph.D. La disertación fue una contribución importante a la verificación de circuitos asincrónicos y fue publicada por MIT Press en 1989. [2] Contribuyó al desarrollo de la verificación de modelos simbólicos , ayudando a mejorar la escalabilidad de la técnica. [3]Poco después de llegar a Stanford, Dill y sus estudiantes desarrollaron el verificador de estado finito murphi, que luego se utilizó para verificar los protocolos de coherencia de la caché en multiprocesadores y CPU de varios fabricantes importantes de computadoras. [4] [5] Él y Rajeev Alur ampliaron la teoría clásica de los autómatas con relojes de valor real, inventando autómatas cronometrados . [6] En 1994, él y Jerry Burch publicaron un artículo influyente sobre la verificación de microprocesadores , inventando una técnica conocida como el método de verificación Burch-Dill. [7] También fue uno de los primeros en contribuir al campo de la investigación conocido como teorías de módulo de satisfacibilidad.(SMT), que supervisa el desarrollo de varios solucionadores SMT tempranos: el Comprobador de validez de Stanford (SVC), [8] el Comprobador de validez cooperante ( CVC ), [9] y el Comprobador de teoremas simple ( STP ). [10] Y contribuyó al desarrollo de una aplicación clave de solucionadores SMT para las pruebas de software conocidas como pruebas concólicas . [11]

En enero de 2003, Dill fue autor de la "Resolución sobre el voto electrónico", [12] que exige una pista de auditoría verificable por los votantes en todo el equipo de votación. La resolución ha sido respaldada por miles de personas, incluidos expertos en informática y seguridad y funcionarios electos. En julio de ese año, creó VerifiedVoting.org, y en febrero de 2004, fundó la Verified Voting Foundation, en cuya junta permanece. En mayo de 2004, realizó varias entrevistas con los medios sobre el tema, incluso con Lou Dobbs Tonight y Jim Lehrer . En abril de 2005, testificó ante la Comisión de Reforma Electoral Federal , copresidida por Jimmy Carter y James Baker., y en junio, testificó ante el Senado de los Estados Unidos . [1] [13]