| 15 | 14 | 13 | 12 | 11 | 10 | 09 | 08 | 07 | 06 | 05 | 04 | 03 | 02 | 01 | 00 | 99 | 98 | 97 | 96 | 95 | 93 | 91 |


2015

SMTpp: preprocessors and analyzers for SMT-LIB. Richard Bonichon, David Déharbe, Pablo Dobal, Cláudia Tavares. Proceedings of the 13th International Workshop on Satisfiability Modulo Theories (SMT 2015). Accepted. [ PDF ].

Verifying Code Generation Tools for the B-Method Using Tests: a Case Study. Ernesto C. B. de Matos, David Déharbe, Anamaria M. Moreira, Cleverton Hentz, Valério de Medeiros Jr. and João B. Souza Neto. 9th International Conference on Tests & Proofs (TAP 2015). Accepted. [ PDF ]


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, (SMT 2014). CEUR Workshop Proceedings, vol. 1163, p. 53-62. [ BibTeX | PDF | online ].

Integrating SMT solvers in Rodin. David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. Science of Computer Programming. In press, accepted manuscript. [ BibTeX | PDF (uncorrected proof) ]. DOI: 10.1016/j.scico.2014.04.012.

BEval: a plug-in to extend Atelier B with current verification technologies. Valério Medeiros Jr, David Déharbe. In Nazareno Aguirre and Leila Ribeiro: Proceedings First Latin American Workshop on Formal Methods (LAFM 2013), Buenos Aires, Argentina, Electronic Proceedings in Theoretical Computer Science 139, pp. 53–58. [ Final version ]. DOI: 10.4204/EPTCS.139.5.


2013

Computing prime implicants. David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), p.46-52. Portland, USA. October, 2013. [ Final version

SyMT: finding symmetries in SMT formulas (Extended Abstract: Work in progress). Carlos Areces, David Deharbe, Pascal Fontaine and Ezequiel Orbe. 11th International Workshop on Satisfiability Modulo Theories. Helsinki, Finland. July, 2013. [ Submitted version ]

Le solveur SMT veriT. David Déharbe, Pablo Federico Dobal and Pascal Fontaine. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2013).
Tool demonstration. [ Submitted short paper (in French) ]

Integration of SMT-solvers in B and Event-B development environments. David Déharbe. Science of Computer Programming. Vol. 78, nº 3. p. 310-316. Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010. Edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau and Steve Reeves. DOI: 10.1016/j.scico.2011.03.007. [ Preprint ]


2012

An approach using the B method to formal verification of PLC programs in an industrial setting. Haniel Barbosa and David Déharbe. Formal Methods: Foundations and Applications (SBMF 2012). Lecture Notes in Computer Science, 2012, Vol. 7498/2012, 19-34. DOI: 10.1007/978-3-642-33296-8_4. [ Preprint ]

Combining decision procedures by (model-)equality propagation. Diego Oliveira, David Déharbe and Pascal Fontaine. Science of Computer Programming (Print), Vol. 77, p. 518-532, 2012. DOI: 10.1016/j.scico.2010.04.003. [ PDF ]

GridTPT: a distributed platform for Theorem Prover Testing. Thomas Bouton, Diego Caminha, David Déharbe and Pascal Fontaine. EPiC series, Vol. 9, p.33-39.  PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning. Renate A. Schmidt and Stephan Schulz and Boris Konev Editors. 2012. [ PDF ]

Experience in modeling a micro-controller instruction set using B
. Valério Medeiros and David Déharbe. Brazilian Symposium on Formal Methods (SBMF 2012). Short paper. [ PDF ]

SMT Solvers for Rodin. David Déharbe, Pascal Fontaine, Yoann Guyot and Laurent Voisin. In Proc. Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012). Lecture Notes in Computer Science, 2012, Vol. 7316/2012, 194-207, DOI: 10.1007/978-3-642-30885-7_14. [ PDF ]

Special issue: International Colloquium on Theoretical Aspects of Computing — ICTAC 2010. Ana Cavalcanti, David Déharbe. Theoretical Computer Science, Vol. 455. DOI: 10.1016/j.tcs.2012.07.024.

Formal Verification of PLC Programs Using the B Method. Haniel Barbosa and David Déharbe. In Proc. Abstract State Machines, Alloy, B, VDM, and Z (ABZ 2012). Lecture Notes in Computer Science, 2012, Vol. 7316/2012, 353-356, DOI: 10.1007/978-3-642-30885-7_30. [ Preprint ]

2011

Exploiting Symmetry in SMT Problems. David Déharbe, Pascal Fontaine, Stephan Merz and Bruno Wolzenlogel Paleo. Automated Deduction – CADE-23. Lecture Notes in Computer Science, Vol. 6803/2011, p. 222-236. DOI: 10.1007/978-3-642-22438-6_18. [ Preprint ]

B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. Marcel Oliveira, David Déharbe and Luis Cruz. Formal Methods: Foundations and Applications (SBMF 2011). Lecture Notes in Computer Science, Vol. 7021/2011, p. 44-59. DOI: 10.1007/978-3-642-25032-3_4. [ Preprint ]

Quantifier Inference Rules for SMT Proofs. David Déharbe, Pascal Fontaine and Bruno Woltzenlogel Paleo. First Workshop on Proof eXchange for Theorem Proving, affiliated with the 23rd International Conference on Automated Deduction (CADE 23). 2011. [ Final version ]

2010

Automatic Verification for a Class of Proof Obligations with SMT-Solvers. David Déharbe. Abstract State Machines, Alloy, B and Z (ABZ 2010). Lecture Notes in Computer Science, Vol 5977/2010, p. 217-230. DOI: 10.1007/978-3-642-11811-1_17.

Applying the B Method for the Rigorous Development of Smart Card Applications. Bruno Gomes, David Déharbe, Anamaria Moreira and Katia Moraes. Abstract State Machines, Alloy, B and Z (ABZ 2010). Lecture Notes in Computer Science, Vol 5977/2010. DOI: 10.1007/978-3-642-11811-1_16.

Theoretical Aspects of Computing (ICTAC 201o), 7th International Colloquium. Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel and Jim Woodcock. Lecture Notes in Computer Science, Vol 6255/2010. DOI: 10.1007/978-3-642-14808-8.

Integrating SMT-Solvers in Z and B Tools. Alessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Oliveira and David Déharbe. Abstract State Machines, Alloy, B and Z (ABZ 2010). Lecture Notes in Computer Science, Vol 5977/2010, p. 412-413. DOI: 10.1007/978-3-642-11811-1_45.

2009

Satisfiability solving for software verification. David Déharbe, Silvio Ranise. International Journal on Software Tools for Technology Transfer, Vol. 11, p. 255-260. DOI: 10.1007/s10009-009-0105-6.

veriT: An Open, Trustable and Efficient SMT-Solver. Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine 22nd International Conference on Automated Deduction, 2009, Montreal, Canada. Automated Deduction (CADE-22). Lecture Notes in Computer Science, Vol. 5663/2009, p. 151-156. DOI: 10.1007/978-3-642-02959-2_12.

Formal Modelling of a Microcontroller Instruction Set in B. Valério Medeiros, David Déharbe. Formal Methods: Foundations and Applications – XII Brazilian Symposium on Formal Methods (SBMF 2009). Lecture Notes in Computer Science Vol. 5902/2009, p. 282-289. DOI: 10.1007/978-3-642-10452-7_19.

Formalizing FreeRTOS: First Steps. David Déharbe, Stephenson Galvão, Anamaria Martins Moreira. Formal Methods: Foundations and Applications – XII Brazilian Symposium on Formal Methods (SBMF 2009). Lecture Notes in Computer Science Vol. 5902/2009, p. 101-117. DOI: 10.1007/978-3-642-10452-7_8.

Combining Decision Procedures by (Model-)Equality Propagation. Diego Caminha, David Déharbe, Pascal Fontaine. XI Brazilian Symposium on Formal Methods (SBMF 2008). Electronic Notes in Theoretical Computer Science, Vol. 240, p. 113-128. DOI: 10.1016/j.entcs.2009.05.048.

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. XI Brazilian Symposium on Formal Methods (SBMF 2008). Electronic Notes in Theoretical Computer Science, Vol. 240, p. 79-96. DOI: 10.1016/j.entcs.2009.05.046.


2008

BSmart: A Tool for the Development of Java Card Applications with the B Method. David Déharbe, Bruno Gomes, Anamaria Martins Moreira. Abstract State Machines, B and Z (ABZ 2008). Lecture Notes in Computer Science, Vol. 5238/2008, p. 351-352. DOI: 10.1007/978-3-540-87603-8.

A prototype implementation of a distributed Satisfiability Modulo Theories solver in the ToolBus framework. David Déharbe, Silvio Ranise,  Jorgiano Vidal. Journal of the Brazilian Computer Society (Springer), Vol. 14, nº 1, p. 71-86. DOI: 10.1007/BF03192553.

