David Déharbe

According to our database, David Déharbe authored at least 69 papers between 1995 and 2022.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2022

Assigning Safe Executed Systems to Meanings.

Lilian Burdy, David Déharbe, Denis Sabatier

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2022

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

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

Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B.

Héctor Ruíz Barradas, Lilian Burdy, David Déharbe

Proceedings of the Rigorous State-Based Methods - 7th International Conference, 2020

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

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

Proceedings of the Tests and Proofs - 13th International Conference, 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

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2019

Property-Driven Software Analysis - (Extended Abstract).

Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018

Teaching an Old Dog New Tricks - The Drudges of the Interactive Prover in Atelier B.

Lilian Burdy, David Déharbe

Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2018

2017

Applying a Formal Method in Industry: A 25-Year Trajectory.

Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin

Proceedings of the Formal Methods: Foundations and Applications - 20th Brazilian Symposium, 2017

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

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2017

2016

Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa".

Lilian Burdy, David Déharbe, Étienne Prun

Proceedings of the Third Workshop on Formal Integrated Development Environment, 2016

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.

Proceedings of the Tests and Proofs - 9th International Conference, 2015

Software Component Design with the B Method - A Formalization in Isabelle/HOL.

David Déharbe, Stephan Merz

Proceedings of the Formal Aspects of Component Software - 12th International Conference, 2015

2014

Integrating SMT solvers in Rodin.

David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin

Sci. Comput. Program., 2014

The 2014 SMT Competition.

David R. Cok, David Déharbe, Tjark Weber

J. Satisf. Boolean Model. Comput., 2014

Extending SMT-LIB v2 with λ-Terms and Polymorphism.

Richard Bonichon, David Déharbe, Cláudia Tavares

Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, 2014

LLVM-Based Code Generation for B.

Richard Bonichon, David Déharbe, Thierry Lecomte, Valério Medeiros Jr.

Proceedings of the Formal Methods: Foundations and Applications - 17th Brazilian Symposium, 2014

2013

Integration of SMT-solvers in B and Event-B development environments.

David Déharbe

Sci. Comput. Program., 2013

BEval: A Plug-in to Extend Atelier B with Current Verification Technologies.

Valério Medeiros Júnior, David Déharbe

Proceedings of the Proceedings First Latin American Workshop on Formal Methods, 2013

Computing prime implicants.

David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Special issue: International Colloquium on Theoretical Aspects of Computing - ICTAC 2010.

Ana Cavalcanti, David Déharbe

Theor. Comput. Sci., 2012

An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting.

Haniel Barbosa, David Déharbe

Proceedings of the Formal Methods: Foundations and Applications - 15th Brazilian Symposium, 2012

SMT Solvers for Rodin.

David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

Formal Verification of PLC Programs Using the B Method.

Haniel Barbosa, David Déharbe

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

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

Proceedings of the Formal Methods, Foundations and Applications - 14th Brazilian Symposium, 2011

Quantifier Inference Rules for SMT proofs.

David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

Exploiting Symmetry in SMT Problems.

David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

GridTPT: a distributed platform for Theorem Prover Testing.

Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine

Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 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

Proceedings of the Abstract State Machines, 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

Proceedings of the Abstract State Machines, 2010

Automatic Verification for a Class of Proof Obligations with SMT-Solvers.

David Déharbe

Proceedings of the Abstract State Machines, 2010

2009

Satisfiability solving for software verification.

David Déharbe, Silvio Ranise

Int. J. Softw. Tools Technol. Transf., 2009

Refining interfaces: the case of the B method

David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira

CoRR, 2009

Formal Modelling of a Microcontroller Instruction Set in B.

Valério Medeiros Júnior, David Déharbe

Proceedings of the Formal Methods: Foundations and Applications, 2009

Formalizing FreeRTOS: First Steps.

David Déharbe, Stephenson Galvão, Anamaria Martins Moreira

Proceedings of the Formal Methods: Foundations and Applications, 2009

veriT: An Open, Trustable and Efficient SMT-Solver.

Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine

Proceedings of the Automated Deduction, 2009

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

Combining Decision Procedures by (Model-)Equality Propagation.

Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine

Proceedings of the Eleventh Brazilian Symposium on Formal Methods, 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

