Personal information

Activities

Employment (3)

CLEARSY Systems Engineering: Aix-en-Provence, FR

2016-01-11 to present
Employment
Source: Self-asserted source
David Deharbe

Universidade Federal do Rio Grande do Norte: Natal, RN, BR

1997-03-01 to present
Employment
Source: Self-asserted source
David Deharbe

Carnegie Mellon University: Pittsburgh, PA, US

1995-02-01 to 1997-01-31 | Visiting Researcher (School of Computer Science)
Employment
Source: Self-asserted source
David Deharbe

Education and qualifications (4)

Université de Grenoble Alpes: Grenoble, Rhône-Alpes, FR

1993-10-01 to 1996-11-10 | Docteur en Informatique
Education
Source: Self-asserted source
David Deharbe

Institut Polytechnique de Grenoble: Grenoble, Rhône-Alpes, FR

1990-10-01 to 1991-08-31 | DEA Informatics
Education
Source: Self-asserted source
David Deharbe

Université Grenoble Alpes Grenoble IAE: Saint-Martin-d'Heres, Auvergne-Rhône-Alpes, FR

1988-10-01 to 1990-08-31 | Master of Sciences and Techniques - Expert in Informatics Systems (MST ESI)
Education
Source: Self-asserted source
David Deharbe

Université de Lorraine: Épinal, FR

1986-10-01 to 1988-06-30 | DEUG A SSM - Mathematics and Physics.
Education
Source: Self-asserted source
David Deharbe

Professional activities (1)

Agence Nationale de la Recherche: Paris, FR

2020-01-01 to 2020-06-30 | Member of expert committee 25 for call AAPG-2020.
Service
Source: Self-asserted source
David Deharbe

Funding (2)

DISCONT

2017-09 to 2022-08 | Grant
Agence Nationale de la Recherche (Paris, FR)
GRANT_NUMBER: ANR-17-CE25-0005
Source: Self-asserted source
David Deharbe

AMASS

2016-04 to 2019-03 | Grant
European Commission (Brussels, FR)
GRANT_NUMBER: 692474
Source: Self-asserted source
David Deharbe

Works (50 of 55)

Items per page:
Page 1 of 2

The CLEARSY safety platform: 5 years of research, development and deployment

Science of Computer Programming
2020-11 | Journal article
Contributors: Thierry Lecomte; David Deharbe; Paulin Fournier; Marcel Oliveira
Source: check_circle
Crossref

B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution

2019 | Book chapter
Contributors: Dalay Israel de Almeida Pereira; David Deharbe; Matthieu Perin; Philippe Bon
Source: check_circle
Crossref

Integrating SMT solvers in Rodin

Science of Computer Programming
2014-11 | Journal article
Contributors: David Déharbe; Pascal Fontaine; Yoann Guyot; Laurent Voisin
Source: check_circle
Crossref

Combining Decision Procedures by (Model-)Equality Propagation

Electronic Notes in Theoretical Computer Science
2009 | Journal article
Part of ISSN: 1571-0661
Contributors: D�harbe, David; Fontaine, Pascal; de Oliveira, Diego Caminha B.
Source: Self-asserted source
David Deharbe via ResearcherID

Escola Potiguar de Computação e suas Aplicações. EPOCA 2008 - Mini-cursos selecionados

2009 | Book
Source: Self-asserted source
David Deharbe via ResearcherID

Satisfiability solving for software verification

International Journal on Software Tools for Technology Transfer (STTT)
2009 | Journal article
Contributors: Déharbe, David; Ranise, Silvio
Source: Self-asserted source
David Deharbe via ResearcherID

Verified Compilation and the B Method: A Proposal and a First Appraisal

Electronic Notes in Theoretical Computer Science
2009 | Journal article
Part of ISSN: 1571-0661
Contributors: Dantas, Bartira; D�harbe, David; Galv�o, Stephenson; Medeiros J�nior, Val�rio; Moreira, Anamaria Martins
Source: Self-asserted source
David Deharbe via ResearcherID

A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework

Journal of the Brazilian Computer Society
2008 | Journal article
Contributors: Déharbe, David; Ranise, Silvio; Vidal, Jorgiano
Source: Self-asserted source
David Deharbe via ResearcherID

BSmart: A Tool for the Development of Java Card Applications with the B Method

