Currículo do Sistema de Currículos Lattes (David Boris Paul Déharbe)

David Boris Paul Déharbe
Bolsista de Produtividade em Pesquisa do CNPq - Nível 2

Possui graduação em M.S.T. Expert en Systèmes Informatiques - Universite de Grenoble I (Scientifique Et Medicale - Joseph Fourier) (1990), mestrado em D.E.A. Informatique - Institut National Polytechnique de Grenoble (1991) e doutorado em Doctorat En Informatique - Universite de Grenoble I (Scientifique Et Medicale - Joseph Fourier) (1996). Atualmente é professor associado 1 da Universidade Federal do Rio Grande do Norte. Tem experiência na área de Ciência da Computação, com ênfase em Métodos formais, tendo como principais interesses o Método B, e a demonstração automática de teoremas
(Texto informado pelo autor)

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

Dados pessoais

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

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
59072-970 - Natal, RN - Brasil
Telefone: (81) 32153814 Ramal: 224 Fax: (81) 8432153814
URL da Homepage: http://www.dimap.ufrn.br/~david

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

2002 - 2003

Pós-Doutorado .
Laboratoire Lorrain de Recherche en Informatique et ses Applications.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior ,CAPES ,Brasil .
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.

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 .
Palavras-chave: VERIFICACAO FORMAL; CAD DE CIRCUITOS INTEGRADOS; VHDL.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação.
Setores de atividade: Informática; Industria Eletro-Eletrônica.

1990 - 1991

Mestrado em D.E.A. Informatique .
Institut National Polytechnique de Grenoble.
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 / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação.
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.

Atuação profissional

Fundação de Apoio a Pesquisa do Estado do Rio Grande do Norte.

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

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, Departamento de Informática e Matemática Aplicada.
	Atividade realizada Comitê de seleção de workshops do CBSOFT 2011.

2008 - Atual	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Sistemas computacionais confiáveis: desenvolvimento e verificação

2006 - Atual	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Desenvolvimento do Método B e Aplicação ao Projeto de Sistemas Embarcados Industriais

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

08/2004 - Atual	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Ergo: Ferramentas para o desenvolvimento rigoroso de sistemas computacionais seguros e confiáveis

6/2004 - Atual	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Um motor de dedução automatica incremental e produtor de prova

05/2003 - Atual	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Dedução automatica para analise formal de sistemas computacionais

03/1999 - Atual

Pesquisa e desenvolvimento , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

2010 - 2013	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa SMT-SAVeS: Verificação automática de software por resolução módulo teorias

2010 - 2012	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Confiabilidade e Segurança em Software Crítico Embarcado

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, Departamento de Informática e Matemática Aplicada.
	Atividade realizada SBMF 2010: Comitê de Programa.

03/2010 - 04/2010	Outras atividades técnico-científicas , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Atividade realizada Comitê de programa iFM 2010.

2007 - 2010	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Prova automática de teoremas para o desenvolvimento de sistemas computacionais confiáveis

2007 - 2009	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Combinando Técnicas de Métodos Formais e Teste na Construção de Sistemas Embarcados de Tempo Real

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

12/2005 - 11/2008	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa Da Capo: Dedução Automatica e Prova de Correção de Componentes de Software

06/2008 - 07/2008	Outras atividades técnico-científicas , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	Atividade realizada Membro do comitê de programa do SBMF2008.

04/2008 - 05/2008	Outras atividades técnico-científicas , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	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

01/2005 - 12/2006	Atividades de Participação em Projeto, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	Projetos de pesquisa SMART: Engineering of Smart Card Applications (CNPq/CT-Info/PDPG-TI)

03/2006 - 09/2006	Outras atividades técnico-científicas , Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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, Departamento de Informática e Matemática Aplicada.
	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çãoPreparaçã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.

Vínculo institucional

2009 - 2009

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

Carnegie Mellon University.

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 Concepcao de sistemas digitais Model checking

Linhas de Pesquisa

1.	Concepcao de sistemas digitais

2.	Model checking

Projetos de Pesquisa

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: Anamaria Martins Moreira - Integrante / Pascal Fontaine - Integrante / Diego Caminha Barbosa de Oliveira - Integrante / Marcel Vinícius de Medeiros Oliveira - Integrante / Stephan Merz - Integrante / David Boris Paul Déharbe - Coordenador.
Financiador(es): Institut National de Recherche en Informatique et en Automatique - Auxílio financeiro / Conselho Nacional de Desenvolvimento Científico e Tecnológico - 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.
Integrantes: Anamaria Martins Moreira - Integrante / Augusto Cezar Alves Sampaio - Integrante / Alexandre Cabral Mota - Integrante / Martín Alejandro Musicante - Integrante / Marcel Vinícius de Medeiros Oliveira - Integrante / Patrícia Duarte de Lima Machado - Integrante / Juliano Manabu Iyoda - Integrante / Flávia de Almeida Barros - Integrante / Franklin de Souza Ramalho - Integrante / Tiago Lima Massoni - Integrante / Rohit Gheyi - Integrante / Márcio L. Cornélio - Integrante / David Boris Paul Déharbe - Coordenador.
.

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. Integrantes: David Boris Paul Déharbe - Coordenador. Número de produções C, T & A: 3.

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 profissionalizante ( 0) / Doutorado ( 1) .
Integrantes: Anamaria Martins Moreira - Integrante / David Boris Paul Déharbe - Coordenador.
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: 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 / David Boris Paul Déharbe - Coordenador.
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 profissionalizante ( 0) / Doutorado ( 1) .
Integrantes: Anamaria Martins Moreira - Integrante / Christophe Ringeissen - Integrante / Silvio Ranise - Integrante / Pascal Fontaine - Integrante / David Boris Paul Déharbe - Coordenador.
Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Cooperação / Institut National de Recherche en Informatique et en Automatique - 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: Anamaria Martins Moreira - Integrante / David Boris Paul Déharbe - Coordenador. 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 profissionalizante ( 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 profissionalizante ( 0) / Doutorado ( 0) .
Integrantes: Jorgiano Márcio Bruno Vidal - Integrante / David Boris Paul Déharbe - Coordenador.
.

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): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa / Universidade Federal do Rio Grande do Norte - Bolsa.
Número de produções C, T & A: 8 / Número de orientações: 1.

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)

