Publications

David Deharbe's photo
This page displays the full list of journal papers, book chapters and technical reports that I have contributed to. It also includese papers published in conference and workshop proceedings since 2010.

See also:

Technical Reports 4

  • Bartira Dantas, David Déharbe, Stephenson Galvão, Anamaria Moreira, Valério Gutemberg. Verified Compilation based on the B method: An initial appraisal (extended version). DIMAp/UFRN, UFRN-DIMAp-2008-101-RT, 2008.
  • David Déharbe, Silvio Ranise. BDD-Driven First-Order Satisfiability Procedures (Extended Version). Institut National de Recherche in Informatique et en Automatique (INRIA), 4630, 2002.
  • Ayman Wahba, David Déharbe. Design Error Diagnosis in Logic Circuits Using Ternary Test Sets. IMAG, RR-93-928-M, 1993.
  • Dominique Borrione, David Déharbe. Symbolic model checking of VHDL design entities. IMAG, RR-93-925-I, 1993.

Book Chapters 3

  • David Déharbe. Techniques for Temporal Logic Model Checking. Refinement Techniques in Software Engineering. Lecture Notes in Computer Science, volume 3167, . Edited by Ana Cavalcanti, Augusto Sampaio, Jim Woodcock. First Pernambuco Summer School on Software Engineering, PSSE 2004. doi: 10.1007/11889229
  • David Déharbe. A tutorial introduction to symbolic model checking. Logic for Concurrency and Synchronisation. volume 1, . Edited by Ruy J.G.B. de Queiroz. Kluwer Academic Publisher. doi: 10.1007/0-306-48088-3
  • David Déharbe, Dominique Borrione. Symbolic Model Checking with Past and Future Temporal Modalities: Fundamentals and Algorithms. Model Generation in Electronic Design. Current Issues in Electronic Modeling, volume 1, . Edited by Jean-Michel Bergé, Oz Levia, Jacques Rouillard. doi: 10.1007/978-1-4615-2335-2_7

Thesis 1

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