2008 | Book chapter
Contributors: Déharbe, David; Gomes, Bruno; Moreira, Anamaria
Source: Self-asserted source
David Deharbe via ResearcherID

Verified Compilation based on the B method: An initial appraisal (extended version)

2008 | Report
Contributors: Dantas, Bartira; Déharbe, David; Galvão, Stephenson; Jr, Valerio Medeiros; Moreira, Anamaria
Source: Self-asserted source
David Deharbe via ResearcherID

Developing Java Card Applications with B

Electronic Notes in Theoretical Computer Science
2007 | Journal article
Part of ISSN: 1571-0661
Contributors: D�harbe, David; Gomes, Bruno Emerson Gurgel; Moreira, Anamaria Martins
Source: Self-asserted source
David Deharbe via ResearcherID

Distributing the Workload in a Lazy Theorem-Prover

Electronic Notes in Theoretical Computer Science
2007 | Journal article
Part of ISSN: 1571-0661
Contributors: Deharbe, David; Ranise, Silvio; Vidal, Jorgiano
Source: Self-asserted source
David Deharbe via ResearcherID

Agraphs: Definition, implementation and tools

Electronic communications of the EASST
2006 | Journal article
Contributors: Déharbe, David; Moreira, Anamaria; Sena, Demostenes
Source: Self-asserted source
David Deharbe via ResearcherID

Decision procedures for the formal analysis of software

3rd International Colloquium on Theoretical Aspects of Computing
2006 | Conference paper
Part of ISBN:

0302-9743

Contributors: DEHARBE, D; FONTAINE, P; RANISE, S; RINGEISSEN, C
Source: Self-asserted source
David Deharbe via ResearcherID

Techniques for temporal logic model checking

1st Pernambuco Summer School on Software Engineering
2006 | Conference paper
Part of ISBN:

0302-9743

Contributors: DEHARBE, D
Source: Self-asserted source
David Deharbe via ResearcherID

Explicit-Symbolic Modelling for Formal Verification

Electronic Notes in Theoretical Computer Science
2005 | Journal article
Part of ISSN: 1571-0661
Contributors: Campos, S�rgio; Costa, Umberto; D�harbe, David; Vieira, Newton
Source: Self-asserted source
David Deharbe via ResearcherID

Abstraction-driven verification of array programs

7th International Conference on Artificial Intelligence and Symbolic Computation
2004 | Conference paper
Part of ISBN:

0302-9743

Contributors: DEHARBE, D; IMINE, A; RANISE, S
Source: Self-asserted source
David Deharbe via ResearcherID

Evolving Algebraic Specifications with Term-based and Graph-based Representations

Journal of Logic and Algebraic Programming
2004 | Journal article
Contributors: Déharbe, David; Lima, Gleydson; Moreira, Anamaria Martins; Ringeissen, Christophe
Source: Self-asserted source
David Deharbe via ResearcherID

Manipulating algebraic specifications with term-based and graph-based representations

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING
2004 | Journal article
Part of ISSN: 1567-8326
Contributors: DEHARBE, D; LIMA, G; MOREIRA, AM; RINGEISSEN, C
Source: Self-asserted source
David Deharbe via ResearcherID

Proving and Debugging Set-Based Specifications

Electronic Notes in Theoretical Computer Science
2004 | Journal article
Part of ISSN: 1571-0661
Contributors: Couchot, J. F.; Dadeau, F.; D�harbe, D.; Giorgetti, A.; Ranise, S.
Source: Self-asserted source
David Deharbe via ResearcherID

Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs

Electronic Notes in Theoretical Computer Science
2003 | Journal article
Part of ISSN: 1571-0661
Contributors: D�harbe, David; Ranise, Silvio
Source: Self-asserted source
David Deharbe via ResearcherID

Logic for Concurrency and Synchronisation

2003 | Other
Contributors: Déharbe, David
Source: Self-asserted source
David Deharbe via ResearcherID

Scalable Automated Proving and Debugging of Set-Based Specifications

Journal of the Brazilian Computer Society
2003 | Journal article
Contributors: Couchot, Jean-François; Déharbe, David; Giorgetti, Alain; Ranise, Silvio
Source: Self-asserted source
David Deharbe via ResearcherID

BDD-driven first-order satisfiability procedures (extended version)

