default search action
David Déharbe
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2022
- [c54]Lilian Burdy, David Déharbe, Denis Sabatier:
Assigning Safe Executed Systems to Meanings. RSSRail 2022: 130-142 - [e2]David Déharbe, Antti E. J. Hyvärinen:
Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11-12, 2022. CEUR Workshop Proceedings 3185, CEUR-WS.org 2022 [contents] - 2020
- [j13]Thierry Lecomte
, David Déharbe
The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199: 102524 (2020) - [c53]Héctor Ruíz Barradas, Lilian Burdy, David Déharbe:
Existence Proof Obligations for Constraints, Properties and Invariants in Atelier B. ABZ 2020: 255-259 - [i4]Thierry Lecomte
Applying a Formal Method in Industry: a 25-Year Trajectory. CoRR abs/2005.07190 (2020) - [i3]Thierry Lecomte
Low Cost High Integrity Platform. CoRR abs/2005.07191 (2020) - [i2]Thierry Lecomte
The CLEARSY Safety Platform: 5 Years of Research, Development and Deployment. CoRR abs/2005.10662 (2020)
2010 – 2019
- 2019
- [j12]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): 221-259 (2019) - [c52]Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez:
Property-Driven Software Analysis - (Extended Abstract). FM 2019: 746-750 - [c51]Dalay Israel de Almeida Pereira
B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution. RSSRail 2019: 242-258 - [c50]Diego de Azevedo Oliveira, Valério Medeiros Jr.
BTestBox: A Tool for Testing B Translators and Coverage of B Models. TAP@FM 2019: 83-92 - 2018
- [c49]Lilian Burdy, David Déharbe:
Teaching an Old Dog New Tricks - The Drudges of the Interactive Prover in Atelier B. ABZ 2018: 415-419 - 2017
- [c48]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: 148-159 - [c47]Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin:
Applying a Formal Method in Industry: A 25-Year Trajectory. SBMF 2017: 70-87 - 2016
- [c46]Lilian Burdy, David Déharbe, Étienne Prun:
Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa". F-IDE@FM 2016: 82-90 - 2015
- [c45]David Déharbe, Stephan Merz:
Software Component Design with the B Method - A Formalization in Isabelle/HOL. FACS 2015: 31-47 - [c44]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: 76-91 - 2014
- [j11]David R. Cok, David Déharbe, Tjark Weber:
The 2014 SMT Competition. J. Satisf. Boolean Model. Comput. 9(1): 207-242 (2014) - [j10]David Déharbe
Integrating SMT solvers in Rodin. Sci. Comput. Program. 94: 130-143 (2014) - [c43]Richard Bonichon, David Déharbe, Thierry Lecomte
LLVM-Based Code Generation for B. SBMF 2014: 1-16 - [c42]Richard Bonichon, David Déharbe, Cláudia Tavares:
Extending SMT-LIB v2 with λ-Terms and Polymorphism. SMT 2014: 53-62 - 2013
- [j9]David Déharbe:
Integration of SMT-solvers in B and Event-B development environments. Sci. Comput. Program. 78(3): 310-326 (2013) - [c41]David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure:
Computing prime implicants. FMCAD 2013: 46-52 - [c40]Valério Medeiros Júnior, David Déharbe:
BEval: A Plug-in to Extend Atelier B with Current Verification Technologies. LAFM 2013: 53-58 - 2012
- [j8]Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine:
Combining decision procedures by (model-)equality propagation. Sci. Comput. Program. 77(4): 518-532 (2012) - [j7]Ana Cavalcanti
Special issue: International Colloquium on Theoretical Aspects of Computing - ICTAC 2010. Theor. Comput. Sci. 455: 1 (2012) - [c39]David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin:
SMT Solvers for Rodin. ABZ 2012: 194-207 - [c38]Haniel Barbosa
Formal Verification of PLC Programs Using the B Method. ABZ 2012: 353-356 - [c37]Haniel Barbosa
An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. SBMF 2012: 19-34 - 2011
- [c36]David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo:
Exploiting Symmetry in SMT Problems. CADE 2011: 222-236 - [c35]David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo:
Quantifier Inference Rules for SMT proofs. PxTP 2011: 33-39 - [c34]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: 44-59 - 2010
- [c33]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: 203-216 - [c32]David Déharbe:
Automatic Verification for a Class of Proof Obligations with SMT-Solvers. ASM 2010: 217-230 - [c31]Alessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Vinícius Medeiros Oliveira, David Boris Paul Déharbe:
Integrating SMT-Solvers in Z and B Tools. ASM 2010: 412-413 - [c30]Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine:
GridTPT: a distributed platform for Theorem Prover Testing. PAAR@IJCAR 2010: 33-39 - [e1]Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, Jim Woodcock
Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings. Lecture Notes in Computer Science 6255, Springer 2010, ISBN 978-3-642-14807-1 [contents]
2000 – 2009
- 2009
- [j6]David Déharbe, Silvio Ranise
Satisfiability solving for software verification. Int. J. Softw. Tools Technol. Transf. 11(3): 255-260 (2009) - [c29]Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine:
veriT: An Open, Trustable and Efficient SMT-Solver. CADE 2009: 151-156 - [c28]David Déharbe, Stephenson Galvão, Anamaria Martins Moreira:
Formalizing FreeRTOS: First Steps. SBMF 2009: 101-117 - [c27]Valério Medeiros Júnior, David Déharbe:
Formal Modelling of a Microcontroller Instruction Set in B. SBMF 2009: 282-289 - [i1]David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira:
Refining interfaces: the case of the B method. CoRR abs/0907.2039 (2009) - 2008
- [j5]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): 71-86 (2008) - [c26]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: 351-352 - [c25]Bartira Dantas, David Déharbe
Verified Compilation and the B Method: A Proposal and a First Appraisal. SBMF 2008: 79-96 - [c24]Diego Caminha Barbosa De Oliveira, David Déharbe
Combining Decision Procedures by (Model-)Equality Propagation. SBMF 2008: 113-128 - 2006
- [j4]David Déharbe, Anamaria Martins Moreira, Demóstenes Sena:
AGraphs: Definition, implementation and tools. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 1 (2006) - [c23]David Déharbe, Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira:
Automation of Java Card component development using the B method. ICECCS 2006: 259-268 - [c22]David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen:
Decision Procedures for the Formal Analysis of Software. ICTAC 2006: 366-370 - [c21]David Déharbe, Sérgio Medeiros
Aspect-oriented design in systemC: implementation and applications. SBCCI 2006: 119-124 - 2005
- [c20]David Déharbe
Distributing the Workload in a Lazy Theorem-Prover. SBMF 2005: 21-37 - [c19]Bruno Emerson Gurgel Gomes, Anamaria Martins Moreira, David Déharbe
Developing Java Card Applications with B. SBMF 2005: 81-96 - 2004
- [j3]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): 17-36 (2004) - [j2]Anamaria Martins Moreira, Christophe Ringeissen, David Déharbe
Manipulating algebraic specifications with term-based and graph-based representations. J. Log. Algebraic Methods Program. 59(1-2): 63-87 (2004) - [c18]David Déharbe, Abdessamad Imine, Silvio Ranise:
Abstraction-Driven Verification of Array Programs. AISC 2004: 271-275 - [c17]David Déharbe:
Techniques for Temporal Logic Model Checking. PSSE 2004: 315-367 - [c16]Umberto Souza da Costa, Sérgio Vale Aguiar Campos, Newton Vieira, David Déharbe
Explicit-Symbolic Modelling for Formal Verification. SBMF 2004: 301-321 - 2003
- [c15]David Déharbe, Silvio Ranise
Light-Weight Theorem Proving for Debugging and Verifying Units of Code. SEFM 2003: 220-228 - [c14]Silvio Ranise
Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. FTP 2003: 105-119 - [c13]Jean-François Couchot, Frédéric Dadeau, David Déharbe
Proving and Debugging Set-Based Specifications. WMF 2003: 189-208 - [p1]David Déharbe:
A Tutorial Introduction to Symbolic Model Checking. Logic for Concurrency and Synchronisation 2003: 215-237 - 2002
- [c12]Jorgiano Vidal, David Déharbe, Dominique Borrione:
Improving Static Ordering of BDDs for Reachability Analysis. IWLS 2002: 73-77 - [c11]David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen:
Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. RTA 2002: 207-221 - [c10]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: 396-401 - 2001
- [c9]David Déharbe, Jorgiano Márcio Bruno Vidal:
Optimizing BDD-Based Verification Analysing Variable Dependencies. SBCCI 2001: 64-71 - [c8]Sérgio Queiroz de Medeiros, David Déharbe:
BDDmeter - Uma Ferramenta para Visualização Dinâmica de BDDs. SBES 2001: 350-355 - 2000
- [j1]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): 7-48 (2000) - [c7]Umberto Souza da Costa, David Déharbe, Anamaria Martins Moreira:
Variable Ordering of BDDs with Parallel Genetic Algorithms. PDPTA 2000
1990 – 1999
- 1999
- [c6]David Déharbe, Anamaria Martins Moreira:
Symbolic Model Checking with Fewer Fixpoint Computations. World Congress on Formal Methods 1999: 272-288 - 1998
- [c5]David Déharbe, Subash Shankar, Edmund M. Clarke:
Model Checking VHDL with CV. FMCAD 1998: 508-514 - [c4]David Déharbe, Subash Shankar, Edmund M. Clarke:
Formal Verification of VHDL ¾ The Model Checker CV. SBCCI 1998: 95-98 - 1997
- [c3]David Déharbe, Anamaria Martins Moreira:
Using induction and BDDs to model check invariants. CHARME 1997: 203-213 - 1996
- [c2]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: 450-467 - 1995
- [c1]David Déharbe, Dominique Borrione:
Semantics of a verification-oriented subset of VHDL. CHARME 1995: 293-310
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-04-25 05:47 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: