David L. Dill - David L. Dill
David L. Dill | |
|---|---|
| Nascer | 8 de janeiro de 1957 |
| Nacionalidade |
 Estados Unidos
|
| Alma mater | Instituto de Tecnologia de Massachusetts |
| Prêmios |
Alonzo Church Award CAV Award EFF Pioneer Award |
| Carreira científica | |
| Orientador de doutorado | Edmund M. Clarke |
| Alunos notáveis | Rajeev Alur |
| Local na rede Internet | [1] |
David Lansing Dill (nascido em 8 de janeiro de 1957) é um cientista da computação e acadêmico conhecido por suas contribuições para a verificação formal , segurança de votação eletrônica e biologia de sistemas computacionais .
Em 2013, Dill foi eleito membro da National Academy of Engineering para o desenvolvimento de técnicas de verificação de hardware, software e sistemas de votação eletrônica.
Ele é o Donald E. Knuth Professor, Emérito, na Escola de Engenharia e Professor Emérito, de Ciência da Computação na Universidade de Stanford .
Biografia
Dill recebeu um diploma de SB em Ciência da Computação e Engenharia Elétrica do Massachusetts Institute of Technology , Cambridge, MA , em 1979, um diploma de MS em Ciência da Computação pela Carnegie-Mellon University , Pittsburgh, PA , em 1982, e um Ph.D. graduado em Ciência da Computação em 1987, também pela Carnegie-Mellon University . Depois de receber seu Ph.D., ingressou no corpo docente do departamento de ciência da computação na Universidade de Stanford , Stanford, CA . Ele se tornou um professor associado em 1994 e professor titular em 2000. Em 2016, ele se tornou o primeiro a receber o Donald E. Knuth Professorship, uma cadeira dotada na Escola de Engenharia da Universidade de Stanford . De julho de 1995 a setembro de 1996, ele foi Cientista Chefe da 0-In Design Automation (adquirida pela Mentor Graphics em 2004) e, de 2016 a 2017, foi Cientista Chefe da LocusPoint Networks, LLC. .
Trabalhos
Os interesses de Dill incluem projeto de circuito assíncrono , verificação de software e hardware , prova automática de teoremas , segurança de votação eletrônica e biologia de sistemas computacionais . Seu Ph.D. A dissertação foi uma contribuição importante para a verificação de circuitos assíncronos e foi publicada pela MIT Press em 1989. Ele contribuiu para o desenvolvimento da verificação de modelos simbólicos , ajudando a melhorar a escalabilidade da técnica. Logo depois de chegar a Stanford, Dill e seus alunos desenvolveram o verificador de estado finito murphi, que mais tarde foi usado para verificar protocolos de coerência de cache em multiprocessadores e CPUs de vários dos principais fabricantes de computadores. Ele e Rajeev Alur estenderam a teoria clássica dos autômatos com relógios de valor real, inventando autômatos cronometrados . Em 1994, ele e Jerry Burch publicaram um artigo influente sobre verificação de microprocessador , inventando uma técnica conhecida como método de verificação de Burch-Dill. Ele também foi um dos primeiros contribuintes para o campo de pesquisa conhecido como teorias do módulo de satisfatibilidade (SMT), supervisionando o desenvolvimento de vários solucionadores SMT iniciais: o Stanford Validity Checker (SVC), o Cooperating Validity Checker ( CVC ) e o Simple Theorem Prover ( STP ). E ele contribuiu para o desenvolvimento de uma aplicação chave de solucionadores SMT para teste de software conhecido como teste concólico .
Votação Eletrônica
Em janeiro de 2003, Dill foi o autor da "Resolução sobre Votação Eletrônica", que exige uma trilha de auditoria verificável pelo eleitor em todos os equipamentos de votação. A resolução foi endossada por milhares de pessoas, incluindo especialistas em informática e segurança e autoridades eleitas. Em julho daquele ano, criou o VerifiedVoting.org e, em fevereiro de 2004, fundou a Verified Voting Foundation, de cujo conselho permanece. Em maio de 2004, ele deu várias entrevistas à mídia sobre o assunto, incluindo Lou Dobbs Tonight e Jim Lehrer . Em abril de 2005, ele testemunhou perante a Comissão de Reforma Eleitoral Federal , co-presidida por Jimmy Carter e James Baker , e em junho, ele testemunhou perante o Senado dos Estados Unidos .
Reconhecimento profissional
Dill é membro da ACM e do IEEE . Sua dissertação ganhou o prêmio ACM Distinguished Dissertation em 1988 e, no mesmo ano, foi nomeado Jovem Investigador Presidencial . Ele recebeu os prêmios de melhor artigo na IEEE International Conference on Computer Design em 1991 e na Design Automation Conference em 1993 e 1998. Ele recebeu o Prêmio Pioneer da Electronic Frontier Foundation em 2004 por liderar e nutrir o movimento popular pela integridade e transparência na modernidade eleições. Em 2008, ele e Rajeev Alur receberam o prêmio Computer Aided Verification por contribuições fundamentais para a teoria da verificação de sistemas em tempo real . Em 2010, ele recebeu dois prêmios de teste de tempo da conferência Logic in Computer Science (para artigos publicados no LICS em 1990). Em 2013, foi eleito para a National Academy of Engineering e para a American Academy of Arts and Sciences . Em 2016, ele e Rajeev Alur receberam o Prêmio Igreja Alonzo por contribuições notáveis à lógica, do Grupo de Interesse Especial da ACM para Lógica e Computação (SIGLOG) , a Associação Europeia de Ciência da Computação Teórica (EATCS), a Associação Europeia de Lógica da Ciência da Computação (EACSL) e a Kurt Gödel Society (KGS). Também em 2016, ele recebeu um prêmio de teste de tempo da Conferência ACM sobre Segurança de Computadores e Comunicações.