Journal Papers 16

  • Tjark Weber, Sylvain Conchon, David Déharbe, Matthias Heizmann, Aina Niemetz, Gies Reger. The SMT Competition 2015-2018. JSAT: Journal on Satisfiability, Boolean Modeling and Computation, volume 11. IOS Press. doi: 10.3233/SAT190123
  • David R. Cok, David Déharbe, Tjark Weber. The 2014 SMT Competition. JSAT: Journal on Satisfiability, Boolean Modeling and Computation, volume 9. https://satassociation.org/jsat/index.php/jsat/article/view/122
  • David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. Integrating SMT solvers in Rodin. Science of Computer Programming, volume 94(2). 15 November 2014. doi: 10.1016/j.scico.2014.04.012
  • David Déharbe. Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming, volume 78(3). 01 March 2013. Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010. doi: 10.1016/j.scico.2011.03.007
  • Ana Cavalcanti, David Déharbe. Special issue: International Colloquium on Theoretical Aspects of Computing — ICTAC 2010. Theoretical Computer Science, volume 455. 12 October 2012. Elsevier. doi: 10.1016/j.tcs.2012.07.024
  • Diego Oliveira, David Déharbe, Pascal Fontaine. Combining decision procedures by (model-)equality propagation. Science of Computer Programming, volume 77(4). 01 April 2012. doi: 10.1016/j.scico.2010.04.003
  • Bartira Dantas, David Déharbe, Stephenson Galvão, Anamaria Martins Moreira, Valério Medeiros Jr. Verified Compilation and the B Method: A Proposal and a First Appraisal. Electronic Notes in Theoretical Computer Science, volume 240. 02 July 2009. Proceedings of the XI Brazilian Symposium on Formal Methods (SBMF 2008). doi: 10.1016/j.entcs.2009.05.046
  • Diego Caminha, David Déharbe, Pascal Fontaine. Combining Decision Procedures by (Model-)Equality Propagation. Electronic Notes in Theoretical Computer Science, volume 240. 02 July 2009. Proceedings of the XI Brazilian Symposium on Formal Methods (SBMF 2008). doi: 10.1016/j.entcs.2009.05.048
  • David Déharbe, Silvio Ranise. Satisfiability solving for software verification. International Journal on Software Tools for Technology Transfer, volume 11(3). 24 March 2009. doi: 10.1007/s10009-009-0105-6
  • David Déharbe, Silvio Ranise, Jorgiano Vidal. A prototype implementation of a distributed Satisfiability Modulo Theories solver in the ToolBus framework. Journal of the Brazilian Computer Society, volume 14(1). 01 March 2008. doi: 10.1007/BF03192553
  • David Déharbe, Silvio Ranise, Jorgiano Vidal. Distributing the Workload in a Lazy Theorem-Prover. Electronic Notes in Theoretical Computer Science, volume 184. 12 July 2007. Proceedings of the Brazilian Symposium on Formal Methods (SBMF 2005). doi: 10.1016/j.entcs.2007.03.013
  • Bruno Gomes, Anamaria Martins Moreira, David Déharbe. Developing Java Card Applications with B. Electronic Notes in Theoretical Computer Science, volume 184. 12 July 2007. Proceedings of the Brazilian Symposium on Formal Methods (SBMF 2005). doi: 10.1016/j.entcs.2007.03.016
  • Umberto Costa, Sérgio Campos, Newton Vieira, David Déharbe. Explicit-symbolic modelling for formal verification. Electronic Notes in Theoretical Computer Science, volume 130. 12 May 2005. Proceedings of the VII Brazilian Workshop on Formal Methods (WMF'2004). doi: 10.1016/j.entcs.2005.03.016
  • Anamaria Martins Moreira, Christophe Ringeissen, David Déharbe, Gleydson Lima. Evolving algebraic specifications with term-based and graph-based representations.. Journal of Logic and Algebraic Programming, volume 59(1/2). 11 February 2004. doi: 10.1016/j.jlap.2003.12.001
  • Silvio Ranise, David Déharbe. Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs. Electronic Notes in Theoretical Computer Science, volume 86(1). 01 May 2003. Proceedings of the 4th International Workshop on First-Order Theorem Proving (FTP'2003). doi: 10.1016/S1571-0661(04)80656-X.
  • David Déharbe, Anamaria Martins Moreira, Leila Ribeiro, Vanderlei Moraes Rodrigues. Especificação, Semântica e Verificação de Sistemas Concorrentes. Revista de Informática Teórica e Aplicada, volume 7(1). 01 September 2000.

Papers in Conference Proceedings

  • Thierry Lecomte, David Déharbe, Denis Sabatier, Etienne Prun, Patrick Péronne, Emmanuel Chailloux, Steven Varoumas, Adilla Susungi, Sylvain Conchon. Low Cost High Integrity Platform. In Proc. 10th European Congress on Embedded Real Time Systems. Edited by Dirk Beyer, Chantal Keller. 2020. Toulouse, France. https://hal.archives-ouvertes.fr/hal-02446132/document
  • Diego de Azevedo Oliveira, Valério Medeiros, David Déharbe, Martin A. Musicante. BTestBox: A Tool for Testing B Translators and Coverage of B Models. In Proc. Test and Proofs. Edited by Dirk Beyer, Chantal Keller. Lecture Notes in Computer Science, volume 11823 Pages 83-92. 2019. Porto, Portugal. Springer. doi: 10.1007/978-3-030-31157-5_6
  • Dalay Israel de Almeida Pereira, David Déharbe, Matthieu Perrin, Philippe Bon. B-Specification of Relay-Based Railway Interlocking Systems Based on the Propositional Logic of the System State Evolution. In Proc. Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification. Edited by Simon Collart Dutilleul, Thierry Lecomte, Alexander B. Romanovsky. Lecture Notes in Computer Science, volume 11495 Pages 242-258. 2019. Lille, France. Springer. doi: 10.1007/978-3-030-18744-6_16
  • Lilian Burdy, David Déharbe. Teaching an Old Dog New Tricks: The Drudges of the Interactive Prover in Atelier B. In Proc. Abstract State Machines, Alloy, B, TLA, VDM, and Z. Edited by Michael Butler, Alexander Raschke, Thai Son Hoang, Klaus Reichl. Lecture Notes in Computer Science, volume 10817 Pages 415-419. 2018. Southampton, UK. Springer. doi: 10.1007/978-3-319-91271-4_33
  • Thierry Lecomte, David Déharbe, Étienne Prun, Erwan Mottin. Applying a Formal Method in Industry: A 25-Year Trajectory. In Proc. Formal Methods: Foundations and Applications. Edited by Simone Cavalheiro, José Fiadeiro. Lecture Notes in Computer Science, volume 10623 Pages 70-87. 2017. Recife, Brazil. Springer. doi: 10.1007/978-3-319-70848-5_6
  • Mathieu Comptier, David Déharbe, Julien Molinero Perez, Louis Mussat, Thibaut Pierre, Denis Sabatier. Safety Analysis of a CBTC System: A Rigorous Approach with Event-B. In Proc. Reliability, Safety, and Security of Railway Systems: Modelling, Analysis, Verification, and Certification. Edited by Alessandro Fantechi, Thierry Lecomte, Alexander Romanovsky. Lecture Notes in Computer Science, volume 10598 Pages 148-159. 2017. Pistoia, Italy. Springer. doi: 10.1007/978-3-319-68499-4_10
  • David Déharbe, Stephan Merz. Software component design with the B method – a formalization in Isabelle/HOL. In Proc. 12th International Conference on Formal Aspects of Component Software, FACS 2015. Edited by Christiano Braga, Peter Ölveczky. Lecture Notes in Computer Science, volume 9539 Pages 31-47. 2016. Niteroi, Brasil. Springer.
  • Anamaria M. Moreira, Cleverton Hentz, David Déharbe, Ernesto Matos, João Souza Neto, Valério de Medeiros Jr. Verifying Code Generation Tools for the B-Method Using Tests: A Case Study. In Proc. Tests and Proofs, 9th International Conference, TAP 2015. Edited by Jasmin Blanchette, Nikolai Kosmatov. Lecture Notes in Computer Science, volume 9154 Pages 76-91. 2015. L'Aquila, Italy. Springer. doi: 10.1007/978-3-319-2125-9_5
  • Richard Bonichon, David Déharbe, Thierry Lecomte, Valério Medeiros Jr. LLVM-Based Code Generation for B. In Proc. Formal Methods, Foundations and Applications. Edited by Christiano Braga, Narciso Martí-Oliet. Lecture Notes in Computer Science, volume 8941 Pages 1-16. 2014. Maceió, Brazil. Springer Berlin Heidelberg. doi: 10.1007/978-3-319-15075-8_1
  • David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure. Computing prime implicants. In Proc. Proc 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013). Edited by Barbara Jobstmann, Sandip Ray. Pages 46-52. 01 October 2013. Portland, USA.
  • Haniel Barbosa, David Déharbe. An Approach Using the B Method to Formal Verification of PLC Programs in an Industrial Setting. In Proc. Formal Methods: Foundations and Applications. Edited by Rohit Gheyi, David Naumann. Lecture Notes in Computer Science, volume 7498 Pages 19-34. 2012. Natal, Brazil. Springer. Proc. 15th Brazilian Symposium on Formal Methods (SBMF 2012). September 23-28, 2012. doi: 10.1007/978-3-642-33296-8_4
  • David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. SMT Solvers for Rodin. In Proc. Abstract State Machines, Alloy, B, VDM, and Z. Edited by John Derrick, John Fitzgerald, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, Elvinia Riccobene. Lecture Notes in Computer Science, volume 7316 Pages 194-207. 2012. Pisa, Italy. Springer Berlin Heidelberg. Proc. 15th Third International Conference, ABZ 2012. doi: 10.1007/978-3-642-30885-7_14
  • Haniel Barbosa, David Déharbe. Formal Verification of PLC Programs Using the B Method.. In Proc. Abstract State Machines, Alloy, B, VDM, and Z. Edited by John Derrick, John Fitzgerald, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, Elvinia Riccobene. Lecture Notes in Computer Science, volume 7316 Pages 353-356. 2012. Pisa, Italy. Springer Berlin Heidelberg. Proc. 15th Third International Conference, ABZ 2012. doi: 10.1007/978-3-642-30885-7_30
  • Marcel Oliveira, David Déharbe, Luiz Cruz. B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. In Proc. Formal Methods, Foundations and Applications. Edited by Adenilso Simão, Carroll Morgan. Lecture Notes in Computer Science, volume 7021 Pages 44-59. 2011. São Paulo, Brazil. Springer Berlin Heidelberg. doi: 10.1007/978-3-642-25032-3_4
  • David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. Exploiting Symmetry in SMT Problems. In Proc. Automated Deduction – CADE-23. Edited by Nikolaj Bjørner, Viorica Sofronie-Stokkermans. Lecture Notes in Computer Science, volume 6803 Pages 222-236. 2011. Wrocław, Poland. Springer Berlin Heidelberg. doi: 10.1007/978-3-642-22438-6_18
  • Alessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Vinícius Medeiros de Oliveira, David Déharbe. Integrating SMT-Solvers in Z and B Tools. Edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves. Lecture Notes in Computer Science, volume 5977 Pages 412-413. 2010. Orford, QC, Canada. Springer Berlin Heidelberg. Proc. Second International Conference, ABZ 2010. doi: 10.1007/978-3-642-11811-1_45
  • David Déharbe. Automatic Verification for a Class of Proof Obligations with SMT-Solvers. Edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves. Lecture Notes in Computer Science, volume 5977 Pages 217-230. 2010. Orford, QC, Canada. Springer Berlin Heidelberg. Proc. Second International Conference, ABZ 2010. doi: 10.1007/978-3-642-11811-1_17
  • Bruno Gomes, David Déharbe, Anamaria Martins Moreira, Katia Moraes. Applying the B Method for the Rigorous Development of Smart Card Applications. In Proc. Abstract State Machines, Alloy, B, VDM, and Z. Edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau, Steve Reeves. Lecture Notes in Computer Science, volume 5977 Pages 203-216. 2010. Orford, QC, Canada. Springer Berlin Heidelberg. Proc. Second International Conference, ABZ 2010. doi: 10.1007/978-3-642-11811-1_16

Papers In Workshop Proceedings

  • Mathieu Comptier, David Déharbe, Paulin Fournier, Julien Molinero Perez. Property-Driven Software Analysis - (Extended Abstract). In Proc. Formal Methods - The Next 30 Years. Industrial Day Presentations.. Edited by Maurice H. ter Beek, Annabelle McIver, José N. Oliveira. Lecture Notes in Computer Science, volume 11800 Pages 746-750. 2019. Porto, Portugal. Springer International Publishing. doi: 10.1007/978-3-030-30942-8_44
  • Lilian Burdy, David Déharbe, Étienne Prun. Interfacing Automatic Proof Agents in Atelier B: Introducing "iapa". In Proc. Proceedings of the Third Workshop on Formal Integrated Development Environment, F-IDE@FM 2016. Edited by Catherine Dubois, Paolo Masci, Dominique Méry. Electronic Proceedings in Theoretical Computer Science, volume 240 Pages 82-90. 06 November 2017. Limassol, Cyprus. doi: 10.4204/EPTCS.240.6
  • David Déharbe, Diego Azevedo, Ernesto Matos, Valério Medeiros Jr. BTestBox: an automatic test generator for B method. In Proc. VII Congresso Brasileiro de Software: Teoria e Prática - CBSoft 2016 - Sessão de Ferramentas. 21 September 2016. Maringá, Brazil.
  • Richard Bonichon, David Déharbe, Pablo Federico Dobal, Claudia Tavares. SMTpp: preprocessors and analyzers for SMT-LIB. In Proc. 13th International Workshop on Satisfiability Modulo Theories, (SMT 2015). Edited by Vijay Ganesh, Dejan Jovanović. 18 July 2015. San Francisco, CA, USA.
  • Richard Bonichon, David Déharbe, Claudia Tavares. Extending SMT-LIB v2 with λ-Terms and Polymorphism. In Proc. Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, (SMT 2014). Edited by Philipp Rümmer, Christoph M. Wintersteiger. CEUR Workshop Proceedings, volume 139 Pages 53-62. 17 July 2014. Vienna, Austria. http://ceur-ws.org/Vol-1163/paper-08.pdf
  • Valério Medeiros Jr, David Déharbe. BEval: a plug-in to extend Atelier B with current verification technologies. In Proc. Proceedings First Latin American Workshop on Formal Methods (LAFM 2013). Edited by Nazareno Aguirre, Leila Ribeiro. Electronic Proceedings in Theoretical Computer Science, volume 139 Pages 53-58. 26 August 2013. Buenos Aires, Argentina. doi: 10.4204/EPTCS.139.5
  • Carlos Areces, David Déharbe, Pascal Fontaine, Ezequiel Orbe. SyMT: finding symmetries in SMT formulas (Extended Abstract: Work in progress). In Proc. SMT Workshop 2013 - 11th International Workshop on Satisfiability Modulo Theories. Edited by Roberto Bruttomesso, Alberto Griggio. Pages 56-63. 08 July 2013. Helsinki, Finland. http://smt2013.fbk.eu
  • David Déharbe, Pablo Federico Dobal, Pascal Fontaine. Le solveur SMT veriT. In Proc. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL 2013). Edited by Jeanine Souquières, Virgine Wiels. Pages 91-92. 03 April 2013. Nancy, France. in French.
  • Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine. GridTPT: a distributed platform for Theorem Prover Testing. In Proc. PAAR-2010: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning. Edited by Renate A. Schmidt, Stephan Schulz, Boris Konev. EasyChair Proceedings in Computing (EPiC), volume 9 Pages 33-39. 2012. Edinburgh, UK. EasyChair. http://www.easychair.org/publications/?page=453348161
  • David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo. Quantifier Inference Rules for SMT proofs. In Proc. PxTP-2011 – First Workshop on Proof eXchange for Theorem Proving. Edited by Pascal Fontaine, Aaron Stump. Pages 33-39. 2011. Wrocław, Poland. Affiliated with CADE 2011. http://pxtp2011.loria.fr

  • . .