David Boris Paul Déharbe

  • Endereço para acessar este CV: http://lattes.cnpq.br/2985658685449858
  • Última atualização do currículo em 07/02/2016


De nacionalidade francesa, é radicado no Brasil desde 1997, data na qual começou a desenvolver atividades profissionais na Universidade Federal do Rio Grande do Norte, onde atualmente é Professor Associado no Departamento de Informática e Matemática Aplicada. Atua na área de Ciência da Computação, com ênfase em Métodos Formais e Métodos Automáticos de Verificação Formal (model checking, SMT-solving). Realizou seus estudos no sistema francês de educação. A sua formação em nível de graduação divide-se em duas etapas: os dois primeiros anos foram realizados em um curso generalista de Ciências Exatas (opção matemática e física) na Université de Lorraine, e os dois anos seguintes foram realizados em um curso de Informática na Université de Grenoble. Obteve os diplomas "Diplôme d'Études Universitaires Générales - Sciences et Structures de la Matière" (Université de Nancy 1 - 1988) e "Maîtrise ès Sciences et Techniques - Expert en Systèmes Informatiques" (Université de Grenoble 1, 1990). Completou a sua formação em nível de pós-graduação com um D.E.A. Informatique (Institut National Polytechnique de Grenoble, 1991), correspondente ao Mestrado, seguido de um Doctorat En Informatique (Université de Grenoble I, 1996), correspondente ao Doutorado. Enquanto concluía seu doutoramento, e antes de se mudar para o Brasil, trabalhou como pesquisador visitante na Carnegie Mellon University entre 1995 e 1997, na equipe do Dr Edmund Clarke (co-recipiente do prêmio Turing para seu trabalho sobre model checking). (Texto informado pelo autor)


Identificação


Nome
David Boris Paul Déharbe
Nome em citações bibliográficas
DÉHARBE, D. B. P.;Déharbe, David

Endereço


Endereço Profissional
Universidade Federal do Rio Grande do Norte, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
Campus/UFRN
Lagoa Nova
59078970 - Natal, RN - Brasil
Telefone: (81) 32153814
Ramal: 224
Fax: (81) 8432153814
URL da Homepage: http://www.sigaa.ufrn.br/sigaa/public/docente/portal.jsf?siape=2220777


Formação acadêmica/titulação


1992 - 1996
Doutorado em Doctorat En Informatique.
Université Joseph Fourier - Grenoble I, UJF, França.
Título: Vérification formelle de propriétés temporelles:Étude et Application au Langage VHDL, Ano de obtenção: 1996.
Orientador: Dominique Borrione.
Bolsista do(a): Ministère de La Recherche Et de L'éducation Supérieure, M.R.E., França.
Palavras-chave: VERIFICACAO FORMAL; CAD DE CIRCUITOS INTEGRADOS; VHDL.
Grande área: Ciências Exatas e da Terra
Setores de atividade: Informática; Industria Eletro-Eletrônica.
1990 - 1991
Mestrado em D.E.A. Informatique.
Institut National Polytechnique de Grenoble, I.N.P.G., França.
Título: Model-checking symbolique de description de circuits dans le langage SMAX,Ano de Obtenção: 1991.
Orientador: Dominique Borrione.
Palavras-chave: VERIFICACAO FORMAL; CAD DE CIRCUITOS INTEGRADOS.
Grande área: Ciências Exatas e da Terra
Setores de atividade: Informática.
1988 - 1990
Graduação em M.S.T. Expert en Systèmes Informatiques.
Université Joseph Fourier - Grenoble I, UJF, França.


Pós-doutorado


2013 - 2014
Pós-Doutorado.
Laboratoire Lorrain de Recherche en Informatique et ses Applications, LORIA, França.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.
Grande área: Ciências Exatas e da Terra
2002 - 2003
Pós-Doutorado.
Laboratoire Lorrain de Recherche en Informatique et ses Applications, LORIA, França.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior, CAPES, Brasil.
Grande área: Ciências Exatas e da Terra


Formação Complementar


2012 - 2012
Functional Programming Principles in Scala. (Carga horária: 40h).
Coursera, COURSERA, Estados Unidos.


Atuação Profissional



Fundação de Apoio à Pesquisa do Estado do Rio Grande do Norte, FAPERN, Brasil.
Vínculo institucional

2011 - 2011
Vínculo: Colaborador, Enquadramento Funcional: Parecerista ad hoc, Carga horária: 0


Universidade Federal do Rio Grande do Norte, UFRN, Brasil.
Vínculo institucional

2010 - Atual
Vínculo: Servidor Público, Enquadramento Funcional: Professor Associado 2, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2008 - 2010
Vínculo: Servidor Público, Enquadramento Funcional: Professor Associado 1, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2006 - 2008
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto IV, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

1999 - 2006
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto I, Regime: Dedicação exclusiva.

Atividades

02/2012 - Atual
Ensino, Bacharelado em Engenharia de Software, Nível: Graduação

Disciplinas ministradas
Métodos Formais de Engenharia de Software
Conceitos e Técnicas de Programação
02/2012 - Atual
Extensão universitária , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Atividade de extensão realizada
Organizador local do SBMF 2012.
08/2011 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, .

Cargo ou função
Núcleo Docente Estruturante do Bacharelado em Ciência da Computação.
07/2010 - Atual
Direção e administração, Centro de Ciências Exatas, .

Cargo ou função
Vice-Coordenador do Programa de Pós-graduação em Sistemas e Computação.
02/2010 - Atual
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de seleção de workshops do CBSOFT 2011.
08/2005 - Atual
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê diretora da Maratona de Programação da SBC.
03/1999 - Atual
Pesquisa e desenvolvimento , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
02/2012 - 02/2012
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa ABZ 2012.
08/2011 - 12/2011
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação

Disciplinas ministradas
Prática de Conceitos e Técnicas de Programação
Conceitos e Técnicas de Programação
04/2011 - 06/2011
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa SBMF 2011.
04/2011 - 05/2011
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa ICTAC 2011.
07/2010 - 01/2011
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Seminários em Engenharia de Software
06/2010 - 07/2010
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação

Disciplinas ministradas
Introdução a Técnicas de Programação
02/2010 - 06/2010
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação

Disciplinas ministradas
Tópicos Especiais em Computação XIV (Treinamento para Competições de Programação)
Prática de Conceitos e Técnicas de Programação
Conceitos e Técnicas de Programação
02/2010 - 06/2010
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Estágio Docência em Computação 1
03/2010 - 05/2010
Extensão universitária , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Atividade de extensão realizada
Divulgação e realização das provas estaduais da OBI2010 (Olimpiada Brasileira de Informática).
03/2010 - 05/2010
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
SBMF 2010: Comitê de Programa.
03/2010 - 04/2010
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de programa iFM 2010.
08/2008 - 12/2008
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação

Disciplinas ministradas
Conceitos e Técnicas de Programação
Prática de Conceitos e Técnicas de Programação
08/2008 - 12/2008
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Estágio docência
Estudo orientado
06/2008 - 07/2008
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Membro do comitê de programa do LSFA 2008.
02/2008 - 07/2008
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação

Disciplinas ministradas
DIM0425 - Conceitos e Técnicas de Programação
02/2008 - 07/2008
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
DIM0805 - Especificações Formais (30 horas)
05/2008 - 06/2008
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Membro do comitê de programa do SBMF2008.
04/2008 - 05/2008
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Membro do comitê de programa do SBCCI 2008.
05/2006 - 04/2008
Direção e administração, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Vice-coordenador do Programa de Pós-graduação em Sistemas e Computação.
01/2008 - 02/2008
Ensino, Bach. em Ciência da Computação e Eng. Computação, Nível: Graduação

Disciplinas ministradas
DIM0410 - Treinamento para Competições de Programação
01/2008 - 02/2008
Extensão universitária , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Atividade de extensão realizada
Curso básico de C++ (organização).
08/2007 - 12/2007
Ensino, Engenharia de Computação, Nível: Graduação

Disciplinas ministradas
DIM0425 - Conceitos e Técnicas de Programação
08/2007 - 12/2007
Ensino, Bach. em Ciência da Computação e Eng. Computação, Nível: Graduação

Disciplinas ministradas
DIM0422 - Fundamentos Matemáticos da Computação
02/2007 - 08/2007
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
DIM0805 - Especificações formais (16 horas)
02/2007 - 07/2007
Ensino, Bacharelado em Ciência da Computação, Nível: Graduação

Disciplinas ministradas
DIM0410 - Treinamento para Competições de Programação
DIM0425 - Conceitos e Técnicas de Programação
08/2006 - 12/2006
Ensino, Bacharelado em Ciencias da Computacao, Nível: Graduação

Disciplinas ministradas
DIM0013: Estruturas de Dados
08/2006 - 12/2006
Ensino, Engenharia de Computação, Nível: Graduação

Disciplinas ministradas
DIM0324: Conceitos e Técnicas de Programação
08/2006 - 12/2006
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Estudo orientado
03/2006 - 09/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Organização local 3rd International Conference on Graph Transformation (ICGT 2006).
03/2006 - 09/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Organização local Brazilian Symposium on Formal Methods (SBMF2006).
06/2006 - 07/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa Brazilian Symposium on Formal Methods (SBMF2006).
06/2006 - 07/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa International Conference on Software and Data Technologies (ICSOFT 2006).
02/2006 - 07/2006
Ensino, Engenharia de Computação, Nível: Graduação

Disciplinas ministradas
DIM0324 - Conceitos e Técnicas de Programação
02/2006 - 07/2006
Ensino, Bach. em Ciência da Computação e Eng. Computação, Nível: Graduação

Disciplinas ministradas
DIM0096 - Tópicos Especiais em Computação VII
06/2006 - 06/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa GraBaTs 2006 (3rd International Workshop on Graph Based Tools).
04/2006 - 05/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa 3rd International Colloquium on Theoretical Aspects of Computing (ICTAC-2006).
03/2006 - 04/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa XX Simpósio Brasileiro de Engenharia de Software (SBES2006).
03/2006 - 04/2006
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa do Brazilian Symposium on Integrated Circuits and Design (SBCCI2006).
5/2004 - 4/2006
Direção e administração, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Vice-Coordenador do Programa de Pos-Graduacao.
09/2005 - 12/2005
Ensino, Bacharelado em Ciencias da Computacao, Nível: Graduação

Disciplinas ministradas
Estruturas de dados
09/2005 - 12/2005
Ensino, Engenharia de Computação, Nível: Graduação

Disciplinas ministradas
Conceitos e técnicas de programação
09/2005 - 12/2005
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Estudo orientado
01/2005 - 12/2005
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê diretor Brazilian Symposium on Formal Methods (SBMF2005).
07/2005 - 08/2005
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa SBMF 2005.
3/2005 - 07/2005
Ensino, Bacharelado em Ciencias da Computacao, Nível: Graduação

Disciplinas ministradas
Proposta de relatorio de graduação
Topicos avançados - Preparação a Maratona de Programação
3/2005 - 07/2005
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Especificações Formais
04/2005 - 05/2005
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa Brazilian Symp. Integrated Circuits and Systems (SBCCI2005).
04/2005 - 05/2005
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa Simpósio Brasileiro de Engenharia de Software (SBES2005).
04/2005 - 05/2005
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa IEEE Int'l Conf. Soft. Eng. and Formal Methods (SEFM 2005).
03/2005 - 04/2005
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Comitê de Programa Concurso Teses e Dissertações (CTD 2005).
9/2004 - 1/2005
Ensino, Bacharelado em Ciencias da Computacao, Nível: Graduação

Disciplinas ministradas
Estruturas de Dados
Laboratorio de Estruturas de Dados
9/2004 - 1/2005
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Topicos Avancados em Engenharia de Software II: Verificacao Formal
07/2004 - 10/2004
Outras atividades técnico-científicas , Centro de Ciências Exatas, Centro de Ciências Exatas.

Atividade realizada
Treinador para Maratona de Programação.
3/2004 - 8/2004
Ensino, Bacharelado em Ciencias da Computacao, Nível: Graduação

Disciplinas ministradas
Topicos avancados
3/2004 - 8/2004
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Especificacoes Formais
10/2003 - 2/2004
Ensino, Bacharelado em Ciencias da Computacao, Nível: Graduação

Disciplinas ministradas
Laboratório de estruturas de dados
Estruturas de dados
10/2003 - 2/2004
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Estudo individualizado
05/2003 - 07/2003
Ensino, Engenharia de Computação, Nível: Graduação

Disciplinas ministradas
Linguagens Formais
05/2003 - 07/2003
Ensino, Bacharelado em Ciencias da Computacao, Nível: Graduação

Disciplinas ministradas
Tópicos especiais em computação Preparação à maratona ACM de programação
Introdução à Ciência da Computação
05/2003 - 05/2003
Extensão universitária , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Atividade de extensão realizada
Organização local da Olimpiada Brasileira de Informática.
08/2001 - 02/2002
Direção e administração, Centro de Ciências Exatas, .

Cargo ou função
Coordenador de Programa de Pos-graduacao.
03/1999 - 02/2001
Direção e administração, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
COORDENACAO DOS LABORATORIOS DO DEPARTAMENTO.

Universite de Nancy Ii, U.N. II, França.
Vínculo institucional

2009 - 2009
Vínculo: Professor convidado, Enquadramento Funcional: Maître de Conférences, Carga horária: 40


Carnegie Mellon University, CMU, Estados Unidos.
Vínculo institucional

1995 - 1997
Vínculo: Pesquisador visitante, Enquadramento Funcional: Pesquisador visitante, Regime: Dedicação exclusiva.

Atividades

02/1995 - 01/1997
Pesquisa e desenvolvimento , School of Computer Science, .



Linhas de pesquisa


1.
Concepcao de sistemas digitais
2.
Model checking


Projetos de pesquisa


