Semantics of a verification-oriented subset of VHDL. - David Déharbe; Dominique Borrione (CHARME, 1995)

HDL-Based Integration of Formal Methods and CAD Tools in the PREVAIL Environment. - Dominique Borrione; H. Bouamama; David Déharbe; C. Le Faou; Ayman M. Wahba (FMCAD, 1996)

Using induction and BDDs to model check invariants. - David Déharbe; Anamaria Martins Moreira (CHARME, 1997)

Model Checking VHDL with CV. - David Déharbe; Subash Shankar; Edmund M. Clarke (FMCAD, 1998)

Formal Verification of VHDL ¾ The Model Checker CV. - David Déharbe; Subash Shankar; Edmund M. Clarke (SBCCI, 1998)

Symbolic Model Checking with Fewer Fixpoint Computations. - David Déharbe; Anamaria Martins Moreira (World Congress on Formal Methods, 1999)

Variable Ordering of BDDs with Parallel Genetic Algorithms. - Umberto Souza da Costa; David Déharbe; Anamaria Martins Moreira (PDPTA, 2000)

Introdução a Métodos Formais: Especificação, Semântica e Verificação de Sistemas Concorrentes. - David Déharbe; Anamaria Martins Moreira; Leila Ribeiro 001; Vanderlei Moraes Rodrigues (RITA, 2000)

Optimizing BDD-Based Verification Analysing Variable Dependencies. - David Déharbe; Jorgiano Márcio Bruno Vidal (SBCCI, 2001)

BDDmeter - Uma Ferramenta para Visualização Dinâmica de BDDs. - Sérgio Queiroz de Medeiros; David Déharbe (SBES, 2001)

Improving Static Ordering of BDDs for Reachability Analysis. - Jorgiano Vidal; David Déharbe; Dominique Borrione (IWLS, 2002)

Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. - David Déharbe; Anamaria Martins Moreira; Christophe Ringeissen (RTA, 2002)

FERUS: Um Ambiente de Desenvolvimento de Especificações CASL. - Gleydson Lima; Anamaria Martins Moreira; David Déharbe; David Ricardo Do Vale Pereira; Demóstenes Sena; Jorgiano Vidal (SBES, 2002)

A Tutorial Introduction to Symbolic Model Checking. - David Déharbe (Logic for Concurrency and Synchronisation, 2003)

Light-Weight Theorem Proving for Debugging and Verifying Units of Code. - David Déharbe; Silvio Ranise (SEFM, 2003)

Proving and Debugging Set-Based Specifications. - Jean-François Couchot; Frédéric Dadeau; David Déharbe; Alain Giorgetti; Silvio Ranise (WMF, 2003)

Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. - Silvio Ranise; David Déharbe (FTP, 2003)

Abstraction-Driven Verification of Array Programs. - David Déharbe; Abdessamad Imine; Silvio Ranise (AISC, 2004)

Techniques for Temporal Logic Model Checking. - David Déharbe (PSSE, 2004)

Explicit-Symbolic Modelling for Formal Verification. - Umberto Souza da Costa; Sérgio Vale Aguiar Campos; Newton Vieira; David Déharbe (SBMF, 2004)

Scalable Automated Proving and Debugging of Set-Based Specifications. - Jean-François Couchot; David Déharbe; Alain Giorgetti; Silvio Ranise (J. Braz. Comput. Soc., 2004)

Manipulating algebraic specifications with term-based and graph-based representations. - Anamaria Martins Moreira; Christophe Ringeissen; David Déharbe; Gleydson Lima (J. Log. Algebraic Methods Program., 2004)

Distributing the Workload in a Lazy Theorem-Prover. - David Déharbe; Silvio Ranise; Jorgiano Vidal (SBMF, 2005)

Developing Java Card Applications with B. - Bruno Emerson Gurgel Gomes; Anamaria Martins Moreira; David Déharbe (SBMF, 2005)

Automation of Java Card component development using the B method. - David Déharbe; Bruno Emerson Gurgel Gomes; Anamaria Martins Moreira (ICECCS, 2006)

Decision Procedures for the Formal Analysis of Software. - David Déharbe; Pascal Fontaine; Silvio Ranise; Christophe Ringeissen (ICTAC, 2006)

Aspect-oriented design in systemC: implementation and applications. - David Déharbe; Sérgio Medeiros 001 (SBCCI, 2006)

AGraphs: Definition, implementation and tools. - David Déharbe; Anamaria Martins Moreira; Demóstenes Sena (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2006)

BSmart: A Tool for the Development of Java Card Applications with the B Method. - David Déharbe; Bruno Emerson Gurgel Gomes; Anamaria Martins Moreira (ABZ, 2008)

Verified Compilation and the B Method: A Proposal and a First Appraisal. - Bartira Dantas; David Déharbe; Stephenson Galvão; Anamaria Martins Moreira; Valério Medeiros Júnior (SBMF, 2008)

A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework. - David Déharbe; Silvio Ranise; Jorgiano Vidal (J. Braz. Comput. Soc., 2008)

veriT: An Open, Trustable and Efficient SMT-Solver. - Thomas Bouton; Diego Caminha Barbosa De Oliveira; David Déharbe; Pascal Fontaine (CADE, 2009)

Formalizing FreeRTOS: First Steps. - David Déharbe; Stephenson Galvão; Anamaria Martins Moreira (SBMF, 2009)

Formal Modelling of a Microcontroller Instruction Set in B. - Valério Medeiros Júnior; David Déharbe (SBMF, 2009)

Refining interfaces: the case of the B method - David Déharbe; Bruno Emerson Gurgel Gomes; Anamaria Martins Moreira (CoRR, 2009)