Proposta e Avaliação de uma Abordagem de Desenvolvimento de Software Fidedigno por Construção com o Método B. Bartira Dantas, David Déharbe, Stephenson Galvão, Anamaria Martins Moreira, Valério Medeiros Júnior. XXXV Seminário Integrado de Software e Hardware (SEMISH 2008), 2008, Belém, PA. Anais do XXXV Seminário Integrado de Software e Hardware (SEMISH 2008), 2008. v. 1. p. 1-15.

Applying the B method to take on the grand challenge of verified compilation. David Déharbe. Brazilian Symposium on Formal Methods (SBMF2008). Editora Gráfica da UFBA - EDUFBA, 2008. v. 1. p. 35-50.


2007

Developing Java Card Applications with B. Bruno Gomes, Anamaria Martins Moreira, David Déharbe. Brazilian Symposium on Formal Methods (SBMF 2005). Electronic Notes in Theoretical Computer Science, Vol. 184, p. 81-96. DOI: 10.1016/j.entcs.2007.03.016.

Distributing the Workload in a Lazy Theorem-Prover. David Deharbe, Silvio Ranise, Jorgiano Vidal. Brazilian Symposium on Formal Methods (SBMF 2005). Electronic Notes in Theoretical Computer Science, Vol. 184, p. 21-37. DOI: 10.1016/j.entcs.2007.03.013.


2006

Decision Procedures for the Formal Analysis of Software. David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen. Theoretical Aspects of Computing (ICTAC 2006). Lecture Notes in Computer Science, Vol. 4281/2006, p. 366-370. DOI: 10.1007/11921240_26.

Techniques for Temporal Logic Model Checking. David Déharbe. Refinement Techniques in Software Engineering – First Pernambuco Summer School on Software Engineering, (PSSE 2004).  Lecture Notes in Computer Science, Vol. 3167/2006, p. 315-367. DOI: 10.1007/11889229_8.