2011 - Atual
Estudo e desenvolvimento de ferramentas de verificação por análise estática para a validação em engenharia de software
Descrição: Programa Nacional de Pós-Doutorado..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (0) / Mestrado profissional: (0) / Doutorado: (0) .
Integrantes: David Boris Paul Déharbe - Coordenador / Anamaria Martins Moreira - Integrante / Umberto Souza da Costa - Integrante / Martín Alejandro Musicante - Integrante / Marcel Vinícius de Medeiros Oliveira - Integrante.Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Bolsa.
2010 - 2013
SMT-SAVeS: Verificação automática de software por resolução módulo teorias
Descrição: Cooperação bilateral França-Brasil financiada pelo CNPq e pelo INRIA..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Doutorado: (1) .
Integrantes: David Boris Paul Déharbe - Coordenador / Anamaria Martins Moreira - Integrante / Pascal Fontaine - Integrante / Diego Caminha Barbosa de Oliveira - Integrante / Marcel Vinícius de Medeiros Oliveira - Integrante / Stephan Merz - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro / Institut National de Recherche en Informatique et en Automatique - Siège - Auxílio financeiro.
2010 - 2013
Sistemas computacionais confiáveis: desenvolvimento e verificação
Descrição: Projeto de pesquisa submetido para renovação de bolsa de produtividade em pesquisa.
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) / Doutorado: (3) .
Integrantes: David Boris Paul Déharbe - Coordenador.
2010 - 2012
Confiabilidade e Segurança em Software Crítico Embarcado
Descrição: Projeto multi-institucional, coordenado pelo Prof. Augusto Sampaio (CIn-UFPE), fomentado através do edital MCT/CNPq No. 09/2010 - PDI. A parte relativa ao número de alunos envolvidos não foi preenchida..
Situação: Em andamento; Natureza: Pesquisa.
2007 - 2010
Prova automática de teoremas para o desenvolvimento de sistemas computacionais confiáveis
Descrição: Bolsas no País / Produtividade em Pesquisa - PQ - 2006.
Situação: Em andamento; Natureza: Pesquisa.
2007 - 2009
Desenvolvimento do Método B e Aplicação ao Projeto de Sistemas Embarcados Industriais
Descrição: O método B é um processo genêrico de desenvolvimento rigoroso de software, baseado em uma notação própria, com embasamento em lógica de primeira ordem com aritmética inteira e teoria dos conjuntos. Os principais passos são modelagem, refinamentos sucessivos e síntese de código. O método B ainda inclui, para cada passo, um conjunto de obrigações de prova que devem ser verificadas formalmente para garantir a coerência e a corretude dos mesmos. O projeto proposto visa continuar e integrar trabalhos anteriores do grupo, e desenvolver novas especializações do método B para sistemas embarcados industriais nas áreas de transporte ferroviário e cartões inteligentes. A principal meta do projeto é prover um ambiente integrado de desenvolvimento para o método B. Para alcançar essa meta, serão desenvolvidos trabalhos acadêmicos no sentido de identificar padrões de modelagem orientados a diferentes classes de sistemas embarcados, geração de casos de testes a partir de modelos, estender o método B para o nível de linguagem de assemblagem, e integrar o conceito de ajuste de interface (retrenchment). A construção dos componentes que vão compor esse ambiente será dirigida pelas necessidades de um parceiro industrial que utilizará as competências e os trabalhos do grupo para aplicar o método B no desenvolvimento de sistemas de software embarcado na área de transporte ferroviário. Em paralelo, iremos aperfeiçoar os trabalhos realizados no contexto do projeto Bsmart para desenvolvimento rigoroso de aplicações em cartões inteligentes..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Especialização: (0) / Mestrado acadêmico: (2) / Mestrado profissional: (0) / Doutorado: (1) .
Integrantes: David Boris Paul Déharbe - Coordenador / Anamaria Martins Moreira - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
Número de produções C, T & A: 3
2007 - 2009
Combinando Técnicas de Métodos Formais e Teste na Construção de Sistemas Embarcados de Tempo Real
Descrição: Neste projeto focaremos no uso combinado de métodos formais e técnicas de teste baseado em modelos para sistemas embarcados de tempo real. O principal objetivo é compartilhar conhecimentos e experiências para promover avanços conjuntos nesta área de pesquisa. Em particular, procuramos com este projeto promover o desenvolvimento tecnológico de qualidade de sistemas corretos e seguros. O projeto considerará as seguintes direções de pesquisa: (1) investigação de modelos de sistemas de software heterogêneos com características tais como não-determinismo, tempo e interrupção; (2) desenvolvimento de padrões de modelagem para sistemas embarcados utilizando formalismos baseados em estados e processos; (3)proposta de padrões de desenvolvimento baseado em refinamento de modelos baseados em estados e processos; (4) geração automática de código para hardware e software; (5) testes a partir de modelos parciais, considerando sua geração a partir de casos de teste abstratos e comportamento observável; (6) aprimoramento de técnicas atuais para a geração de casos de teste considerando critérios semânticos de cobertura além dos critérios de cobertura estrutural, bem como relações de conformidade pertinentes e critérios de cobertura de verificação de modelos; (7) investigação das relações de conformidade com base em falha e divergência em álgebras de processo; (8) proposta de estratégias para a seleção automática de casos de teste com base em funções de similaridade..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (2) / Doutorado: (2) .
Integrantes: David Boris Paul Déharbe - Coordenador / Anamaria Martins Moreira - Integrante / Augusto Cezar Alves Sampaio - Integrante / Paulo Henrique Monteiro Borba - Integrante / Alexandre Cabral Mota - Integrante / Marcel Vinícius de Medeiros Oliveira - Integrante / Juliano Manabu Iyoda - Integrante / Flávia de Almeida Barros - Integrante / Franklin de Souza Ramalho - Integrante / Marcelo Bezerra d'Amorim - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
2005 - 2008
Da Capo: Dedução Automatica e Prova de Correção de Componentes de Software
Descrição: Da Capo é um projeto conjunto a pesquisadores do LORIA e da UFRN, visando a melhoria do estado da arte na área de engenharia de software no tocante à aplicação de técnicas de verificação formal para aumentar a segurança e a confiabilidade das aplicações e componentes desenvolvidos. O projeto tem como alvo os casos onde a presença de falhas pode ser evidenciada através da satisfatibilidade de uma fórmula da lógica da primeira ordem, arbitrariamente complexa tanto em nível de aplicação de quantificadores quanto na sua estrutura booleana, em relação ainda uma teoria definindo a semântica dos operadores do domínio de aplicação. Essa problemática abrange uma larga gama de problemas de verificação de correção de componentes de software. Em particular, no projeto, estamos interessados em aplicar os resultados teóricos e as técnicas desenvolvidas aos seguintes domínios de aplicação: 1) Obrigações de prova geradas na aplicação da metodologia B de desenvolvimento de software, que são expressas em lógica da primeira ordem com aritmética e uma teoria definido operações sobre conjuntos; 2) Obrigações de prova geradas para garantir a correção de classes Java em relação a seus contratos expressos em JML, uma extensão da lógica da primeira ordem. Em particular, focaremos a nossa atenção para classes da plataforma JavaCard. 3) Obrigações de prova geradas para garantir a consistência semântica de extensões para dar maior suporte à modularidade em linguagens de especificação e de programação. Esse desafio motiva o nosso interesse em desenvolver técnicas e ferramentas de prova combinando flexibilidade e automação. A nossa abordagem é baseada na construção de pequenos motores de prova. A originalidade da nossa abordagem consiste em desenvolver uma metodologia de prova integrando técnicas de dedução automática, como o cálculo por superposição, procedimentos de decisão baseados em lógica de reescrita, e a combinação de tais procedimentos de decisão com procedimentos de satisfatibilidade p.
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Especialização: (0) / Mestrado acadêmico: (1) / Mestrado profissional: (0) / Doutorado: (1) .
Integrantes: David Boris Paul Déharbe - Coordenador / Anamaria Martins Moreira - Integrante / Christophe Ringeissen - Integrante / Silvio Ranise - Integrante / Pascal Fontaine - Integrante.Financiador(es): Institut National de Recherche en Informatique et en Automatique - Siège - Cooperação / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Cooperação.
Número de produções C, T & A: 8 / Número de orientações: 4
2005 - 2007
SMART: Engineering of Smart Card Applications (CNPq/CT-Info/PDPG-TI)
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (1) .
Integrantes: David Boris Paul Déharbe - Coordenador / Anamaria Martins Moreira - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
Número de produções C, T & A: 5
2004 - 2007
Um motor de dedução automatica incremental e produtor de prova
Descrição: O projeto proposto se enquadra no desenvolvimento de haRVey, um provador automático de teoremas, desenvolvido em cooperação entre a UFRN e o LORIA (Nancy, França). haRVey está atualmente sendo aplicado para a verificação de obrigações de prova geradas na metodologia B e a verificação de anotações JML em programas JavaCard. haRVey representa a estrutura proposicional de fórmulas lógicas, podendo incluir operadores aritméticos, usando diagramas de decisão binária (BDDs) ou um motor de satisfatibilidade baseado no algoritmo de David e Putnam melhorado(DPLL). O objetivo do projeto é estudar técnicas de prova na lógica da primeira ordem com igualdade (basicamente provas por saturação usando passos de paramodulação), e desenvolver um agente interativo de prova na lógica da primeira ordem com igualdade. Esse agente interativo poderá então ser integrado no provador de teoremas haRVey para melhorar a eficiência do mesmo. Através desse projeto, o aluno de IC receberá uma formação complementar muito forte na área de dedução automática e prova automática de teoremas e desenvolverá suas capacidades de programação e projeto de estruturas de dados. Serão também solicitados ao aluno seminários de andamento e participação na redação de artigos científicos sobre o seu trabalho, de forma a desenvolver suas capacidades de comunicação científica..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (1) / Especialização: (0) / Mestrado acadêmico: (0) / Mestrado profissional: (0) / Doutorado: (0) .
Integrantes: David Boris Paul Déharbe - Coordenador.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.
2004 - 2007
Ergo: Ferramentas para o desenvolvimento rigoroso de sistemas computacionais seguros e confiáveis
Descrição: O uso de sistemas computacionais embarcados tem sido cada vez mais usado como forma de aumentar o valor agregado dos mais diversos tipos de produtos. Porém seu uso em sistemas críticos põe a questão de sua correção. Muitas vezes, a validação de sistemas computacionais é realizada através de testes que, por mais elaborados que sejam, não podem ser exaustivos. Neste caso, complementarmente aos métodos tradicionais de verificação, o uso de métodos formais, matematicamente fundamentados, permite aumentar de forma drástica a robustez dos sistemas desenvolvidos. Se o potencial desses métodos já foi demonstrado em alguns casos, seu uso em escala industrial é barrado por limitações tecnológicas. Visamos nesse projeto prover ferramentas abertas permitindo certificar sistemas críticos complexos de forma automatizada. Uma metodologia geral de verificação de um sistema consiste em, dado sua descrição, gerar obrigações de prova cuja validade garantem a correção do mesmo. haRVey é um provador automático para lógicas equacionais da primeira ordem sem quantificadores. Posiciona-se como candidato, enquanto ferramenta de verificação formal, à inclusão em ambientes de projeto de sistemas computacionais críticos. O uso de haRVey para verificação de invariantes de especificações B já deu primeiros resultados encorajadores e está sendo extendida. Em particular, estão sendo investigadas aplicações de haRVey à verificação de programas Java (em particular JavaCard) anotados com JML De criação recente, haRVey demostrou ter flexibilidade, eficiência, e precisão comparável ou superior a ferramentas estabelecidas. Em primeiros experimentos, haRVey foi aplicado à verificação de programas C, de especificações formais baseada na teoria dos conjuntos (notação B), e de algoritmos sequenciais (Union Find). Uma das diretrizes que norteou o desenvolvimento de haRVey, que reusa de forma oportuna ferramentas de terceiros, foi o de adoptar sistemas com o seu código aberto. O projeto apresentado é constitu.
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Especialização: (0) / Mestrado acadêmico: (1) / Mestrado profissional: (0) / Doutorado: (0) .
Integrantes: David Boris Paul Déharbe - Coordenador / Jorgiano Márcio Bruno Vidal - Integrante.
2003 - 2005
Dedução automatica para analise formal de sistemas computacionais
Descrição: O uso de sistemas computacionais em aplicações críticas põe a questão de sua corretude. Muitas vezes, a validação de sistemas computacionais é realizada através de testes que, por mais elaborados que sejam, não são suficientes. Os métodos formais, matematicamente fundamentados, permitem garantir as propriedades de um sistema. Mas, se o potencial desses métodos já foi mostrado em alguns casos, seu uso em escala industrial é barrado por limitações tecnológicas, e requer mais pesquisa. A certificação de sistemas complexos é viável apenas se for automatizada. Portanto é estratégico desenvolver provadores capazes de lidar com a complexidade dos sistemas atuais. Este é o desafio desse projeto. haRVey é um provador automático para lógicas equacionais da primeira ordem sem quantificadores. Posiciona-se como candidato, enquanto ferramenta de verificação formal, à inclusão em ambientes de projeto de sistemas computacionais críticos. Em prática, dada uma fórmula F e uma teoria T, haRvey permite verificar que F é válida em T, combinando prova por casos e prova por refutação da forma seguinte: um BDD (diagrama de decisão binária) é utilizado para representar a negação de F: cada ramo do BDD corresponde a um caso que deve ser provado insatisfatível em T. Para cada ramo, a verificação da insatisfabilidade do mesmo é realizada por um provador por superposição. Caso o provador por superposição não chegue à clausula vazia, o ramo correspondente é satisfatível. Logo, a negação de F não é insatisfatível, e F não é válida (e o ramo pode ser utilizado para fornecer um contreexemplo). haRVey ainda aproveita cada prova por saturação para reduzir o conjunto dos casos remanescentes. De criação recente, haRVey demostrou ter flexibilidade, eficiência, e precisão comparável ou superior a ferramentas estabelecidas. Em primeiros experimentos, haRVey foi aplicado à verificação de programas C, de especificações formais baseada na teoria dos conjuntos (notação B), e de algoritmos sequenciais (Union.
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (3) / Mestrado acadêmico: (1) .
Integrantes: David Boris Paul Déharbe - Coordenador.Financiador(es): Universidade Federal do Rio Grande do Norte - Bolsa / Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.
Número de produções C, T & A: 8 / Número de orientações: 1


Membro de corpo editorial


2011 - 2012
Periódico: Theoretical Computer Science


Membro de comitê de assessoramento


2012 - 2012
Agência de fomento: Fundação Cearense de Apoio ao Desenvolvimento Científico e Tecnológico


Revisor de periódico


2008 - 2009
Periódico: Journal of Logic and Algebraic Programming
2011 - 2011
Periódico: International Journal on Software Tools for Technology Transfer (Print)
2009 - 2010
Periódico: Science of Computer Programming (Print)
2012 - Atual
Periódico: Software and Systems Modeling (Print)


Revisor de projeto de fomento


2013 - Atual
Agência de fomento: Conselho Nacional de Desenvolvimento Científico e Tecnológico


Áreas de atuação


1.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Métodos formais.
2.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Engenharia de Software.
3.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Lógicas e Semântica de Programas.


Idiomas


Francês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Português
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.


Prêmios e títulos


2014
First Prize in the error-free multi-division competition, SMT-COMP.
2013
Conferencista Sênior (Métodos Formais), Sociedade Brasileira de Computação.
2006
Medalha de prata na Maratona de Programação (5º lugar), Sociedade Brasileira de Computação.
2006
Trabalho selecionado entre os três melhores artigos para submissão ao IEEE Design & Test of Computers, XIX Brazilian Symposium on Integrated Circuits and Systems Design (SBCCI 2006).
2005
Best Paper Award, Brazilian Symposium on Formal Methods (SBMF2005).
2004
Medalha de Bronze - Décimo Lugar da Maratona de Programação (Coach), Sociedade Brasileira de Computação.
2003
Best Paper Award, VI Workshop Brasileiro de Metodos Formais: WMF2003 (SBC).
2000
Segundo lugar no Concurso de Trabalho de Iniciação Científica (como orientador), Sociedade Brasileira de Computação.


Produções



Produção bibliográfica
Artigos completos publicados em periódicos

1.
COK, D.2016COK, D. ; DÉHARBE, D. B. P. ; WEBER, T. . The 2014 SMT Competition. Journal on Satisfiability, Boolean Modeling and Computation, v. 9, p. 207-242, 2016.

2.
Déharbe, David2014Déharbe, David; Fontaine, Pascal ; GUYOT, YOANN ; VOISIN, LAURENT . Integrating SMT solvers in Rodin. Science of Computer Programming (Print), v. 94, p. 130-143, 2014.

3.
MEDEIROS, VALÉRIO2014MEDEIROS, VALÉRIO ; Déharbe, David . BEval: A Plug-in to Extend Atelier B with Current Verification Technologies. Electronic Proceedings in Theoretical Computer Science, v. 139, p. 53-58, 2014.

4.
Déharbe, David2013Déharbe, David. Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming (Print), v. 78, p. 310-326, 2013.

5.
de Oliveira, Diego Caminha B.2012de Oliveira, Diego Caminha B. ; Déharbe, David ; Fontaine, Pascal . Combining decision procedures by (model-)equality propagation. Science of Computer Programming (Print), v. 77, p. 518-532, 2012.

6.
Bouton, T.2012Bouton, T. ; OLIVEIRA, D. C. B. ; DÉHARBE, D. B. P. ; FONTAINE, P. . GridTPT: a distributed platform for Theorem Prover Testing. Easychair Proceedings in Computing, v. 9, p. 33-39, 2012.

7.
DÉHARBE, D. B. P.;Déharbe, David2009DÉHARBE, D. B. P.; RANISE, S. . Satisfiability solving for software verification. International Journal on Software Tools for Technology Transfer, v. 11, p. 255-260, 2009.

8.
DANTAS, B. P.2009DANTAS, B. P. ; DÉHARBE, D. B. P. ; GALVAO, S. S. L. ; MOREIRA, A. M. ; GUTEMBERG, Valério . Verified Compilation and the B Method: A Proposal and a First Appraisal. Electronic Notes in Theoretical Computer Science, v. 240, p. 76-96, 2009.

9.
DÉHARBE, D. B. P.;Déharbe, David2008DÉHARBE, D. B. P.; RANISE, S. ; VIDAL, J. M. B. . A prototype implementation of a distributed Satisfiability Modulo Theories solver in the ToolBus framework. Journal of the Brazilian Computer Society (Impresso), v. 14, p. 71-86, 2008.

10.
DÉHARBE, D. B. P.;Déharbe, David2007DÉHARBE, D. B. P.; RANISE, S. ; VIDAL, J. M. B. . Distributing the Workload in a Lazy Theorem Prover. Electronic Notes in Theoretical Computer Science, v. 184, p. 21-37, 2007.

11.
GOMES, B.E.G.2007GOMES, B.E.G. ; MOREIRA, A. M. ; DÉHARBE, D. B. P. . Developing Java Card Applications with B. Electronic Notes in Theoretical Computer Science, v. 184, p. 81-96, 2007.

12.
DÉHARBE, D. B. P.;Déharbe, David2006DÉHARBE, D. B. P.; MOREIRA, A. M. ; SENA, D. . Agraphs: Definition, implementation and tools. Electronic Communications of the EASST, v. 1, p. 2, 2006.

13.
2005CAMPOS, Sergio Vale Aguiar ; VIEIRA, Newton ; DÉHARBE, D. B. P. . Explicit-Symbolic Modelling for Formal Verification. Electronic Notes in Theoretical Computer Science, v. 130, p. 301-321, 2005.

14.
MOREIRA, A. M.2004MOREIRA, A. M. ; RINGEISSEN, C. ; DÉHARBE, D. B. P. ; LIMA, G. . Evolving algebraic specifications with term-based and graph-based representations. Journal of Logic and Algebraic Programming, v. 59, n.1/2, p. 63-87, 2004.

15.
COUCHOT, J.2004COUCHOT, J. ; DADEAU, F. ; DÉHARBE, D. B. P. ; GIORGETTI, A. ; RANISE, S. . Proving and debugging set-based specifications. Electronic Notes in Theoretical Computer Science, v. 95, p. 189-208, 2004.

16.
RANISE, S.2003RANISE, S. ; DÉHARBE, D. B. P. . Applying light-weight theorem proving for debugging and verifying pointer manipulating programs.. Electronic Notes in Theoretical Computer Science, v. 86, p. 1-15, 2003.

17.
GIORGETTI, A.2003 GIORGETTI, A. ; COUCHOT, J. ; DÉHARBE, D. B. P. ; RANISE, S. . Scalable Automated Proving and Debugging of Set-Based Specifications. Journal of the Brazilian Computer Society, v. 9, n.2, p. 17-36, 2003.

18.
DANTAS, B. P.2000DANTAS, B. P. ; DÉHARBE, D. B. P. ; PAULA, V. C. C. . An Architectural Description of Enterprise Java Beans. Electronic Notes in Theoretical Computer Science, v. 38, p. 1-14, 2000.

19.
MOREIRA, A. M.2000MOREIRA, A. M. ; DÉHARBE, D. B. P. ; RIBEIRO, L. ; RODRIGUES, V. M. . Introdução a Métodos Formais: Especificação, Semântica e Verificação de Sistemas Concorrentes. Revista de Informática Teórica e Aplicada, v. 7, n.1, p. 7-48, 2000.

20.
DÉHARBE, D. B. P.;Déharbe, David1995DÉHARBE, D. B. P.; BORRIONE, D. . Symbolic Model Checking of VHDL Design Entities with Past and Future Modalities. CURRENT ISSUES IN ELECTRONIC MODELLING, v. 1, p. 105-126, 1995.

Livros publicados/organizados ou edições
1.
CAVALCANTI, A. L. C. (Org.) ; DÉHARBE, D. B. P. (Org.) ; GAUDEL, M.-C. (Org.) ; WOODCOCK, J. (Org.) . Theoretical Aspects of Computing. 1. ed. Berlim: Springer, 2010. v. 1. 397p .

2.
DÉHARBE, D. B. P.; SOUZA NETO, P. A. (Org.) ; DANTAS, B. P. (Org.) ; MENDES NETO, F. M. (Org.) . Escola Potiguar de Computação e suas Aplicações - EPOCA 2008 Minicursos selecionados. 1. ed. Natal, RN: EDUFRN, 2009. v. 1. 112p .

3.
MARTINI, A. (Org.) ; DÉHARBE, D. B. P. (Org.) . WMF2002 - Proceedings of V Workshop on Formal Methods. 1. ed. , 2002. v. 1. 242p .

Capítulos de livros publicados
1.
DÉHARBE, D. B. P.. Techniques for Temporal Logic Model Checking. In: CAVALCANTI, A.; SAMPAIO, A.; WOODCOCK, J.. (Org.). Refinement Techniques in Software Engineering. Berlin Heidelberg: Springer, 2006, v. 3167, p. 315-367.

2.
DÉHARBE, D. B. P.. A tutorial introduction to symbolic model checking. In: Ruy J.G.B. de Queiroz. (Org.). Logic for Concurrency and Synchronisation. 1ed.: Kluwer Academic Publisher, 2003, v. 1, p. 135-158.

Trabalhos completos publicados em anais de congressos
1.
MOREIRA, A. M. ; HENTZ, C. ; Déharbe, David ; MATOS, E. ; GUTEMBERG, Valério . Verifying Code Generation Tools for the B-Method Using Tests: A Case Study.. In: Tests and Proofs, 2015, L'Aquila. Tests and Proofs, 9th International Conference, TAP 2015. Berlin: Springer, 2015. v. 9154. p. 76-91.

2.
DÉHARBE, D. B. P.; MERZ, S. . Software Component Design with the B Method - A Formalization in Isabelle/HOL.. In: Formal Aspects of Component Software ? FACS 2015, 2015, Niteroi, RJ. Formal Aspects of Component Software - 12th International Conference, FACS 2015, Niterói, Brazil, October 14-16, 2015, Revised Selected Papers.. Berlin: Springer, 2015. v. 9539. p. 31-47.

3.
BONICHON, R. ; Déharbe, David ; TAVARES, C. F. O. K. . Extending SMT-LIB v2 with λ-Terms and Polymorphism. In: 12th International Workshop on Satisfiability Modulo Theories (SMT 2014), 2014, Vienna, Austria. Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014. v. 1163. p. 53-62.

4.
BONICHON, R. ; Déharbe, David ; LECOMTE, T. ; GUTEMBERG, Valério . LLVM-Based Code Generation for B. In: 17th Brazilian Symposium on Formal Methods, 2014, Maceió, AL. Formal Methods: Foundations and Applications. Berlim: Springer, 2014. v. 8941. p. 1-16.

5.
DÉHARBE, D. B. P.; FONTAINE, P. ; LE BERRE, D. ; MAZURE, B. . Computing prime implicants. In: International Conference on Formal Methods in Computer-Aided Design, 2013, Portland. International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), 2013. p. 46-52.

