David Déharbe

Publication Activity (10 Years)

Years Active: 1995-2022
Publications (10 Years): 16

Top Topics

Extended Abstract

Propositional Logic

Safety Analysis

Code Generation

Top Venues

J. Satisf. Boolean Model. Comput.

Sci. Comput. Program.

Publications

Lilian Burdy, David Déharbe, Denis Sabatier
Assigning Safe Executed Systems to Meanings. RSSRail (2022)
Thierry Lecomte, David Déharbe, Paulin Fournier, Marcel Oliveira
The CLEARSY Safety Platform: 5 Years of Research, Development and Deployment. CoRR (2020)
Thierry Lecomte, David Déharbe, Denis Sabatier, Étienne Prun, Patrick Péronne, Emmanuel Chailloux, Steven Varoumas, Adilla Susungi, Sylvain Conchon
Low Cost High Integrity Platform. CoRR (2020)
Thierry Lecomte, David Déharbe, Paulin Fournier, Marcel Oliveira
The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199 (2020)
Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin
Applying a Formal Method in Industry: a 25-Year Trajectory. CoRR (2020)
Héctor Ruíz Barradas, Lilian Burdy, David Déharbe
Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B. ABZ (2020)
Diego de Azevedo Oliveira, Valério Medeiros Jr., David Déharbe, Martin A. Musicante
BTestBox: A Tool for Testing B Translators and Coverage of B Models. TAP@FM (2019)
Dalay Israel de Almeida Pereira, David Déharbe, Matthieu Perin, Philippe Bon
B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution. RSSRail (2019)
Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez
Property-Driven Software Analysis - (Extended Abstract). FM (2019)
Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Giles Reger
The SMT Competition 2015-2018. J. Satisf. Boolean Model. Comput. 11 (1) (2019)
Lilian Burdy, David Déharbe
Teaching an Old Dog New Tricks - The Drudges of the Interactive Prover in Atelier B. ABZ (2018)
Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin
Applying a Formal Method in Industry: A 25-Year Trajectory. SBMF (2017)
Mathieu Comptier, David Déharbe, Julien Molinero Perez, Louis Mussat, Pierre Thibaut, Denis Sabatier
Safety Analysis of a CBTC System: A Rigorous Approach with Event-B. RSSRail (2017)
Lilian Burdy, David Déharbe, Étienne Prun
Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa". F-IDE@FM (2016)
David Déharbe, Stephan Merz
Software Component Design with the B Method - A Formalization in Isabelle/HOL. FACS (2015)
Anamaria Martins Moreira, Cleverton Hentz, David Déharbe, Ernesto Cid Brasil de Matos, João Batista de Souza Neto, Valério de Medeiros Jr.
Verifying Code Generation Tools for the B-Method Using Tests: A Case Study. TAP@STAF (2015)
David R. Cok, David Déharbe, Tjark Weber
The 2014 SMT Competition. J. Satisf. Boolean Model. Comput. 9 (1) (2014)
Richard Bonichon, David Déharbe, Cláudia Tavares
Extending SMT-LIB v2 with λ-Terms and Polymorphism. SMT (2014)
David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
Integrating SMT solvers in Rodin. Sci. Comput. Program. 94 (2014)
Richard Bonichon, David Déharbe, Thierry Lecomte, Valério Medeiros Jr.
LLVM-Based Code Generation for B. SBMF (2014)
David Déharbe
Integration of SMT-solvers in B and Event-B development environments. Sci. Comput. Program. 78 (3) (2013)
David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
Computing prime implicants. FMCAD (2013)
Valério Medeiros Júnior, David Déharbe
BEval: A Plug-in to Extend Atelier B with Current Verification Technologies. LAFM (2013)
Haniel Barbosa, David Déharbe
An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. SBMF (2012)
Haniel Barbosa, David Déharbe
Formal Verification of PLC Programs Using the B Method. ABZ (2012)
Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
Combining decision procedures by (model-)equality propagation. Sci. Comput. Program. 77 (4) (2012)
Ana Cavalcanti, David Déharbe
Special issue: International Colloquium on Theoretical Aspects of Computing - ICTAC 2010. Theor. Comput. Sci. 455 (2012)
David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
SMT Solvers for Rodin. ABZ (2012)
David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
Exploiting Symmetry in SMT Problems. CADE (2011)
Marcel Vinícius Medeiros Oliveira, David Déharbe, Luís C. D. S. Cruz
B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. SBMF (2011)
David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo
Quantifier Inference Rules for SMT proofs. PxTP (2011)
Bruno Emerson Gurgel Gomes, David Déharbe, Anamaria Martins Moreira, Katia Moraes
Applying the B Method for the Rigorous Development of Smart Card Applications. ASM (2010)
David Déharbe
Automatic Verification for a Class of Proof Obligations with SMT-Solvers. ASM (2010)
Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine
GridTPT: a distributed platform for Theorem Prover Testing. PAAR@IJCAR (2010)
David Déharbe, Stephenson Galvão, Anamaria Martins Moreira
Formalizing FreeRTOS: First Steps. SBMF (2009)
Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
veriT: An Open, Trustable and Efficient SMT-Solver. CADE (2009)
David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira
Refining interfaces: the case of the B method CoRR (2009)
Valério Medeiros Júnior, David Déharbe
Formal Modelling of a Microcontroller Instruction Set in B. SBMF (2009)
David Déharbe, Silvio Ranise
Satisfiability solving for software verification. Int. J. Softw. Tools Technol. Transf. 11 (3) (2009)
Bartira Dantas, David Déharbe, Stephenson Galvão, Anamaria Martins Moreira, Valério Medeiros Júnior
Verified Compilation and the B Method: A Proposal and a First Appraisal. Electron. Notes Theor. Comput. Sci. 240 (2009)
Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
Combining Decision Procedures by (Model-)Equality Propagation. Electron. Notes Theor. Comput. Sci. 240 (2009)
David Déharbe, Silvio Ranise, Jorgiano Vidal
A Prototype Implementation of a Distributed Satisfiability Modulo Theories Solver in the ToolBus Framework. J. Braz. Comput. Soc. 14 (1) (2008)
David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira
BSmart: A Tool for the Development of Java Card Applications with the B Method. ABZ (2008)
David Déharbe, Silvio Ranise, Jorgiano Vidal
Distributing the Workload in a Lazy Theorem-Prover. Electron. Notes Theor. Comput. Sci. 184 (2007)
Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira, David Déharbe
Developing Java Card Applications with B. Electron. Notes Theor. Comput. Sci. 184 (2007)
David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen
Decision Procedures for the Formal Analysis of Software. ICTAC (2006)
David Déharbe, Anamaria Martins Moreira, Demóstenes Sena
AGraphs: Definition, implementation and tools. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 1 (2006)
David Déharbe, Sergio Medeiros
Aspect-oriented design in systemC: implementation and applications. SBCCI (2006)
David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira
Automation of Java Card component development using the B method. ICECCS (2006)
Umberto Souza da Costa, Sérgio Vale Aguiar Campos, Newton Vieira, David Déharbe
Explicit-Symbolic Modelling for Formal Verification. Electron. Notes Theor. Comput. Sci. 130 (2005)
Jean-François Couchot, David Déharbe, Alain Giorgetti, Silvio Ranise
Scalable Automated Proving and Debugging of Set-Based Specifications. J. Braz. Comput. Soc. 9 (2) (2004)
David Déharbe
Techniques for Temporal Logic Model Checking. PSSE (2004)
David Déharbe, Abdessamad Imine, Silvio Ranise
Abstraction-Driven Verification of Array Programs. AISC (2004)
Jean-François Couchot, Frédéric Dadeau, David Déharbe, Alain Giorgetti, Silvio Ranise
Proving and Debugging Set-Based Specifications. Electron. Notes Theor. Comput. Sci. 95 (2004)
Anamaria Martins Moreira, Christophe Ringeissen, David Déharbe, Gleydson Lima
Manipulating algebraic specifications with term-based and graph-based representations. J. Log. Algebraic Methods Program. 59 (1-2) (2004)
Silvio Ranise, David Déharbe
Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. Electron. Notes Theor. Comput. Sci. 86 (1) (2003)
David Déharbe, Silvio Ranise
Light-Weight Theorem Proving for Debugging and Verifying Units of Code. SEFM (2003)
Gleydson Lima, Anamaria Martins Moreira, David Déharbe, David Ricardo Do Vale Pereira, Demóstenes Sena, Jorgiano Vidal
FERUS: Um Ambiente de Desenvolvimento de Especificações CASL. SBES (2002)
David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen
Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. RTA (2002)
Jorgiano Vidal, David Déharbe, Dominique Borrione
Improving Static Ordering of BDDs for Reachability Analysis. IWLS (2002)
David Déharbe, Jorgiano Márcio Bruno Vidal
Optimizing BDD-Based Verification Analysing Variable Dependencies. SBCCI (2001)
Sérgio Queiroz de Medeiros, David Déharbe
BDDmeter - Uma Ferramenta para Visualização Dinâmica de BDDs. SBES (2001)
David Déharbe, Anamaria Martins Moreira, Leila Ribeiro, Vanderlei Moraes Rodrigues
Introdução a Métodos Formais: Especificação, Semântica e Verificação de Sistemas Concorrentes. RITA 7 (1) (2000)
Umberto Souza da Costa, David Déharbe, Anamaria Martins Moreira
Variable Ordering of BDDs with Parallel Genetic Algorithms. PDPTA (2000)
David Déharbe, Anamaria Martins Moreira
Symbolic Model Checking with Fewer Fixpoint Computations. World Congress on Formal Methods (1999)
David Déharbe, Subash Shankar, Edmund M. Clarke
Formal Verification of VHDL ¾ The Model Checker CV. SBCCI (1998)
David Déharbe, Subash Shankar, Edmund M. Clarke
Model Checking VHDL with CV. FMCAD (1998)
David Déharbe, Anamaria Martins Moreira
Using induction and BDDs to model check invariants. CHARME (1997)
Dominique Borrione, H. Bouamama, David Déharbe, C. Le Faou, Ayman M. Wahba
HDL-Based Integration of Formal Methods and CAD Tools in the PREVAIL Environment. FMCAD (1996)
David Déharbe, Dominique Borrione
Semantics of a verification-oriented subset of VHDL. CHARME (1995)