Á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

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ção em C,T & A

Produção bibliográfica

Citações

Web of Science

null

Outras
Total de trabalhos68	Total de citações289
deharbe Data: 25/03/2009

Artigos completos publicados em periódicos

1.	de 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.

2.	DÉ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.

3.	DANTAS, 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.

4.	DÉ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, v. 14, p. 71-86, 2008.

5.	DÉ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.

6.	GOMES, 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.

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

8.	CAMPOS, 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.

9.	MOREIRA, 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.

10.	COUCHOT, 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.

11.	RANISE, 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.

12.	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.

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

14.	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. Revista de Informática Teórica e Aplicada, v. 7, n. 1, p. 7-48, 2000.

15.	DÉ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. 397 p.

2.	DÉHARBE, D. B. P. (Org.) ; SOUZA NETO, P. A. (Org.) ; PARAGUAÇU, B. D. (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. 112 p.

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

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. 1 ed. : Kluwer Academic Publisher, 2003, v. 1, p. 135-158.

Trabalhos completos publicados em anais de congressos

1.	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.

2.	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.

3.	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.

4.	Bouton, T. ; OLIVEIRA, D. C. B. ; DÉHARBE, D. B. P. ; FONTAINE, P. . GridTPT: a distributed platform for Theorem Prover Testing. In: Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), 2010, Edinburgo. Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), 2010. p. 33-39.

5.	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.

6.	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.

7.	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.

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.

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.

10.

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.

11.

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.

12.

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.

13.

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.

14.

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.

15.	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.

16.

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.

17.	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.

18.	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.

19.	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.

20.	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.

21.	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.

22.	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.

23.

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.

24.

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.

25.	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.

26.

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.

27.

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.

28.

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.

29.	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.

30.	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.

31.

DÉHARBE, D. B. P. ; PARAGUAÇU, B. D. ; 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.

32.

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.

33.	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.

34.	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.

35.	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.

36.

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.

37.	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.

38.	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.

39.	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.

40.

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.

41.

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.

42.	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.	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.

2.	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.

3.	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.

4.	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.

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.

6.	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.

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.

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.

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.

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.

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.	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.

10.	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.

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.

Artigos aceitos para publicação

1.	Déharbe, David . Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming (Print), 2011.

2.	de Oliveira, Diego Caminha B. ; DÉHARBE, D. B. P. ; Fontaine, Pascal . Combining decision procedures by (model-)equality propagation?. Science of Computer Programming (Print), 2010.

Apresentações de Trabalho

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

2.	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).

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

Demais tipos de produção bibliográfica

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

Softwares sem registro de patente

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. ; Russo Jr, A. . Desenvolvimento de software para sistemas críticos: estado da arte no Brasil. 2009. (Curso de curta duração ministrado/Extensão).

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

3.	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).

4.	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).

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).

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 examinadoras

Dissertações

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.

2.	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.

3.	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.

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.

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.

6.	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.

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.

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.

9.	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.

10.	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.

11.	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.

12.	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.

13.	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.

14.

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.

15.	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.

16.	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.

17.	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.

18.	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.

19.	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.

20.	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.

21.	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.

22.	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.

23.	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.

24.	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.

25.	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.

26.	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

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.

2.	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.

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.

4.	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.	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.

2.	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.

3.	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.

4.	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.

5.	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.

Trabalhos de Conclusão de Curso de graduação

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.

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.

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.

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 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.

13.

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.

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.	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.

4.	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.

Eventos

Organização de eventos

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 em andamento

Dissertação de mestrado

1.	Haniel Moreira Barbosa. Uso do Método B no desenvolvimento de PLC. Início: 2010. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Agência Nacional do Petróleo. (Orientador).

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).

2.	Bartira Paraguaçu Falcão Dantas Rocha. Semántica formal do método B. Início: 2009. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte. (Orientador).

3.	Bruno Emerson Gurgel Gomes. Desenvolvimento Rigoroso de Aplicações de Smart Card. Início: 2008. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. (Orientador).

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).

Supervisões e orientações concluídas

Dissertação de mestrado

1.	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.

2.	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.

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.

4.	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.

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.

6.	Í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. Co-Orientador: David Boris Paul Déharbe.

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.

8.	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.

9.	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.	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. Co-Orientador: 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.

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.

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

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.

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.

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.

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.

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.

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.

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.

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.

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 12/02/2012 às 4:52:15