6.
GUTEMBERG, Valério ; DÉHARBE, D. B. P. . B-Eval: a plug-in to extend Atelier-B with current verification technologies. In: Latin American Workshop on Formal Methods (LAFM), 2013, Buenos Aires. Latin American Workshop on Formal Methods (LAFM 2013), 2013. p. 1-6.

7.
Déharbe, David; FONTAINE, P. ; GUYOT, Y. ; VOISIN, L. . SMT solvers for Rodin. In: ABZ, 2012, Pisa, Italy. Abstrasct State Machines, Alloy, B, VDM, and Z. Berlin: Springer, 2012. v. 7316. p. 194-207.

8.
BARBOSA, H. M. ; Déharbe, David . An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. In: 15th Brazilian Symposium on Formal Methods (SBMF 2012), 2012, Natal. Formal Methods: Foundations and Applications - 15th Brazilian Symposium, SBMF 2012. Berlin: Springer, 2012. v. 7498. p. 19-34.

9.
DÉHARBE, D. B. P.; FONTAINE, P. ; MERZ, S. ; WOLZENLOGEL PALEO, B. . Exploiting Symmetry in SMT Problems. In: 23rd International Conference on Automated Deduction, 2011, Wroklaw. CADE 2011. Berlim: Springer, 2011. v. 6803. p. 222-236.

10.
OLIVEIRA, M. V. M. ; Déharbe, David ; CRUZ, L. . B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. In: Brazilian Symposium on Formal Methods (SBMF), 2011, São Paulo, Brazil. Formal Methods, Foundations and Applications. Berlin: Springer, 2011. v. 7021. p. 44-59.

11.
GOMES, B.E.G. ; DÉHARBE, D. B. P. ; MOREIRA, A. M. ; MORAES, K. K. O. . Applying the B method for the Rigorous Development of Smart Card Applications. In: ABZ 2010, 2010, Orford, QC, Canadá. Abstract State Machines, Alloy, B and Z. Berlim: Springer, 2010. v. 5977. p. 203-216.

12.
DÉHARBE, D. B. P.. Automatic Verification of a Class of Proof Obligations with SMT-Solvers. In: ABZ 2010, 2010, Orford, QC, Canadá. Abstract State Machines, Alloy, B and Z. Berlim: Springer, 2010. v. 5977. p. 217-230.

13.
Bouton, T. ; OLIVEIRA, D. C. B. ; DÉHARBE, D. B. P. ; FONTAINE, P. . veriT: An Open, Trustable and Efficient SMT-Solver. In: 22nd International Conference on Automated Deduction, 2009, Montreal, Canada. Automated Deduction ? CADE-22. Heidelberg: Springer, 2009. v. 5663. p. 151-156.

14.
DÉHARBE, D. B. P.; FONTAINE, P. ; MERZ, S. ; MOREIRA, A. M. ; OLIVEIRA, A. S. . Automating model-based software engineering. In: COLIBRI - Colóquio em Informática: Brasil / INRIA, Cooperações, Avanços e Desafios, 2009, Bento Gonçalves. COLIBRI, 2009. p. 22-27.

15.
DÉHARBE, D. B. P.; GALVAO, S. S. L. ; MOREIRA, A. M. . Formalizing FreeRTOS: First Steps. In: 12th Brazilian Symposium on Formal Methods, 2009, Gramado. Formal Methods: Foundations and Applications. Berlin: Springer, 2009. v. 5902. p. 101-117.

16.
OLIVEIRA, A. S. ; DÉHARBE, D. B. P. ; MOREAU, P.-E. . Vérification automatique des systèmes à base de règles avec le narrowing stratégique. In: COLIBRI 2009, 2009, Bento Gonçalves, RS. COLIBRI - Colóquio em Informática: Brasil / INRIA, Cooperações, Avanços e Desafios. Porto Alegre, RS: Sociedade Brasileira de Computação ? SBC, 2009. v. 1. p. 28-32.

17.
DANTAS, B. P. ; DÉHARBE, D. B. P. ; GALVAO, S. S. L. ; MOREIRA, A. M. ; GUTEMBERG, Valério . Proposta e Avaliação de uma Abordagem de Desenvolvimento de Software Fidedigno por Construção com o Método B. In: XXXV Seminário Integrado de Software e Hardware (SEMISH 2008), 2008, Belém, PA. Anais do XXXV Seminário Integrado de Software e Hardware (SEMISH 2008), 2008. v. 1. p. 1-15.

18.
OLIVEIRA, D. C. B. ; DÉHARBE, D. B. P. ; FONTAINE, P. . Combining decision procedures by (model-)equality propagation. In: Brazilian Symposium on Formal Methods (SBMF2008), 2008, Salvador, BA. Brazilian Symposium on Formal Methods (SBMF2008) - Proceedings. Salvador, BA: Editora Gráfica da UFBA - EDUFBA, 2008. v. 1. p. 51-66.

19.
DÉHARBE, D. B. P.. Applying the B method to take on the grand challenge of verified compilation. In: Brazilian Symposium on Formal Methods (SBMF2008), 2008, Salvador, BA. Brazilian Symposium on Formal Methods (SBMF2008) - Proceedings. Salvador, BA: Editora Gráfica da UFBA - EDUFBA, 2008. v. 1. p. 35-50.

20.
DÉHARBE, D. B. P.; MOREIRA, A. M. ; MUNIZ SILVA, P.S. ; Russo Jr, A. . Modelling Control Systems in B: an Industrial Case Study. In: Brazilian Symposium on Formal Methods (SBMF2007), 2007, Ouro Preto. Brazilian Symposium on Formal Methods (SBMF2007). Ouro Preto: SBC/Universidade Federal de Ouro Preto, 2007. v. 1. p. 112-127.

21.
DÉHARBE, D. B. P.; GOMES, B.E.G. ; MOREIRA, A. M. . Automation of Java Card Component Development Using the B Method. In: 11th International Conference on Engineering of Complex Computer Systems, 2006, Stanford, CA. Proceedings Eleventh International Conference on Engineering of Complex Computer Systems. Los Alamitos: IEEE Computer Society. v. 1. p. 259-268.

22.
DÉHARBE, D. B. P.; MEDEIROS, S. Q. . Aspect-Oriented Design in SystemC: Implementation and Applications. In: 19th Brazilian Symposium on Integrated Circuits and System Design, 2006, Ouro Preto, MG. Proceedings of the Nineteenth Brazilian Symposium on Integrated Circuits and System Design (SBCCI2006). p. 1-6.

23.
DÉHARBE, D. B. P.; FONTAINE, P. ; RANISE, S. ; RINGEISSEN, C. . Decision Procedures for the Formal Analysis of Software. In: Theoretical Aspects of Computing---ICTAC 2006, 2006, Tunis. Proc. 3rd Int'l Conf. Theoretical Aspects of Computing. Berlin: Springer, 2006. p. 366-370.

24.
DÉHARBE, D. B. P.; RANISE, S. . Satisfiability Solving for Software Verification. In: IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, 2005, Columbia, MD, USA. IEEE ISoLA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation, 2005. p. 1-16.

25.
GOMES, Í. H. S. ; SOUZA FILHO, G. L. ; DÉHARBE, D. B. P. . tVoice: Um Sistema de Manipulação de Linguagens para Auxiliar Portadores de Necessidades Especiais através da Web. In: WebMedia 2005, 2005, Poços de Caldas. XI Simpósio Brasileiro de Multimídia e Web - WebMedia 2005, 2005. v. 1. p. 129-144.

26.
DÉHARBE, D. B. P.; VIDAL, J. M. B. ; RANISE, S. . Distributing the Workload in a Lazy Theorem-Prover. In: Brazilian Symposium on Formal Methods - SBMF 2005, 2005, Porto Alegre. Brazilian Symposium on Formal Methods - SBMF2005, 2005. v. 1. p. 17-31.

27.
GOMES, B.E.G. ; MOREIRA, A. M. ; DÉHARBE, D. B. P. . Developing Java Card Applications with B. In: Brazilian Symposium on Formal Methods - SBMF2005, 2005, Porto Alegre. Brazilian Symposium on Formal Methods - SBMF2005. Porto Alegre: SBC/Instituto de Informatica da UFRGS, 2005. v. 1. p. 63-77.