2002 | Report
Contributors: Déharbe, David; Ranise, Silvio
Source: Self-asserted source
David Deharbe via ResearcherID

Improving symbolic model checking by rewriting temporal logic formulae

13th International Conference on Rewriting Techniques and Applications
2002 | Conference paper
Part of ISBN:

0302-9743

Contributors: DEHARBE, D; MOREIRA, AM; RINGEISSEN, C
Source: Self-asserted source
David Deharbe via ResearcherID

Proceedings of the 5th Workshop on Formal Methods

2002 | Book
Source: Self-asserted source
David Deharbe via ResearcherID

Symbolic model checking with fewer fixpoint computations

1st World Congress on Formal Methods in the Development of Computing Systems (FM 99)
1999 | Conference paper
Part of ISBN:

0302-9743

Contributors: DEHARBE, D; MOREIRA, AM
Source: Self-asserted source
David Deharbe via ResearcherID

HDL-based integration of formal methods and CAD tools in the PREVAIL environment

1st International Conference on Formal Methods in Computer-Aided Design (FMCAD 96)
1996 | Conference paper
Part of ISBN:

0302-9743

Contributors: BORRIONE, D; BOUAMAMA, H; DEHARBE, D; LE FAOU, C; WAHBA, A
Source: Self-asserted source
David Deharbe via ResearcherID

Semantics of a verification-oriented subset of VHDL

IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 95)
1995 | Conference paper
Part of ISBN:

0302-9743

Contributors: BORRIONE, D; DEHARBE, D
Source: Self-asserted source
David Deharbe via ResearcherID

A cache-based parallel genetic algorithm for the BDD variable ordering problem