Satisfiability solving for software verification. - David Déharbe; Silvio Ranise (Int. J. Softw. Tools Technol. Transf., 2009)

Automatic Verification for a Class of Proof Obligations with SMT-Solvers. - David Déharbe (ASM, 2010)

Applying the B Method for the Rigorous Development of Smart Card Applications. - Bruno Emerson Gurgel Gomes; David Déharbe; Anamaria Martins Moreira; Katia Moraes (ASM, 2010)

Integrating SMT-Solvers in Z and B Tools. - Alessandro Cavalcante Gurgel; Valério Gutemberg de Medeiros; Marcel Vinícius Medeiros Oliveira; David Boris Paul Déharbe (ASM, 2010)

GridTPT: a distributed platform for Theorem Prover Testing. - Thomas Bouton; Diego Caminha; David Déharbe; Pascal Fontaine (PAAR@IJCAR, 2010)

Exploiting Symmetry in SMT Problems. - David Déharbe; Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo (CADE, 2011)

Quantifier Inference Rules for SMT proofs. - David Déharbe; Pascal Fontaine; Bruno Woltzenlogel Paleo (PxTP, 2011)

B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. - Marcel Vinícius Medeiros Oliveira; David Déharbe; Luís C. D. S. Cruz (SBMF, 2011)

Formal Verification of PLC Programs Using the B Method. - Haniel Barbosa; David Déharbe (ABZ, 2012)

SMT Solvers for Rodin. - David Déharbe; Pascal Fontaine; Yoann Guyot; Laurent Voisin (ABZ, 2012)

An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. - Haniel Barbosa; David Déharbe (SBMF, 2012)

Combining decision procedures by (model-)equality propagation. - Diego Caminha Barbosa De Oliveira; David Déharbe; Pascal Fontaine (Sci. Comput. Program., 2012)

Special issue: International Colloquium on Theoretical Aspects of Computing - ICTAC 2010. - Ana Cavalcanti 001; David Déharbe (Theor. Comput. Sci., 2012)

Computing prime implicants. - David Déharbe; Pascal Fontaine; Daniel Le Berre; Bertrand Mazure (FMCAD, 2013)

BEval: A Plug-in to Extend Atelier B with Current Verification Technologies. - Valério Medeiros Júnior; David Déharbe (LAFM, 2013)

Integration of SMT-solvers in B and Event-B development environments. - David Déharbe (Sci. Comput. Program., 2013)

LLVM-Based Code Generation for B. - Richard Bonichon; David Déharbe; Thierry Lecomte; Valério Medeiros Jr. (SBMF, 2014)

Extending SMT-LIB v2 with λ-Terms and Polymorphism. - Richard Bonichon; David Déharbe; Cláudia Tavares (SMT, 2014)

The 2014 SMT Competition. - David R. Cok; David Déharbe; Tjark Weber (J. Satisf. Boolean Model. Comput., 2014)

Integrating SMT solvers in Rodin. - David Déharbe; Pascal Fontaine; Yoann Guyot; Laurent Voisin (Sci. Comput. Program., 2014)

Software Component Design with the B Method - A Formalization in Isabelle/HOL. - David Déharbe; Stephan Merz (FACS, 2015)

Verifying Code Generation Tools for the B-Method Using Tests: A Case Study. - Anamaria Martins Moreira; Cleverton Hentz; David Déharbe; Ernesto Cid Brasil de Matos; João Batista de Souza Neto; Valério de Medeiros Jr. (TAP@STAF, 2015)

Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa". - Lilian Burdy; David Déharbe; Étienne Prun (F-IDE@FM, 2016)

Safety Analysis of a CBTC System: A Rigorous Approach with Event-B. - Mathieu Comptier; David Déharbe; Julien Molinero Perez; Louis Mussat; Pierre Thibaut; Denis Sabatier (RSSRail, 2017)

Applying a Formal Method in Industry: A 25-Year Trajectory. - Thierry Lecomte; David Déharbe; Étienne Prun; Erwan Mottin (SBMF, 2017)

Teaching an Old Dog New Tricks - The Drudges of the Interactive Prover in Atelier B. - Lilian Burdy; David Déharbe (ABZ, 2018)

Property-Driven Software Analysis - (Extended Abstract). - Mathieu Comptier; David Déharbe; Paulin Fournier; Julien Molinero Perez (FM, 2019)

B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution. - Dalay Israel de Almeida Pereira; David Déharbe; Matthieu Perin; Philippe Bon (RSSRail, 2019)

BTestBox: A Tool for Testing B Translators and Coverage of B Models. - Diego de Azevedo Oliveira; Valério Medeiros Jr.; David Déharbe; Martin A. Musicante (TAP@FM, 2019)

The SMT Competition 2015-2018. - Tjark Weber; Sylvain Conchon; David Déharbe; Matthias Heizmann; Aina Niemetz; Giles Reger (J. Satisf. Boolean Model. Comput., 2019)

Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B. - Héctor Ruíz Barradas; Lilian Burdy; David Déharbe (ABZ, 2020)

Low Cost High Integrity Platform. - Thierry Lecomte; David Déharbe; Denis Sabatier; Étienne Prun; Patrick Péronne; Emmanuel Chailloux; Steven Varoumas; Adilla Susungi; Sylvain Conchon (CoRR, 2020)

The CLEARSY safety platform: 5 years of research, development and deployment. - Thierry Lecomte; David Déharbe; Paulin Fournier; Marcel Oliveira (Sci. Comput. Program., 2020)

Assigning Safe Executed Systems to Meanings. - Lilian Burdy; David Déharbe; Denis Sabatier (RSSRail, 2022)