Proceedings of the Eleventh Brazilian Symposium on Formal Methods, 2008

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

David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira

Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2006

AGraphs: Definition, implementation and tools.

David Déharbe, Anamaria Martins Moreira, Demóstenes Sena

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2006

Aspect-oriented design in systemC: implementation and applications.

David Déharbe, Sérgio Medeiros

Proceedings of the 19th Annual Symposium on Integrated Circuits and Systems Design, 2006

Decision Procedures for the Formal Analysis of Software.

David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen

Proceedings of the Theoretical Aspects of Computing, 2006

Automation of Java Card component development using the B method.

David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira

Proceedings of the 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 2006

2005

Developing Java Card Applications with B.

Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira, David Déharbe

Proceedings of the Second Brazilian Symposium on Formal Methods, 2005

Distributing the Workload in a Lazy Theorem-Prover.

David Déharbe, Silvio Ranise, Jorgiano Vidal

Proceedings of the Second Brazilian Symposium on Formal Methods, 2005

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

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

Explicit-Symbolic Modelling for Formal Verification.

Umberto Souza da Costa, Sérgio Vale Aguiar Campos, Newton Vieira, David Déharbe

Proceedings of the Seventh Brazilian Symposium on Formal Methods, 2004

Techniques for Temporal Logic Model Checking.

David Déharbe

Proceedings of the Refinement Techniques in Software Engineering, 2004

Abstraction-Driven Verification of Array Programs.

David Déharbe, Abdessamad Imine, Silvio Ranise

Proceedings of the Artificial Intelligence and Symbolic Computation, 2004

2003

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

Silvio Ranise, David Déharbe

Proceedings of the 4th International Workshop on First-Order Theorem Proving, 2003

Proving and Debugging Set-Based Specifications.

Jean-François Couchot, Frédéric Dadeau, David Déharbe, Alain Giorgetti, Silvio Ranise

Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003

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

David Déharbe, Silvio Ranise

Proceedings of the 1st International Conference on Software Engineering and Formal Methods (SEFM 2003), 2003

A Tutorial Introduction to Symbolic Model Checking.

David Déharbe

Proceedings of the Logic for Concurrency and Synchronisation, 2003

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

Proceedings of the 16th Brazilian Symposium on Software Engineering, 2002

Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae.

David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen

Proceedings of the Rewriting Techniques and Applications, 13th International Conference, 2002

Improving Static Ordering of BDDs for Reachability Analysis.

Jorgiano Vidal, David Déharbe, Dominique Borrione

Proceedings of the 11th IEEE/ACM International Workshop on Logic & Synthesis, 2002

2001

BDDmeter - Uma Ferramenta para Visualização Dinâmica de BDDs.

Sérgio Queiroz de Medeiros, David Déharbe

Proceedings of the 15th Brazilian Symposium on Software Engineering, 2001

Optimizing BDD-Based Verification Analysing Variable Dependencies.

David Déharbe, Jorgiano Márcio Bruno Vidal

Proceedings of the 14th Annual Symposium on Integrated Circuits and Systems Design, 2001

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, Vanderlei Moraes Rodrigues

RITA, 2000

Variable Ordering of BDDs with Parallel Genetic Algorithms.

Umberto Souza da Costa, David Déharbe, Anamaria Martins Moreira

Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 2000

1999

Symbolic Model Checking with Fewer Fixpoint Computations.

David Déharbe, Anamaria Martins Moreira

Proceedings of the FM'99 - Formal Methods, 1999

1998

Formal Verification of VHDL ¾ The Model Checker CV.

David Déharbe, Subash Shankar, Edmund M. Clarke

Proceedings of the 11th Annual Symposium on Integrated Circuits Design, 1998

Model Checking VHDL with CV.

David Déharbe, Subash Shankar, Edmund M. Clarke

Proceedings of the Formal Methods in Computer-Aided Design, 1998

1997

Using induction and BDDs to model check invariants.

David Déharbe, Anamaria Martins Moreira

Proceedings of the Advances in Hardware Design and Verification, 1997

1996

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

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

1995

Semantics of a verification-oriented subset of VHDL.

David Déharbe, Dominique Borrione

Proceedings of the Correct Hardware Design and Verification Methods, 1995