28.
SILVA, A. A. V. V. ; DÉHARBE, D. B. P. ; SILVA, Ivan Saraiva ; CARRO, L. . Considerações sobre especificação e verificação formal de sistemas embarcados utilizando JML. In: X Workshop Iberchip, 2004, Cartagena de Indias. X IBERCHIP Workshop (IWS'2004), 2004. p. 11-20.

29.
DÉHARBE, D. B. P.; IMINE, A. ; RANISE, S. . Abstraction-Driven Verification of Array Programs. In: Artificial Intelligence and Symbolic Computation, 2004, Linz, Austria. Proceedings of 7th International Conference on Artificial Intelligence and Symbolic Computation, 2004. v. 3249. p. 271-275.

30.
COSTA, U. S. ; CAMPOS, Sergio Vale Aguiar ; DÉHARBE, D. B. P. ; VIEIRA, Newton . Explicit-symbolic model checking for formal verification. In: Simpósio Brasileiro de Métodos Formais, 2004, Recife, PE. Anais do Simpósio Brasileiro de Métodos Formais (SBMF'2004), 2004. p. 217-232.

31.
DÉHARBE, D. B. P.; RANISE, S. . Light-weight theorem proving for debugging and verifying pointer manipulating programms. In: 4th International Workshop on First-Order Theorem Proving (FTP'2003), 2003, Valencia. Proceedings of the 4th International Workshop on First-Order Theorem Proving. Valencia: Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, 2003. v. 1. p. 119-131.

32.
DÉHARBE, D. B. P.; RANISE, S. . Light-weight theorem proving for debugging and verifying units of code. In: IEEE International Conference on Software Engineering and Formal Methods, 2003, Brisbane. Proceeding of the 1st IEEE International Conference on Software Engineering and Formal Methods (SEFM 2003), 2003. v. 1. p. 220-228.

33.
COUCHOT, J. ; DADEAU, F. ; DÉHARBE, D. B. P. ; GIORGETTI, A. ; RANISE, S. . Proving and debugging set-based specifications. In: VI Workshop Brasileiro de Métodos Formais (WMF'2003), 2003, Campina Grande, PB. Anais do VI Workshop Brasileiro de Métodos Formais (WMF'2003), 2003. v. 1. p. 137-151.

34.
LEITE, J. C. ; DÉHARBE, D. B. P. ; LOPES, A. B. ; GOUVEA, E. F. ; CERQUEIRA, N. T. . Flexibilidade e Transversalidade no Projeto Pedagógico para o Curso de Ciência da Computação na UFRN. In: Workshop de Educacao em Informatica (WEI'2002), 2002, Florianopolis, SC. Anais do XXII Congresso da SBC. Porto Alegre, RS: Sociedade Brasileira de Computacao, 2002. v. 1. p. 741-752.

35.
DÉHARBE, D. B. P.; MOREIRA, A. M. ; RINGEISSEN, C. . Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. In: Conference on Rewriting Techniques and Application (RTA 2002), 2002, Cpenhagen, Dinamarca. Conference on Rewriting Techniques and Applications (RTA 2002). Berlin: Springer Verlag, 2002. p. 1-15.

36.
COSTA, U. S. ; MOREIRA, A. M. ; DÉHARBE, D. B. P. . Advances in BDD reduction using Parallel Genetic Algorithms. In: IEEE 10th International Workshop on Logic & Synthesis, 2001, Granlibakken, CA (E.U.A.). Proceedings of the IEEE 10th International Workshop on Logic & Synthesis (IWLS'2001), 2001. v. 1. p. 84-89.

37.
DÉHARBE, D. B. P.; VIDAL, J. M. B. . Optimizing BDD-based verification analysing variable dependencies. In: Symposium on Integrated Circuits and System Design, 2001, Pirenópolis, GO. XIV Symposium on Integrated Circuits and System Design, 2001. v. 1. p. 1-6.

38.
MEDEIROS, S. Q. ; DÉHARBE, D. B. P. . BDDmeter - Uma Ferramenta para Visualização Dinâmica de BDDs. In: Simpósio Brasileiro de Engenharia de Software, 2001, Rio de Janeiro, RJ. Anais do XVI Simpósio Brasileiro de Engenharia de Software (SBES'2001), 2001. v. 1. p. 1-6.

39.
DÉHARBE, D. B. P.; DANTAS, B. P. ; PAULA, V. C. C. . Uma Descrição ZCL para a Arquitetura de Componentes Enterprise JavaBeans. In: Simpósio Brasileiro de Linguagens de Programação, 2000, Recife, Pe. IV Simpósio Brasileiro de Linguagens de Programação: SBLP'2000. Recife, PE: Editora Universitária UFPE, 2000. p. 158-171.

40.
COSTA, U. S. ; MOREIRA, A. M. ; DÉHARBE, D. B. P. . A cache-based parallel genetic algorithm for the BDD variable ordering problem. In: XII Simpósio Brasileiro de Arquiteturas de Computadores e Processamento de Alto Desempenho (SBAC-PAD'2000), 2000, São Carlos, SP. Anais do XII Simpósio Brasileiro de Arquiteturas de Computadores e Processamento de Alto Desempenho, 2000. v. 1. p. 99-105.

41.
DÉHARBE, D. B. P.; MOREIRA, A. M. . Symbolic Model Checking with Fewer Fixpoint Computations. In: World Congress on Formal Methods in the Development of Computing Systems, 1999, Toulouse, França. FM'99 Formal Methods. Berlin Heidelberg: Springer Verlag, 1999. v. 1708. p. 272-288.

42.
DÉHARBE, D. B. P.. Uma abordagem modular na verificação de descrições de hardware. In: Workshop de Métodos Formais, 1999, Florianópolis, SC. WMF'99 Second Workshop on Formal Methods, 1999. v. 1.

43.
DÉHARBE, D. B. P.; SHANKAR, S. ; CLARKE JR, E. M. . Model Checking VHDL with CV. In: Formal Methods in Circuit Automation Design, 1998, Palo Alto, California. FMCAD'98: Formal Methods in Circuit Automation Design. Berlin, Heidelberg: Springer Verlag, 1998.

44.
DÉHARBE, D. B. P.; SHANKAR, S. ; CLARKE JR, E. M. . Formal Verification of VHDL: The Model Checker CV. In: BRAZILIAN SYMPOSIUM ON INTEGRATED CIRCUIT DESIGN, 1998, BUZIOS, RN, BRAZIL. SBCCI98: XI BRAZILIAN SYMPOSIUM ON INTEGRATED CIRCUIT DESIGN: SBCCI'98. Los Alamitos, California: IEEE Computer Society, 1998. p. 95-98.

45.
DÉHARBE, D. B. P.. Slicing: A Novel Application for BDD-Based Modeling of VHDL. In: I Workshop Brasileiro de Métodos Formais: WMF'98, 1998, Porto Alegre, RS, 1998. p. 117-124.

46.
DÉHARBE, D. B. P.; SHANKAR, S. ; CLARKE JR, E. M. . Model Checking VHDL with CV. In: I Workshop Brasileiro de Métodos Formais: WMF'98, 1998, Porto Alegre, RS, 1998. p. 135-140.

47.
DÉHARBE, D. B. P.; MOREIRA, A. M. . Using Induction and BDDs to Model Check Invariants. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 1997, Montréal, Québec, Canadá. Advances in Hardware Design and Verification - CHARME'97, 1997. p. 203-213.

48.
BOUAMAMA, H. ; BORRIONE, D. ; DÉHARBE, D. B. P. ; LEFAOU, C. ; WAHBA, A. . HDL-Based integration of formal methods and CAD tools in the PREVAIL environment. In: Conference on Formal Methods in Circuit Automation Design, 1996, Palo Alto, California. FMCAD'96: Formal Methods in Circuit Automation Design. Berlin, Heidelberg: Springer Verlag, 1996. v. 1166.

49.
DÉHARBE, D. B. P.; BORRIONE, D. . Semantics of a verification-oriented subset of VHDL. In: IFIP WG10.5 Advanced Research Working Conference Correct Hardware Design and Verification Methods, 1996, FRANKFURT, ALEMANHA. CHARME'95: Correct Hardware Design and Verification Methods. Berlin Heidelberg: Springer Verlag, 1996. v. 987. p. 293-310.

50.
DÉHARBE, D. B. P.. Model checking on finite-state machines: extensions and applications to VHDL Designs. In: First Asian-Pacific Conference on Hardware Description Languages: Standards and Applications, 1993, Brisbane, Austrália. APCHDLSA'93:, 1993.

Resumos expandidos publicados em anais de congressos
1.
ARECES, C. ; Déharbe, David ; FONTAINE, P. ; ORBE, E. . SyMT: finding symmetries in SMT formulas. In: 11th International Workshop on Satisfiability Modulo Theories (SMT), 2013, Helsinki. Proc. of 11th International Workshop on Satisfiability Modulo Theories, 2013. v. 1. p. 56-63.

2.
BARBOSA, H. M. ; Déharbe, David . Formal Verification of PLC Programs Using the B Method. In: ABZ, 2012, Pisa, Italy. Abstract State Machines, Alloy, B, VDM, and Z. Berlin: Springer, 2012. v. 7316. p. 353-356.

3.
DÉHARBE, D. B. P.; FONTAINE, P. ; WOLZENLOGEL PALEO, B. . Quantifier Inference Rules for SMT proofs. In: First Workshop on Proof eXchange for Theorem Proving - PxTP 2011, 2011, Wroklaw. Proceedings PxTP 2011, 2011. p. 1-7.

4.
GURGEL, A. ; GUTEMBERG, Valério ; OLIVEIRA, M. V. M. ; DÉHARBE, D. B. P. . Integrating SMT-Solvers in Z and B Tools. In: ABZ 2010, 2010, Orford, QC, Canadá. Abstract State Machines, Alloy, B and Z. Berlim: Springer, 2010. v. 5977. p. 412-413.

5.
GUTEMBERG, Valério ; DÉHARBE, D. B. P. . Formal Modelling of a Microcontroller Instruction Set in B. In: Brazilian Symposium on Formal Methods, 2009, Gramado. Formal Methods: Foundations and Applications. Berlin: Springer, 2009. v. 5902. p. 282-289.

6.
DÉHARBE, D. B. P.; GOMES, B.E.G. ; MOREIRA, A. M. . BSmart: A Tool for the Development of Java Card Applications with the B Method. In: ABZ 2008, 2008, Londres. Abstract State Machines, B and Z, 2008. v. 5238. p. 351-352.

7.
GOMES, B.E.G. ; MOREIRA, A. M. ; DÉHARBE, D. B. P. ; MORAES, K. K. O. . A Ferramenta BSmart para o Desenvolvimento Rigoroso de Aplicações JavaCard com o Método Formal B. In: Sessão de Ferramentas do SBES 2007, 2007, João Pessoa. Simpósio Brasileiro de Engenharia de Software: Sessão de Ferramentas. João Pessoa: UFPB/BC, 2007. v. 1. p. 11-17.

8.
DÉHARBE, D. B. P.; FONTAINE, P. . haRVey: combining reasoners. In: Sixth International Workshop on Automated Verification of Critical Systems, 2006, Nancy. Proc. 6th Int'l Workshop on Automated Verification of Critical Systems (AVOCS'06). Nancy, França: LORIA, 2006. v. 1. p. 1-5.

9.
LIMA, G. ; MOREIRA, A. M. ; DÉHARBE, D. B. P. ; PEREIRA, D. ; SENA, D. ; VIDAL, J. M. B. . FERUS: um ambiente de desenvolvimento de especificações CASL. In: Simposio Brasileiro de Engenharia de Software (Sessao de Ferramentas), 2002, Gramado. Anais do 16o Simpósio Brasileiro de Engenharia de Software (SBES'2002), 2002. v. 1. p. 1-6.

Resumos publicados em anais de congressos
1.
DÉHARBE, D. B. P.. A prospective study on a formal compilation approach based on the B method. In: Franco-Brazilian Scientific Colloquium, 2008, Orsay, França. Franco-Brazilian Scientific Colloquium. Orsay, França: Université de Paris Sud, 2008. v. 1. p. 17-18.

2.
MARINHO, Eberton da Silva ; GUTEMBERG, Valério ; TAVARES, C. F. O. K. ; DÉHARBE, D. B. P. . Batcave - Um ambiente de Verificação Automática para o Método B. In: Brazilian Symposium on Formal Methods (SBMF2007), 2007, Ouro Preto. Brazilian Symposium on Formal Methods (SBMF2007). Ouro Preto: SBC/Universidade Federal de Ouro Preto, 2007. v. 1. p. 184-184.

3.
OLIVEIRA, D. C. B. ; DÉHARBE, D. B. P. ; FONTAINE, P. . haRVey: satisfaisabilité et théories. In: Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2007, Namur. AFADL 2007: Approches Formelles dans l'Assistance au Développement de Logiciels, 2007. v. 1. p. 287-288.

4.
VIDAL, J. M. B. ; DÉHARBE, D. B. P. ; BORRIONE, D. . Improving static ordering of BDDs for reachability analysis. In: ACM/IEEE 11th International Workshop on Logic & Synthesis (IWLS'02), 2002, New Orleans, LO, EstadosUnidos. Proceedings of the 11th IWLS, 2002. v. 1. p. 73-77.

5.
SOUZA, C. M. P. ; DÉHARBE, D. B. P. . Agendamento de captação, estocagem e distribuição de óleo. In: 1o Workshop dos Programa de Recursos Humanos da ANP-UFRN para o Setor de Petróleo e Gas, 2001, Natal, RN. 1o Workshop dos Programa de Recursos Humanos da ANP-UFRN para o Setor de Petróleo e Gas, 2001. v. 1. p. 27-28.

6.
COSTA, W. E. ; DÉHARBE, D. B. P. . Estudo sobre o problema SPT-Offline. In: 1o Workshop dos Programas de Recursos Humanos da ANP-UFRN para o Setor de Petróleo e Gás, 2001, Natal, RN. 1o Workshop dos Programas de Recursos Humanos da ANP-UFRN para o Setor de Petróleo e Gás - Resumos, 2001. v. 1. p. 113-114.

7.
COSTA, U. S. ; DÉHARBE, D. B. P. ; MOREIRA, A. M. . Variable Orderings of BDDs with Parallel Genetic Algorithms. In: PDPTA'2000, 2000, Las Vegas, Ne, Estados-Unidos. Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 2000. v. II. p. 1181-1186.

8.
DÉHARBE, D. B. P.; SANTIAGO, J. S. . An Automatic Design Flow from Models to FPGA. In: Concursos de Trabalhos de Iniciação Científica, 2000, Curitiba, PR. Concurso de Trabalhos de Iniciação Científica, 2000. p. 1-1.

9.
DÉHARBE, D. B. P.; DANTAS, B. P. ; PAULA, V. C. C. . Comparação entre descrições formais da arquitetura Enterprise Java Beans. In: Workshop Brasileiro de Métodos Formais, 2000, João Pessoa. Proceedings of 3rd Brazilian Workshop on Formal Methods: WMF'2000, 2000. p. 1-4.

10.
SANTIAGO, J. S. ; DÉHARBE, D. B. P. . Geração automática de FPGA usando SMV. In: Workshop Brasileiro de Métodos Formais, 2000, João Pessoa, PB. 3rd Brazilian Workhop on Formal Methods, 2000. p. 1-4.

11.
DÉHARBE, D. B. P.; MOREIRA, A. M. . Model Checking Invariants With Reduced Complexity. In: WORKSHOP ON LOGIC, PROOFS AND ALGORITHMS, 1998, CAMPINAS, SP, BRAZIL. LPA'98: SECOND WORKSHOP ON LOGIC, PROOFS AND ALGORITHMS, 1998. p. 9-10.

Apresentações de Trabalho
1.
BONICHON, R. ; Déharbe, David ; DOBAL, P. F. ; TAVARES, C. F. O. K. . SMTpp: preprocessors and analyzers for SMT-LIB. 2015. (Apresentação de Trabalho/Conferência ou palestra).

2.
DÉHARBE, D. B. P.. b2llvm: B developments onto the LLVM. 2014. (Apresentação de Trabalho/Conferência ou palestra).

3.
Déharbe, David; DOBAL, P. F. ; FONTAINE, P. . Le solveur SMT veriT. 2013. (Apresentação de Trabalho/Outra).

4.
ALMEIDA, V. A. ; DÉHARBE, D. B. P. . Integrating Rodin with SMT-Solvers. 2010. (Apresentação de Trabalho/Comunicação).

5.
BARBOSA, H. M. ; Russo Jr, A. ; DÉHARBE, D. B. P. . A Methodological WRSPM Approach to a B Formalization in an Industrial Setting. 2010. (Apresentação de Trabalho/Comunicação).

6.
DÉHARBE, D. B. P.. Model Checking (a tutorial). 1998. (Apresentação de Trabalho/Seminário).

Outras produções bibliográficas
1.
DÉHARBE, D. B. P.. Atelier B: Writing Mathematical Rules, 2009. (Tradução/Outra).

2.
DÉHARBE, D. B. P.; RANISE, S. . Bdd-driven first-order satisfiability procedures (extended version). Le Chesnay: Institut National de Recherche en Informatique et Automatique, 2002 (Relatorio de pesquisa).


Produção técnica
Programas de computador sem registro
1.
Bouton, T. ; OLIVEIRA, D. C. B. ; DÉHARBE, D. B. P. ; FONTAINE, P. . veriT: an open, trustable and efficient SMT-solver. 2009.

2.
DÉHARBE, D. B. P.; RANISE, S. . haRVey. 2003.

3.
DÉHARBE, D. B. P.. CV. 1997.


Demais tipos de produção técnica
1.
DÉHARBE, D. B. P.. Projeto rigoroso de componentes de software imperativo. 2014. (Curso de curta duração ministrado/Outra).

2.
DÉHARBE, D. B. P.; Russo Jr, A. . Desenvolvimento de software para sistemas críticos: estado da arte no Brasil. 2009. (Curso de curta duração ministrado/Extensão).

3.
DÉHARBE, D. B. P.. Programa PRIME. 2009. (Avaliador ad-hoc).

4.
DANTAS, B. P. ; DÉHARBE, D. B. P. ; GALVAO, S. S. L. ; MOREIRA, A. M. ; GUTEMBERG, Valério . Verified Compilation based on the B method: An initial appraisal (extended version).. 2008. (Relatório de pesquisa).

5.
MOREIRA, A. M. ; DÉHARBE, D. B. P. ; RIBEIRO, L. ; RODRIGUES, V. M. . Introdução a Métodos Formais: Especificação, Semântica e Verificação de Sistemas Concorrentes. 2000. (Curso de curta duração ministrado/Extensão).

6.
DÉHARBE, D. B. P.. Métodos Formais em Engenharia de Software e Verificação de Modelos. 2000. (Curso de curta duração ministrado/Outra).

Demais trabalhos
1.
DÉHARBE, D. B. P.. Model Checking. 2004 (Mini-curso) .

2.
DÉHARBE, D. B. P.. Interpretação abstrata. 2003 (Mini-curso) .



Bancas



Participação em bancas de trabalhos de conclusão
Mestrado
1.
Déharbe, David; OLIVEIRA, M. V. M.; BONICHON, R.; GOMES, B.E.G.. Participação em banca de Paulo Ewerton Gomes Fragoso. Contribuições para o Processo de Verificação de Satisfatibilidade Módulo Teoria em Event-B. 2015. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
MOREIRA, A. M.; Déharbe, David; GHEYI, R.. Participação em banca de João Batista de Souza Neto. Um estudo empírico sobre geração de testes com BETA: Avaliação e aperfeiçoamento. 2015. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

3.
MOREIRA, A. M.; Déharbe, David; GHEYI, R.. Participação em banca de Simone de Oliveira Santos. KitSmart: Uma biblioteca de componentes para o desenvolvimento rigoroso de aplicações Java Card com o método B. 2012. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

4.
OLIVEIRA, M. V. M.; ANDRADE, A. M. S.; DÉHARBE, D. B. P.. Participação em banca de Stephenson de Sousa Lima Galvão. Modelagem Formal do Sistema Operacional de Tempo Real FreeRTOS Utilizando o Método B. 2010. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

5.
DÉHARBE, D. B. P.; MOREIRA, A. M.; CAVALCANTI, A. L. C.. Participação em banca de Valério Gutemberg de Medeiros Júnior. Aplicação do Método B ao Projeto Formal de Software Embarcado. 2009. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

6.
DÉHARBE, D. B. P.; SILVA, Ivan Saraiva; KREUTZ, M. E.. Participação em banca de Bruno Cruz de Oliveira. Simulação de Reservatório em Ambiente MP-SoC. 2009. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

7.
SILVA, Ivan Saraiva; WANDERLEY NETTO, Eduardo Braulio; STRUM, Marius; DÉHARBE, D. B. P.. Participação em banca de Rodrigo Soares de Lima Sá Rego. Projeto e Implementação de uma Plataforma MP-SoC usando System C. 2006. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

8.
DÉHARBE, D. B. P.; SILVA, Ivan Saraiva; BARROS, Edna Natividade da Silva. Participação em banca de Sérgio Queiroz de Medeiros. Utilizando Programação Orientada a Aspectos no Projeto de Sistemas Hardware Desenvolvidos com SystemC. 2006. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

9.
MOREIRA, A. M.; DÉHARBE, D. B. P.; MUSICANTE, M. A.; IERUSALIMSCHY, R.. Participação em banca de Demóstenes Santos de Sena. AGraphs: Definição, Implementaçõ e Ferramentas. 2006. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

10.
SOUZA FILHO, G. L.; DÉHARBE, D. B. P.; PIMENTEL, M. G.. Participação em banca de Ítalo Herbert Santos e Gomes. TVOICE: Um Sistema de Manipulação de Linguagens para Auxiliar Portadores de Necessidades Especiais Atraves da Web. 2005. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

11.
SILVA, Ivan Saraiva; DÉHARBE, D. B. P.; WANDERLEY NETTO, Eduardo Braulio; BARROS, Marcelo Alves. Participação em banca de Leonardo Augusto Casillo. Projet e implementação de um processador com conjunto de instruções reconfiguravel em FPGA utilizando VHDL. 2005. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

12.
DÉHARBE, D. B. P.; SAMPAIO, A. C. A.; BORBA, P. H. M.. Participação em banca de Rohit Gehyi. Leis de Modelos e Projeto. 2004. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

13.
DÉHARBE, D. B. P.; SILVA, Ivan Saraiva; CARRO, L.. Participação em banca de José Iran Saraiva da Silva. Malha de interconexão para sistemas integrados em chip único. 2004. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

14.
MOTA, A. C.; DÉHARBE, D. B. P.; SAMPAIO, A. C. A.. Participação em banca de Walter Miranda Mesquita Neto. Uma estratégia para composição formal de frameworks. 2004. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

15.
CAMPOS, Sergio Vale Aguiar; DÉHARBE, D. B. P.; FERREIRA, R. A. C.. Participação em banca de Hugo Valentim barros. Um algoritmo distribuído para Verificação de Modelos com Fronteiras. 2004. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

16.
DÉHARBE, D. B. P.; SILVA, Ivan Saraiva; PERKUSICH, A.. Participação em banca de Antônio Augusto Oliveira Viana da Silva. Verificação formal de applets Java usando haRVey. 2004. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

17.
DÉHARBE, D. B. P.; BATISTA, Thais Vasconcelos; RODRIGUEZ, Noemi de La Rocque. Participação em banca de Fabricio de Alexandria Fernandes. Combinando Aspectos e Componentes: uma Abordagem Interpretada. 2004. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

18.
BORBA, P. H. M.; DÉHARBE, D. B. P.; SAMPAIO, A. C. A.. Participação em banca de Adalberto Cajueiro de Farias. Efficient and Mechanised Analysis of Infinite CSP-Z Specifications: strategy and tool support. 2003. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

19.
DÉHARBE, D. B. P.; MOREIRA, A. M.; REIS, A. I.. Participação em banca de Jorgiano Márcio Bruno Vidal. Ordenação inicial de BDDs para a verificação automática de sistemas de transição finita. 2002. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

20.
DÉHARBE, D. B. P.; GOUVEA, E. F.; GOLDBARG, M. C.. Participação em banca de Ana Carla Cabral Medeiros de Souza. Algoritmo transgenético para o problema do passeio de pistoneio. 2001. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

21.
DÉHARBE, D. B. P.; ALOISE, D. J.; FERNANDES, J. H. C.. Participação em banca de Carlos Avelino Barros. Uma aplicação de GRASP na otimização do emprego da unidade móvel de pistoneio. 2001. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

22.
DÉHARBE, D. B. P.; MOREIRA, A. M.; SAMPAIO, A. C. A.. Participação em banca de Bartira Paraguaçu Falcão Dantas. A linguagem de descrição de arquiteturas ZCLcsp. 2000. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

23.
DÉHARBE, D. B. P.; SILVA, Ivan Saraiva. Participação em banca de Nadja Rogéria Araújo Cândido. Concepção e implementação de uma malha de interconexão crossbar. 2000. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

24.
DÉHARBE, D. B. P.; GOUVEA, E. F.; GOLDBARG, M. C.. Participação em banca de Inalva Rangel de Morais Ferreira. Infecções virais na aceleração da solução do passeio do pistoneio. 2000. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

25.
CUNHA, P. R. F.; DÉHARBE, D. B. P.; SAMPAIO, A. C. A.. Participação em banca de Adnan Mahmoud Sherif. Especificação e verificação formal de sistemas de tempo-real. 2000. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

26.
DÉHARBE, D. B. P.. Participação em banca de Ana Karla Alves de Medeiros. Mecanismos de interação para um modelo de redes de Petri orientado a objetos. 2000. Dissertação (Mestrado em Informática [C.Grande]) - Universidade Federal da Paraíba.

27.
DÉHARBE, D. B. P.; MOREIRA, A. M.; MARTINS, S.. Participação em banca de Umberto Souza da Costa. Ordenação de variáveis de BDDs utilizando algoritmo genéticos paralelos. 2000. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

28.
DÉHARBE, D. B. P.; BEDREGAL, B. R. C.; ACIOLY, B. M.. Participação em banca de Aarão Lyra. Computabilidade no espaço dos intervalos reais: um modelo BSS intervalar. 1999. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

29.
VASCONCELOS, A. L.; DÉHARBE, D. B. P.; SAMPAIO, A. C. A.. Participação em banca de Leonardo Reis Lucena. Um ambiente unificador para as semânticas de Statecharts. 1999. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

Teses de doutorado
1.
DÉHARBE, D. B. P.; GHEYI, R.; MOREIRA, A. M.; OLIVEIRA, M. V. M.; SAMPAIO, A. C. A.. Participação em banca de Bruno Emerson Gurgel Gomes. Desenvolvimento Formal de Aplicações para Smart Cards. 2012. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
DÉHARBE, D. B. P.; FONTAINE, P.; MERZ, S.; GRIBOMONT, P.; MARCHE, C.; MONNIAUX, D.; SOUQUIERES, J.. Participação em banca de Diego Caminha Barbosa de Oliveira. Arithmétique et combinaison de procédures de décision. 2011. Tese (Doutorado em Doctorat en Informatique) - Laboratoire Lorrain de Recherche en Informatique et ses Applications.

3.
BORBA, P. H. M.; IYODA, J. M.; CORNELIO, M. L.; MELO, A. C. V.; DÉHARBE, D. B. P.. Participação em banca de Rodrigo Teixeira Ramos. Systematic Development of Trustworthy Component-based Systems. 2011. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

4.
CAMPOS, Sergio Vale Aguiar; DÉHARBE, D. B. P.; MOREIRA, A. M.; MOURA, A. V.; COELHO, C. J. N.; CHI, W. H.; VIEIRA, N. J.. Participação em banca de Umberto Souza da Costa. Um verificador de modelos explícito-simbólico. 2005. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Minas Gerais.

5.
DÉHARBE, D. B. P.. Participação em banca de Haroldo Gonçalves Benatti. Complexidade Descritiva de Problemas em Grafos. 2000. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

Qualificações de Doutorado
1.
MOREIRA, A. M.; Déharbe, David; Machado, P.; LEUSCHEL, M.. Participação em banca de Ernesto Cid Brasil de Matos. BETA: uma abordagem de testes baseada em B. 2015. Exame de qualificação (Doutorando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
Déharbe, David; MUSICANTE, M. A.; MOTA, A. C.; GOMES, B.E.G.. Participação em banca de Valério Gutemberg de Medeiros Júnior. Método B e a síntese verificada para código de montagem. 2015. Exame de qualificação (Doutorando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

3.
DÉHARBE, D. B. P.; MOREIRA, A. M.; SAMPAIO, A. C. A.. Participação em banca de Bruno Emerson Gurgel Gomes. Desenvolvimento Formal de Aplicaões para Smart Cards. 2010. Exame de qualificação (Doutorando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

4.
Machado, P.; MASSONI, T. L.; GHEYI, R.; DÉHARBE, D. B. P.. Participação em banca de Wilkerson de Lucena Andrade. Symbolic Testing of Real-Time Systems. 2009. Exame de qualificação (Doutorando em Ciência da Computação) - Universidade Federal de Campina Grande.

5.
BORBA, P. H. M.; DÉHARBE, D. B. P.. Participação em banca de Adalberto Cajueiro Farias. Abstraction of Data Dependent and Infinitely Communicationg CSPZ Processes. 2006. Exame de qualificação (Doutorando em Programa de Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.

6.
DÉHARBE, D. B. P.; COELHO, C. J. N.; MEDEIROS, S. Q.; CHI, W. H.. Participação em banca de Umberto Souza da Costa. Um verificador de modelos explícito-simbólico. 2003. Exame de qualificação (Doutorando em Pos-graduacao em Ciencia da Computacao) - Universidade Federal de Minas Gerais.

7.
DÉHARBE, D. B. P.. Participação em banca de Sandro Alex Damasceno Costa. Relações flexíveis de subtipo. 2003. Exame de qualificação (Doutorando em Programa de Pós-graduação em Engenharia Eletríca) - Universidade Federal de Campina Grande.

Qualificações de Mestrado
1.
DÉHARBE, D. B. P.; COSTA, U. S.; MEDEIROS, S. Q.; BONICHON, R.. Participação em banca de VÍtor Alcântara de Almeida. WPTrans: Um Assistente para Verificação de Programas em Frama-C. 2015. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
Déharbe, David; OLIVEIRA, M. V. M.; BONICHON, R.. Participação em banca de Paulo Ewerton Gomes Fragoso. Contribuições para o Processo de Verificação de Satisfatibilidade Módulo Teoria em Event-B. 2014. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

3.
MOREIRA, A. M.; Déharbe, David; MUSICANTE, M. A.. Participação em banca de João Batista de Souza Neto. Um estudo sobre geração de testes com BETA: Avaliação e aperfeiçoamento. 2014. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

Trabalhos de conclusão de curso de graduação
1.
DÉHARBE, D. B. P.; OLIVEIRA, M. V. M.; DANTAS, B. P.. Participação em banca de Haniel Moreira Barbosa.Desenvolvendo um Sistema Crítico através de Formalização de Requisitos Utilizando o Método B. 2010. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.

2.
OLIVEIRA, M. V. M.; DÉHARBE, D. B. P.; MAITELLI, A. L.. Participação em banca de Alessandro Cavalcante Gurgel.Suporte ao Cálculo de Refinamentos de Sistemas Concorrentes. 2009. Trabalho de Conclusão de Curso (Graduação em Engenharia de Computação) - Universidade Federal do Rio Grande do Norte.

3.
OLIVEIRA, M. V. M.; DÉHARBE, D. B. P.; MOREIRA, A. M.. Participação em banca de Luís Celso Dantas Silveira Cruz.Tradutor B-CSP. 2009. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.

4.
CAMPOS, A. M. C.; DÉHARBE, D. B. P.. Participação em banca de Kaio Alencar de Azevedo Dantas.Aplicativos Móveis em J2ME: Desenvolvimento de um Jogo para Celular. 2007. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

5.
DÉHARBE, D. B. P.; BEDREGAL, B. R. C.; MOTTA, B.. Participação em banca de Diego Caminha Barbosa de Oliveira.Procedimento de Decisão em Linha, Produtor de Prova, para Aritmética Linear Sobre Inteiros. 2006. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

6.
DÉHARBE, D. B. P.; BEDREGAL, B. R. C.; MOTTA, B.. Participação em banca de Alessandro Érik de Jesus.Procedimento de Decisão em Linha, Produtor de Prova, para Aritmética Linear sobre Números Racionais. 2006. Trabalho de Conclusão de Curso (Graduação em Bach. em Ciência da Computação e Eng. Computação) - Universidade Federal do Rio Grande do Norte.

7.
MOREIRA, A. M.; DÉHARBE, D. B. P.; VIDAL, J. M. B.. Participação em banca de Thiago Fernandes Silva Dutra.KitSmart: Um Kit de Tipos e Estruturas de Dados Projetados com o Método B para o Desenvolvimento Rigoroso em JavaCard. 2006. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

8.
DÉHARBE, D. B. P.. Participação em banca de Sérgio Queiroz de Medeiros.Especificação e verificação formal do modelo de comunicação do projeto automação de poços. 2004. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

9.
DÉHARBE, D. B. P.. Participação em banca de Demostenes Santos de Sena.Geração automatica de AGRAPHS. 2004. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

10.
DÉHARBE, D. B. P.; SILVA, Ivan Saraiva; SOUSA, Galileu Batista. Participação em banca de Rodrigo Soares de Lima Sa Rego.Implementação de uma Unidade Reconfiguravel de Granularidade Grossa usando SystemC. 2004. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

11.
DÉHARBE, D. B. P.. Participação em banca de Glaudson Marcel Nunes Maia.Generalização de componentes e softwares através de especificações algébricas para reutilização. 2000. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

12.
DÉHARBE, D. B. P.. Participação em banca de Georgen André Alves Freire.Uma estrutura de dados para FERUS: uma ferramenta para a criação de componentes reutilizáveis. 2000. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

13.
DÉHARBE, D. B. P.. Participação em banca de Dina Márcia de Vasconcelos Maranhão.Integração da linguagem de descrição de arquitetura de software ZCL com UML. 2000. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

14.
DÉHARBE, D. B. P.. Participação em banca de Jucimara Vanessa Balduíno.Ampliando CVA ? Uma ferramenta de análise VHDL. 1999. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.

15.
DÉHARBE, D. B. P.. Participação em banca de João Manuel Sousa Baptista Tavares.Comunicação entre agentes inteligentes. 1999. Trabalho de Conclusão de Curso (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte.



Participação em bancas de comissões julgadoras
Concurso público
1.
DÉHARBE, D. B. P.; SILVA, Ivan Saraiva; Wagner, F. R.. Concurso público de provas e títulos para o cargo de Professor 3º grau na classe Adjunto 1 na área de Concepção de Sistemas Integrados. 2008. Universidade Federal do Rio Grande do Norte.

2.
DÉHARBE, D. B. P.. Concurso Público de Provas e Títulos para Professor de Magistério Superior na classe de Adjunto, na área de Informática. 2005. Universidade Federal do Rio Grande do Norte.

3.
DÉHARBE, D. B. P.; SANTIAGO, R. H. N.; LIFSCHITZ, S.. Concurso Público de Provas e Títulos para Professor de Magistério Superior na classe de Adjunto, na área de Informática. 2004. Universidade Federal do Rio Grande do Norte.

Outras participações
1.
GOLDBARG, Elizabeth Ferreira Gouvêa; CAMPOS, A. M. C.; DÉHARBE, D. B. P.. Processo Seletivo Simplificado para Professores Substituto. 2005. Universidade Federal do Rio Grande do Norte.

2.
GOLDBARG, Elizabeth Ferreira Gouvêa; CAMPOS, A. M. C.; DÉHARBE, D. B. P.. Processo Seletivo Simplificado para Professor Substituto do Departamento de Informatica e Matematica Aplicada na area de Algoritmos e Estrutura de Dados. 2005. Universidade Federal do Rio Grande do Norte.

3.
DÉHARBE, D. B. P.; LOPES, A. B.; LEITE, J. C.. Processo Seletivo para Professor Substituto - Compiladores. 2004. Universidade Federal do Rio Grande do Norte.

4.
SOUSA, Galileu Batista; DÉHARBE, D. B. P.; SILVA, Ivan Saraiva. Processo Seletivo para Professor Substituto - Compiladores. 2004. Universidade Federal do Rio Grande do Norte.



Eventos



Organização de eventos, congressos, exposições e feiras
1.
DÉHARBE, D. B. P.. ICTAC - International Colloquium on Theoretical Aspects of Computing. 2010. (Outro).

2.
DÉHARBE, D. B. P.. XIII Brazilian Symposium on Formal Methods - SBMF. 2010. (Outro).

3.
DÉHARBE, D. B. P.; DANTAS, B. P. ; SOUZA NETO, P. A. ; SANTIAGO, J. S. . EPOCA 2008 - Escola Potiguar de Computação e suas Aplicações. 2008. (Outro).

4.
DÉHARBE, D. B. P.. Maratona de Programação da SBC - Sede local. 2006. (Outro).

5.
DÉHARBE, D. B. P.. 3rd IEEE International Conference on Software Engineering and Formal Methods. 2005. (Congresso).

6.
DÉHARBE, D. B. P.. Simpósio Brasileiro de Métodos Formais (SBMF2004). 2004. (Congresso).

7.
DÉHARBE, D. B. P.. XVIII Simpósio Brasileiro de Engenharia de Software (SBES'2004). 2004. (Congresso).

8.
DÉHARBE, D. B. P.. XVI Symposium on Integrated Circuits and System (SBCCI2004). 2004. (Congresso).

9.
DÉHARBE, D. B. P.. 2nd International Conference on Software Engineering and Formal Methods (SEFM'2004). 2004. (Congresso).

10.
DÉHARBE, D. B. P.. Concurso de Teses e Dissertações. 2004. (Congresso).

11.
DÉHARBE, D. B. P.. VI Brazilian Workshop on Formal Methods (WMF2003). 2003. (Congresso).

12.
DÉHARBE, D. B. P.. XVII Simpósio Brasileiro de Engenharia de Software (SBES'2003). 2003. (Congresso).

13.
DÉHARBE, D. B. P.. 15th Computer-Aided Verification conference (CAV'03). 2003. (Congresso).

14.
DÉHARBE, D. B. P.. 14th International Conference on Rewriting Techniques and Applications (RTA'03). 2003. (Congresso).

15.
DÉHARBE, D. B. P.. Eighteenth International Joint Conference on Artificial Intelligence (IJCAI'03). 2003. (Congresso).

16.
DÉHARBE, D. B. P.. V Workshop de Métodos Formais (WMF'2002). 2002. (Congresso).

17.
DÉHARBE, D. B. P.. XIV Symposium on Integrated Circuits and System (SBCCI2002). 2002. (Congresso).

18.
DÉHARBE, D. B. P.. XVI Simpósio Brasileiro de Engenharia de Software (SBES'2002). 2002. (Congresso).

19.
DÉHARBE, D. B. P.. 9th International Conference on Algebraic Methodology and Software Technology. 2002. (Congresso).

20.
DÉHARBE, D. B. P.. XV Simpósio Brasileiro de Engenharia de Software (SBES'2001). 2001. (Congresso).

21.
DÉHARBE, D. B. P.. XIII Symposium on Integrated Circuits and Systems Design (SBCCI2001). 2001. (Congresso).

22.
DÉHARBE, D. B. P.. IV Workshop Brasileiro de Métodos Formais (WMF'2001). 2001. (Congresso).

23.
DÉHARBE, D. B. P.; MOREIRA, A. M. . Workshop on Logic, Language, Information and Computation. 2000. (Congresso).

24.
DÉHARBE, D. B. P.. III Workshop Brasileiro de Métodos Formais (WMF'2000). 2000. (Congresso).

25.
DÉHARBE, D. B. P.. XIV Simpósio Brasileiro de Engenharia de Software (SBES'2000). 2000. (Congresso).

26.
DÉHARBE, D. B. P.. XII Symposium on Integrated Circuits and System Design. 2000. (Congresso).

27.
SILVA, Ivan Saraiva ; DÉHARBE, D. B. P. . XI Simpósio Brasileiro de Concepção de Circuitos Integrados. 1999. (Congresso).



Orientações



Orientações e supervisões em andamento
Tese de doutorado
1.
Valério Gutemberg de Medeiros Júnior. Formally verified compilation with the B method. Início: 2010. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte. (Orientador).

Supervisão de pós-doutorado
1.
Claudia Fernanda Oliveira Kiermes Tavares. Início: 2012. Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior.

Iniciação científica
1.
Vítor Alcântara de Almeida. Um plug-in de resolução SMT para a plataforma Rodin. Início: 2009. Iniciação científica (Graduando em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).


Orientações e supervisões concluídas
Dissertação de mestrado
1.
Haniel Moreira Barbosa. Formal Verification of PLC Programs using the B Method. 2012. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Agência Nacional do Petróleo. Orientador: David Boris Paul Déharbe.

2.
Valério Gutemberg de Medeiros Júnior. Extensão do método B ao projeto formal de sistemas embarcados micro-controlados.. 2008. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Agência Nacional do Petróleo. Orientador: David Boris Paul Déharbe.

3.
Stephenson de Sousa Lima Galvão. Construção de um sistema de arquivos verificado com o método B.. 2008. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Orientador: David Boris Paul Déharbe.

4.
Cláudia Fernando Oliveira Kiermes Tavares. Prova automática de Satisfatibilidade Módulo Teoria Aplicada ao Método B. 2007. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: David Boris Paul Déharbe.

5.
Diego Caminha Barbosa de Oliveira. Deciding Difference Logic in a Nelson-Oppen Combination Framework.. 2007. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Orientador: David Boris Paul Déharbe.

6.
Sérgio Queiroz de Medeiros. Aplicação de técnicas de engenharia de software para a linguagem SystemC. 2006. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

7.
Ítalo Herbert Santos Gomes. Mecanismo de acessibilidade da Web para deficientes visuais. 2005. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Coorientador: David Boris Paul Déharbe.

8.
Antônio Augusto Oliveira Viana da Silva. Contribuições para Verificação Automática de Applets JavaCard. 2004. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

9.
Jorgiano Márcio Bruno Vidal. Ordenação inicial de BDDs para a verificação automática de sistemas de transição finita. 2002. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Orientador: David Boris Paul Déharbe.

10.
Bartira Dantas Paraguaçu. A linguagem de descrição de arquitetura ZCLcsp. 2000. 0 f. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Orientador: David Boris Paul Déharbe.

Tese de doutorado
1.
Bruno Emerson Gurgel Gomes. Desenvolvimento Formal de Aplicações para Smart Card. 2012. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

2.
Umberto Souza Costa. Um verificador de modelos explícito-simbólico. 2005. Tese (Doutorado em Pos-graduacao em Ciencia da Computacao) - Universidade Federal de Minas Gerais, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Coorientador: David Boris Paul Déharbe.

Supervisão de pós-doutorado
1.
Anderson Santana de Oliveira. 2007. Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. David Boris Paul Déharbe.

Trabalho de conclusão de curso de graduação
1.
Haniel Moreira Barbosa. Desenvolvendo um sistema crítico através de formalização de requisitos utilizando o método B. 2010. Trabalho de Conclusão de Curso. (Graduação em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

2.
Valério Gutemberg de Medeiros Júnior. Aplicação do método B para a construção de programas de assemblagem. 2007. Trabalho de Conclusão de Curso. (Graduação em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

3.
Éberton da Silva Marinho. Geração de condições de verificação para o método B. 2007. Trabalho de Conclusão de Curso. (Graduação em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

4.
Diego Caminha Barbosa de Oliveira. Procedimento de Decisão em Linha, Produtor de Prova, para Aritmética Linear Sobre Inteiros. 2006. Trabalho de Conclusão de Curso. (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

5.
Alessandro Érik de Jesus. Procedimento de Decisão em Linha, Produtor de Prova, para Aritmética Linear Sobre Números Racionais. 2006. Trabalho de Conclusão de Curso. (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

6.
Cláudia Fernanda Oliveira Kiermes Tavares. Validação de provas equacionais com o assistente de prova Coq. 2005. Trabalho de Conclusão de Curso. (Graduação em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

7.
Jucimara Vanessa Balduíno. Ampliando CVA - uma ferramenta de análise para VHDL. 1998. 0 f. Trabalho de Conclusão de Curso. (Graduação em Engenharia de Computação) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

8.
Jorgiano Márcio Bruno Vidal. Um analisador léxico e sintático para a linguagem Verilog HDL. 1997. 0 f. Trabalho de Conclusão de Curso. (Graduação em Engenharia de Computação) - Universidade Federal do Rio Grande do Norte. Orientador: David Boris Paul Déharbe.

Iniciação científica
1.
Otto Luís Pontes Soares de Araújo. Uma abordagem formal para o projeto e implementação de componentes de software para sistemas embarcados. 2008. Iniciação Científica. (Graduando em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

2.
Thales Vieira Galdino. Prova automática de teoremas em lógica da primeira ordem e suas aplicações. 2008. Iniciação Científica. (Graduando em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Universidade Federal do Rio Grande do Norte - Pró-reitoria de Pesquisa. Orientador: David Boris Paul Déharbe.

3.
Edson Alyppyo Gomes Coutinho. BatCave - Geração de obrigações de prova no método B: integração no Eclipse. 2007. Iniciação Científica. (Graduando em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte, Universidade Federal do Rio Grande do Norte - Pró-reitoria de Pesquisa. Orientador: David Boris Paul Déharbe.

4.
Valério Gutemberg de Medeiros Júnior. Investigação da aplicação do Método B para a geração de programas em nível de assemblagem. 2007. Iniciação Científica. (Graduando em Bacharelado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Universidade Federal do Rio Grande do Norte - Pró-reitoria de Pesquisa. Orientador: David Boris Paul Déharbe.

5.
Paulo Moura Bittencourt. Geração de obrigações de prova na metodologia B. 2004. Iniciação Científica. (Graduando em Engenharia de Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

6.
Valmar da Silva Severiano. Instalação de melhores práticas de desenvolvimento de software no projeto haRVey. 2004. Iniciação Científica. (Graduando em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

7.
Valério Gutemberg Medeiros Júnior. BatCave - Geração de obrigações de prova no método B. 2004. Iniciação Científica. (Graduando em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

8.
Eberton da Silva Marinho. BatCave - Geração de obrigações de prova no método B. 2004. Iniciação Científica. (Graduando em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

9.
João Paulo Fernandes Farias. Aplicação de técnicas de verificação de modelos para o cálculo do pior tempo de execução. 2002. Iniciação Científica. (Graduando em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

10.
Sérgio Queiroz de Medeiros. BDDmeter: plug-in para o engenheiro de verificação. 2001. Iniciação Científica. (Graduando em Bacharelado em Ciencias da Computacao) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

11.
Judson Santos Santiago. Tradução automática de SMV para VHDL. 2000. 0 f. Iniciação Científica. (Graduando em Engenharia de Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.

12.
Manuel Ferreira Gomes Júnior. Inclusão de uma heurística de verificação de invariantes na ferramenta SMV.. 1998. 0 f. Iniciação Científica. (Graduando em Engenharia de Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: David Boris Paul Déharbe.



Educação e Popularização de C & T



Cursos de curta duração ministrados
1.
DÉHARBE, D. B. P.. Projeto rigoroso de componentes de software imperativo. 2014. (Curso de curta duração ministrado/Outra).



Outras informações relevantes


Para quem gosta de numerologia apenas;-)... Os resultados do processamento do nome de autor "deharbe", na area de Engenharia/Ciencia da Computacao/Matematica, pelo aplicativo "Harzing's Publish or Perish", no dia 25 de marco de 2009, foram:

"deharbe: eng", Papers:68,Citations:289,Years:18,Cites/year:16.06,Cites/paper:4.25/1.0/0,Cites/author:126.51,Papers/author:29.59,Authors/paper:2.75/3.0/2,h-index:10,g-index:14,hc-index:8,hI-index:3.45,hI-norm:6,AWCR:31.07,AW-index:5.57,AWCRpA:12.43

Em resumo sao os principais indices de producao (h-index, g-index, etc.) calculados a partir da base de dados no endereco scholar.google.com.



Página gerada pelo Sistema Currículo Lattes em 14/12/2018 às 23:04:38