haRVey: combining reasoners. David Déharbe, Pascal Fontaine. Sixth International Workshop on Automated Verification of Critical Systems (AVOCS'06). v. 1. p. 1-5.

Agraphs: Definition, implementation and tools. David Déharbe, Anamaria Martins Moreira, Demóstenes Sena. Electronic Communications of the EASST, v. 1, p. 1-13, 2006.


2005

Explicit-Symbolic Modelling for Formal Verification. Umberto Costa, Sérgio Campos, Newton Vieira, David Déharbe. VII Brazilian Workshop on Formal Methods (WMF'2004). Electronic Notes in Theoretical Computer Science, Vol. 130, p. 301-321. DOI: 10.1016/j.entcs.2005.03.016.


2004

Proving and Debugging Set-Based Specifications. Jean-François Couchot, Frédéric Dadeau, David Déharbe, A. Giorgetti, S. Ranise. VI Brazilian Workshop on Formal Methods (WMF'2003). Electronic Notes in Theoretical Computer Science, Vol. 95, p. 189–208. DOI: 10.1016/j.entcs.2004.04.012.

Abstraction-Driven Verification of Array Programs. David Déharbe, Abdessamad Imine, Silvio Ranise. Artificial Intelligence and Symbolic Compution (AISC'2004).  Lecture Notes in Computer Science, Volume 3249/2004, 143-146, DOI: 10.1007/978-3-540-30210-0_23.

Evolving algebraic specifications with term-based and graph-based representations. Anamaria Martins Moreira, Christophe Ringeisse, David Déharbe, Gleydson Lima. Journal of Logic and Algebraic Programming, v. 59, n.1/2, p. 63-87. DOI: 10.1016/j.jlap.2003.12.001.


2003

Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. Silvio Ranise, David Déharbe. 4th International Workshop on First-Order Theorem Proving (FTP'2003). Electronic Notes in Theoretical Computer Science, Vol. 86, p. 105-119. DOI: 10.1016/S1571-0661(04)80656-X.

A Tutorial Introduction to Symbolic Model Checking. David Déharbe. Logic for Concurrency and Synchronisation. Trends in Logic, Vol. 15-II, p. 215-237. DOI: 10.1007/0-306-48088-3_5.


2002

Improving Symbolic Model Checking by Rewriting Temporal Logic Formulae. David Déharbe, Anamaria Martins Moreira, Christophe Ringeissen. 13th International Conference on Rewriting Techniques and Application (RTA 2002). Lecture Notes in Computer Science, Vol. 2378/2002, p. 207-221. DOI: 10.1007/3-540-45610-4_15.

BDD-Driven First-Order Satisfiability Procedures (Extended Version). David Déharbe, Silvio Ranise. INRIA Research Report RR-4630, 24 pages. 2002.

Improving Static Ordering of BDDs for Reachability Analysis. Jorgiano Vidal, David Déharbe, Dominique Borrione. IEEE/ACM 11th International Workshop on Logic & Synthesis (IWLS 2002). Pages 73-77. June 4-7, 2002, New Orleans, Louisiana, USA. IEEE Computer Society & ACM SIGDA.


2001

Advances in BDD reduction using Parallel Genetic Algorithms. Umberto Costa, Anamaria Martins Moreira, David Déharbe.IEEE 10th International Workshop on Logic & Synthesis (IWLS'2001), v. 1. p. 84-89.

Optimizing BDD-based verification analysing variable dependencies. David Déharbe, Jorgiano Vidal. XIV Symposium on Integrated Circuits and System Design (SBCCI 2001), v. 1. p. 64-70. DOI: 10.1109/SBCCI.2001.953005

2000

Variable Ordering of BDDs with Parallel Genetic Algorithms. Umberto Costa, David Déharbe, Anamaria Martins Moreira. Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA 2000). Preprint.

A cache-based parallel genetic algorithm for the BDD variable ordering problem
. Umberto Costa, David Déharbe, Anamaria Martins Moreira.. 12th Symposium on Computer Architecture and High Performance Computing (SPAC-PAD'2000), p.99-105. Preprint.

An Architectural Description of Enterprise Java Beans. Bartira Dantas, David Déharbe, Virgínia de Paula. Electronic Notes in Theoretical Computer Science, Vol. 38, p. 1-14.

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. Revista de Informática Teórica e Aplicada - RITA. Volume 7, nº 1, p. 7-48.

Comparação entre descrições formais da arquitetura Enterprise Java Beans. Bartira Dantas, David Déharbe, Virgínia de Paula. III Workshop Brasileiro de Métodos Formais (WMF'00). Preprint.

1999

Symbolic Model Checking with Fewer Fixpoint Computations. David Déharbe, Anamaria Moreira. FM’99 — Formal Methods. Lecture Notes in Computer Science, Vol. 1708/1999, p. 272-288. DOI: 10.1007/3-540-48119-2_17.

1998

Model Checking VHDL with CV. David Déharbe, Subash Shankar and Edmund Clarke. Formal Methods in Computer-Aided Design (FMCAD'98). Lecture Notes in Computer Science, Volume 1522/1998, p. 522-522. DOI: 10.1007/3-540-49519-3_33.

Slicing: a Novel Approach for BDD-Based Modeling of VHDL. David Déharbe. I Workshop Brasileiro de Métodos Formais (WMF'98). Porto Alegre, RS.

Formal Verification of VHDL The Model Checker CV. David Déharbe, Subash Shankar, Edmund Clarke. XI Brazilian Symposium on Integrated Circuits and Systems (SBCCI'98), p.95-98. DOI:  10.1109/SBCCI.1998.715418.

1997

Using Induction and BDDs to Model Check Invariants. David Déharbe, Anamaria Martins Moreira. Proceedings of the IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods: Advances in Hardware Design and Verification (CHARME'97), p.  203 - 213.

1996

HDL-based integration of formal methods and CAD tools in the PREVAIL environment. Dominique Borrione, Hakim Bouamama, David Déharbe, Claude Le Faou, Ayman Wahba. 1st Internal Conference on Formal Methods in Computer-Aided Design (FMCAD '96). Lecture Notes in Computer Science, Volume 1166/1996, p. 450-467. DOI: 10.1007/BFb0031827.

Vérification formelle de propriétés temporelles: étude et application au langage VHDL. David Déharbe. Doctoral thesis. Université de Grenoble (then Université Joseph Fourier - Grenoble 1). In French.

1995

Semantics of a verification-oriented subset of VHDL. David Déharbe and Dominique Borrione. Correct Hardware Design and Verification Methods (CHARME'95). Lecture Notes in Computer Science, Vol. 987/1995, p. 293-310. DOI: 10.1007/3-540-60385-9_18.

1993

Symbolic model checking of VHDL design entities. David Déharbe and Dominique Borrione. Research report RR-925-I. Lab Artemis-IMAG, Grenoble, France.

Model checking on finite-state machines: extensions and applications to VHDL designs
. David Déharbe. First Asian-Pacific Conference on Hardware Description Languages: Standards and Applications (APCHDLSA'93), Brisbane, Australia.

1991

Application of a BDD package to the Verification of HDL Descriptions. Dominique Borrione, David Déharbe, Hans Eveking, Stephan Höreth. Advanced Research Workshop on Correct Hardware Design Methodologies (CHARME'91), Turin, Italia. North Holland.