12th Symposium on Computer Architecture and High Performance Computing (SPAC-PAD'2000)
Conference paper
Contributors: Déharbe, David; Moreira, Anamaria Martins; da Costa, Umberto Souza
Source: Self-asserted source
David Deharbe via ResearcherID

A Ferramenta Batcave para a Verificação de Especificações Formais na Notaçao B

XV Sessão de Ferramentas do Simpósio Brasileiro de Engenharia de Software
Conference paper
Contributors: Déharbe, David; Gomes, Bruno; Jr, Valério Medeiros; Marinho, Eberton; Tavares, Cláudia
Source: Self-asserted source
David Deharbe via ResearcherID

A Ferramenta BSmart para o Desenvolvimento Rigoroso de Aplicações Java Card com o Método Formal B

XIV Sessão de Ferramentas do XXI Simpósio Brasileiro de Engenharia de Software
Conference paper
Contributors: Déharbe, David; Gomes, Bruno; Moraes, Kátia; Moreira, Anamaria
Source: Self-asserted source
David Deharbe via ResearcherID

Advances in BDD reduction using Parallel Genetic Algorithms

IEEE 10th International Workshop on Logic & Synthesis (IWLS'2001)
Conference paper
Contributors: Costa, Umberto Souza; Déharbe, David; Moreira, Anamaria Martins
Source: Self-asserted source
David Deharbe via ResearcherID

Applying the B method to take on the grand challenge of verified compilation

Brazilian Symposium on Formal Methods (SBMF2008)
Conference paper
Contributors: Déharbe, David
Source: Self-asserted source
David Deharbe via ResearcherID

Aspect-Oriented Design in SystemC: Implementation and Applications

Proceedings of the Nineteenth Brazilian Symposium on Integrated Circuits and System Design (SBCCI2006)
Conference paper
Contributors: Déharbe, David; Medeiros, Sergio
Source: Self-asserted source
David Deharbe via ResearcherID

Automation of Java Card component development using the B method

11th IEEE International Conference on Engineering of Complex Computer Systems, 2006. ICECCS 2006
Conference paper
Contributors: Deharbe, David; Gomes, Bruno Emerson Gurgel; Moreira, Anamaria Martins
Source: Self-asserted source
David Deharbe via ResearcherID

BDDmeter - Uma ferramenta para visualização din�mica de BDDs

Anais do XVI Simpósio Brasileiro de Engenharia de Software (SBES'2001) -- Sessão de Ferramentas
Conference paper
Contributors: Déharbe, David; de Medeiros, Sérgio Queiroz
Source: Self-asserted source
David Deharbe via ResearcherID

Combining decision procedures by (model-)equality propagation

Brazilian Symposium on Formal Methods (SBMF2008)
Conference paper
Contributors: Déharbe, David; Fontaine, Pascal; Oliveira, Diego B. C.
Source: Self-asserted source
David Deharbe via ResearcherID

Consideracoes sobre Especificacao e Verificacao Formal de Sistemas Embarcados utilizando JML

Proceedings X Workshop IBERCHIP
Conference paper
Contributors: Carro, Luigi; Deharbe, David; Silva, Ivan Saraiva; da Silva, Antonio Augusto Vieira Viana
Source: Self-asserted source
David Deharbe via ResearcherID

FERUS: um ambiente de desenvolvimento de especificações CASL

Proceedings of SBES'2002 16o Simpósio Brasileiro de Engenharia de Software): Sessão de ferramentas
Conference paper
Contributors: Déharbe, David; Lima, Gleydson; Moreira, Anamaria Martins; Pereira, David; Sena, Demostenes; Vidal, Jorgiano
Source: Self-asserted source
David Deharbe via ResearcherID

Flexibilidade e Transversalidade no Projeto Pedagógico para o Curso de Ci�ncia da Computação na UFRN

X Workshop de Educacao em Informatica (WEI'2002)
Conference paper
Contributors: Cerqueira, Nilda Teixeira; Déharbe, David; Gouv�ia, Elizabeth Ferreira; Leite, Jair Cavalcanti; Lopes, Adilson Barbosa
Source: Self-asserted source
David Deharbe via ResearcherID

Formal Modelling of a Microcontroller Instruction Set in B

Formal Methods: Foundations and Applications, 12th Brazilian<p> Symposium on Formal Methods, SBMF 2009, Gramado, Brazil,<p> August 19-21, 2009, Revised Selected Papers
Conference paper
Contributors: Déharbe, David; Jr, Valério Medeiros
Source: Self-asserted source
David Deharbe via ResearcherID

Formalizing FreeRTOS: First Steps

Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009, Revised Selected Papers
Conference paper
Contributors: Déharbe, David; Galvão, Stephenson; Moreira, Anamaria Martins
Source: Self-asserted source
David Deharbe via ResearcherID

Improving static ordering of BDDs for reachability analysis

IEEE/ACM 11th International Workshop on Logic & Synthesis
Conference paper
Contributors: Borrione, Dominique; Déharbe, David; Vidal, Jorgiano
Source: Self-asserted source
David Deharbe via ResearcherID

Improving symbolic model checking by rewriting temporal formulae

RTA'02 -- Conference on Rewriting Techniques and Applications
Conference paper
Contributors: Déharbe, David; Moreira, Anamaria Martins; Ringeissen, Christophe
Source: Self-asserted source
David Deharbe via ResearcherID

Light-weight theorem proving for debugging and verifying pointer manipulating programs

4th International Workshop on First-Order Theorem Proving (FTP'2003)
Conference paper
Contributors: Déharbe, David; Ranise, Silvio
Source: Self-asserted source
David Deharbe via ResearcherID

Light-Weight Theorem Proving for Debugging and Verifying Units of Code

1st IEEE International Conference on Software Engineering and Formal Methods (SEFM03)
Conference paper
Contributors: Déharbe, David; Ranise, Silvio
Source: Self-asserted source
David Deharbe via ResearcherID

Model checking VHDL with CV

Formal Methods in Circuit Automation Design (FMCAD'98)
Conference paper
Contributors: Déharbe, David; Jr, Edmund M. Clarke; Shankar, Subash
Source: Self-asserted source
David Deharbe via ResearcherID

Modelling Control Systems in B: an Industrial Case Study

Brazilian Symposium on Formal Methods (SBMF2007)
Conference paper
Contributors: Déharbe, David; Jr, Aryldo Russo; Moreira, Anamaria; Silva, Paulo Muniz
Source: Self-asserted source
David Deharbe via ResearcherID

Optimizing BDD-based verification analysing variable dependencies

XIV Symposium on Integrated Circuits and System Design (SBCCI'01)
Conference paper
Contributors: Déharbe, David; Vidal, Jorgiano Márcio Bruno
Source: Self-asserted source
David Deharbe via ResearcherID
Items per page:
Page 1 of 2

Peer review (1 review for 1 publication/grant)

Review activity for Formal aspects of computing. (1)